LoginSignup
3
1

More than 3 years have passed since last update.

@nekonibox(Kenta Inoue)

Coq/SSReflectで辞書式順序で引数が構造的に小さくなる再帰関数をFixpointで定義する

Last updated at Posted at 2020-09-24

はじめに

Coq/SSReflectで再帰関数を定義するとき、必ず停止する関数しか記述できません。特に特定の引数が必ず構造的に小さくなる場合でない場合は停止性の証明が必要になります。しかし、引数が複数あり、辞書式順序で構造的に小さくなる場合は停止性の証明を書かずに定義する方法があります。
基本的にはこちらのサイト「停止性が明らかでない関数を定義するには」を参考にしておりますが、定義だけでなく証明に必要な補題を作るところまで説明していきます。

辞書式順序で引数が構造的に小さくなる関数

本記事で考える関数は、以下の等式を満たす関数myfun : X -> Y -> Zのように、第一引数から順番にmatchで分岐して、再帰呼び出しする際のmyfunの引数が辞書的に構造的に小さくなっているものです。1

  myfun x y =
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn (* x0 ... xn : X *)
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym (* y0 ... yn : Y *)
             => gij (myfun x0) ... (myfun xn)
                    (myfun x y0) ... (myfun x ym)
                    x y a0 ... ak b0 ... bl
              (*
                gij : (Y -> Z) -> ... -> (Y -> Z) ->
                      Z -> ... -> Z ->
                      X -> Y -> ... -> ... ->
                      Z
              *)
         ...
         end
  ...
  end.

返り値を計算するgijではmyfunの再帰呼び出しを行いますが、第一引数が構造的に小さくなっている、すなわちmyfun x0 ... myfun xn であるか、第一引数がxのままで第二引数が構造的に小さくなっている、すなわちmyfun x y0 ... myfun x ymのいずれかで記述できるもののみで構成されています。

後述する解説ではこのmyfunを用いますが、一般的な例だけだと分かりづらいので、まずは具体例を見ていきます。

具体例

辞書式順序で引数が小さくなる再帰関数の例として以下のようなものが挙げられます。

引数のうち、どれか1つ以上が小さくなり、他の引数は変わらない再帰関数

再帰呼び出しを行うときの引数のうちどれか1つでも小さくなる場合は辞書式順序で引数が小さくなっていると言えます。
例えばPascalの三角形の(n,m)座標の値を求める関数Pascalは以下のように定義され、再帰呼び出しする際にはどちらかの引数が固定され、もう片方の引数が小さくなっています。

\operatorname{Pascal}(0,m) := 1\\
\operatorname{Pascal}(n,0) := 1\\
\operatorname{Pascal}(n+1,m+1) := \operatorname{Pascal}(n,m+1)+\operatorname{Pascal}(n+1,m)

Coqでこれをpascal : nat -> nat -> natとして実装したとき、満たすべき漸化式は以下のとおりです。

  pascal n m =
  match n with
  | 0 => 1
  | n'.+1 => match m with
           | 0 => 1
           | m'.+1 => pascal n' m + pascal n m'
           end
  end.
(*
  g11 (fn':nat -> nat) (fnm':nat) (n m:nat) : nat := fn' m + fnm'

  g11 (pascal n') (pascal n m') n m = pascal n' m + pascal n m' 
*)

上記以外の辞書式順序で引数が小さくなる再帰関数

Ackermann関数は上記に当てはまらない辞書式順序で引数が小さくなる関数です。

\operatorname{Ackermann}(0,m) := m+1\\
\operatorname{Ackermann}(n+1,0) := \operatorname{Ackermann}(n,1)\\
\operatorname{Ackermann}(n+1,m+1) := \operatorname{Ackermann}(n,\operatorname{Ackermann}(n+1,m))

これもCoqで実装したときに満たしてほしい性質は以下のとおりです。

  ackermann n m =
  match n with
  | 0 => m.+1
  | n'.+1 => match m with
            | 0 => ackermann n' 1
            | m'.+1 => ackermann n' (ackermann n m')
            end
  end.
(*
  g10 (fn':nat -> nat) (n m:nat) : nat := fn' 1
  g11 (fn':nat -> nat) (fn'm:nat) (n m:nat) : nat := fn' fnm'

  g10 (ackermann n') n m = ackermann n' 1
  g11 (ackermann n') (ackermann n m') n m = ackermann n' (ackermann n m')
*)

ここで挙げたpascalとackermannのCoqでの実装は後述します。まずは一般のmyfunの場合で説明します。

Fixpointを使って実装する

話を戻して、冒頭で説明したmyfunをFixpointを使って定義する方法を説明していきます。

まず、そのまま定義しようとすると引数の減少性が自明でないためエラーが出ます。

Fixpoint myfun (x:X) (y:Y) : Z :=
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym
             => gij (myfun x0) ... (myfun xn)
                    (myfun x y0) ... (myfun x ym)
                    x y a0 ... ak b0 ... bl
         ...
         end
  ...
  end.
(* Error: Cannot guess decreasing argument of fix. *)

そこで、以下のような手順でこの式を書き換えます。

手順

1.関数名を書き換える

Fixpoint myfun_rec (x:X) (y:Y) : Z := (* 関数名変更 *)
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym
             => gij (myfun_rec x0) ... (myfun_rec xn)
                    (myfun_rec x y0) ... (myfun_rec x ym)
                    x y a0 ... ak b0 ... bl
                    (* 再帰呼び出し部分も関数名変更 *)
         ...
         end
  ...
  end.

名称変更はしなくてもいいですが、証明中simplした際に式が不必要に展開されるを防ぐため、行っておくことをオススメします。

2.fix文を入れる

第二引数(y)のmatch文の前にlet fixを挿入してその内部式全体を返す関数(myfun_rec')を定義し、返り値を今定義した関数で書き換えます。このとき、内部関数の引数は元の関数の引数と同じ型、同じ値にします。

Fixpoint myfun_rec (x:X) (y:Y) : Z :=
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => let fix myfun_rec' x y := (* 追加 *)
             match y with
             ...
             | ConYj b0 ... bl y0 ... ym
                 => gij (myfun_rec x0) ... (myfun_rec xn)
                        (myfun_rec x y0) ... (myfun_rec x ym)
                        x y a0 ... ak b0 ... bl
             ...
             end in
         myfun_rec' x y (* 追加 *)
  ...
  end.

3.再帰呼び出し部分の変更

再帰呼び出しをしている関数のうち、第一引数が元の引数と同じもの(xのままのもの)をfixで定義した内部関数名(myfun_rec')で書き換えます。

Fixpoint myfun_rec (x:X) (y:Y) : Z :=
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => let fix myfun_rec' x y :=
             match y with
             ...
             | ConYj b0 ... bl y0 ... ym
                 => gij (myfun_rec x0) ... (myfun_rec xn)
                        (myfun_rec' x y0) ... (myfun_rec' x ym) (* この部分 *)
                        x y a0 ... ak b0 ... bl
             ...
             end in
         myfun_rec' x y
  ...
  end.

この時点でFixpointの定義が通るようになります。23

4.元の関数をDefinitionで再定義する。

本来、関数名として付けたかった名前をDefinitionで再定義します。

Definition myfun := myfun_rec.

こうしておくと、証明中にsimplしてもmyfunが元のmyfun_recの定義式に分解されず、fixなどの煩雑な式が命題中に表示されるのを防ぐことができます。

追加で用意しておきたい補題

上記のような流れで再帰関数をFixpointで定義できますが、定義しただけでは証明する際に使いづらいので、以下のような補題を用意しておくといいと思います。

equation

本来myfunを定義したかった漸化式そのものです。Functionで定義した場合は自動生成されますが、今回の方法では自分で定義する必要があります。
この補題は、主に証明中でsimplの代わりにrewrite myfun_equation.の形で使います。
これでmyfunの実装がどうであるかを考えずに、元の漸化式だけを考えて証明することができます。

Lemma myfun_equation x y :
  myfun x y =
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym
             => gij (myfun x0) ... (myfun xn)
                    (myfun x y0) ... (myfun x ym)
                    x y a0 ... ak b0 ... bl
         ...
         end
  ...
  end.
Proof.
  by case : x; case : y.
Qed.

myfun_equation自体の証明ですが、全ての引数に対してcaseを行うだけで示せるはずです。

帰納原理

必須というわけではないですが、帰納原理も作っておくと便利です。

Lemma myfun_ind (P:X -> Y -> Prop) :
  ... ->
  (forall a0 ... ak x0 ... xn b0 ... bl y0 ... ym,
   P x0 (...) ->
   ...
   P xn (...) ->
   (*
     第二引数はgij内部のmyfun xi (...)と同じ形になるように。
     gij中に記述がない場合は仮定しなくてよい。
     場合によっては命題を(forall y, P xi y)の形にするのも可。
   *)
   P (ConXi a0 ... ak x0 ... xn) y0 ->
   ...
   P (ConXi a0 ... ak x0 ... xn) ym ->
   (* 仮定はgijの内部でmyfun x yjの記述があるものだけでよい *)
   P (ConXi a0 ... ak x0 ... xn) (ConYj b0 ... bl y0 ... ym)) ->
  ... ->
  forall x y, P x y.
Proof.
  move => ... Hij ... x y.
  elim : x =>[...|a0 ... ak x0 ... xn IHx0 ... IHxn|...] in y *;
    elim : y =>[...|b0 ... bl y0 ... ym IHy0 ... IHym|...].
  ...
  - exact : Hij.
    (*
      (Hij (IHx0 ...) ... (IHxn ...) IHy0 ... IHym)
      の形で書けるはずなのでexactで通ると思います。
     *)
  ...
Qed.

証明は辞書式順序で引数が減少しているので、elim : x =>[...] in y *; elim : y.で示せると思います。

実用例

辞書式順序で引数が小さくなる関数の例として出したPascalの三角形とAckermann関数を例に定義してみます。

Pascalの三角形

Fixpoint pascal_rec n m :=
  match n with
  | 0 => 1
  | n'.+1 => let fix pascal_rec' n m :=
              match m with
              | 0 => 1
              | m'.+1 => pascal_rec n' m + pascal_rec' n m'
              end in
            pascal_rec' n m
  end.

Definition pascal := pascal_rec.

Lemma pascal_equation n m:
  pascal n m =
  match n with
  | 0 => 1
  | n'.+1 => match m with
           | 0 => 1
           | m'.+1 => pascal n' m + pascal n m'
           end
  end.
Proof.
  by case : n; case : m.
Qed.

Lemma pascal_ind (P:nat -> nat -> Prop) :
  (forall m, P 0 m) ->
  (forall n, P n.+1 0) ->
  (forall n m, P n.+1 m -> P n m.+1 -> P n.+1 m.+1) ->
  forall n m, P n m.
Proof.
  move => H0m Hn0 Hnm n m.
  elim : n =>[|n IHn] in m *; elim : m =>[|m IHm]=>//.
  - exact : Hnm.
Qed.

ちなみにpascal_recの内部関数はもう少し省略して記述できます。23

Fixpoint pascal2_rec n m :=
  match n with
  | 0 => 1
  | n'.+1 => (fix pascal2_rec'n m :=
              match m with
              | 0 => 1
              | m'.+1 => pascal2_rec n' m + pascal2_rec'n m'
              end) m
  end.

Ackermann関数

Fixpoint ackermann_rec n m :=
  match n with
  | 0 => S m
  | n'.+1 => let fix ackermann_rec' n m :=
                match m with
                | 0 => ackermann_rec n' 1
                | m'.+1 => ackermann_rec n' (ackermann_rec' n m')
                end in
             ackermann_rec' n m
  end.

Definition ackermann := ackermann_rec.

Lemma ackermann_equation n m:
  ackermann n m =
  match n with
  | 0 => S m
  | n'.+1 => match m with
            | 0 => ackermann n' 1
            | m'.+1 => ackermann n' (ackermann n m')
            end
  end.
Proof.
    by case : n; case : m.
Qed.

Lemma ackermann_ind (P:nat -> nat -> Prop) :
  (forall m, P 0 m) ->
  (forall n, P n 1 -> P n.+1 0) ->
  (forall n m, P n.+1 m -> P n (ackermann n.+1 m) -> P n.+1 m.+1) ->
  forall n m, P n m.
Proof.
  move => H0m Hn0 Hnm n m.
  elim : n =>[|n IHn] in m *=>//; elim : m =>[|m IHm].
  - exact : Hn0.
  - exact : Hnm.
Qed.

ackermann_ind内部にackermannが現れて少し気持ち悪いですが、一応これで簡単な命題は示せると思います。

まとめ

辞書式順序で引数が構造的に小さくなる再帰関数をFixpointで定義する方法について記述しました。今回の説明は2変数関数の場合ですが、他変数関数でも同様に記述することができるので、この方法を参考にしていただければ幸いです。

  1. この例は2変数関数ですが、多変数関数でも同様に考えることができます。 ↩

  2. 内部関数myfun_rec'の引数xは実は引数として受け取る必要はないため、xの値は外部変数とし、yの値だけ受け取る1変数関数として定義してもいいです。 ↩

  3. myfun_rec'は外部で1回しか使わないため、let fixではなく単にfixで定義してそのまま引数を渡してもいいです。 ↩

3
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
3
1