More than 5 years have passed since last update.

@nekonibox(Kenta Inoue)

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

Last updated at 2020-09-25Posted at 2020-09-24

はじめに

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

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

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

myfunxy=matchxwith...|ConXia0...akx0...xn(* x0 ... xn : X *)=>matchywith...|ConYjb0...bly0...ym(* y0 ... yn : Y *)=>gij(myfunx0)...(myfunxn)(myfunxy0)...(myfunxym)xya0...akb0...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として実装したとき、満たすべき漸化式は以下のとおりです。

pascalnm=matchnwith|0=>1|n'.+1=>matchmwith|0=>1|m'.+1=>pascaln'm+pascalnm'endend.(*
 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で実装したときに満たしてほしい性質は以下のとおりです。

ackermannnm=matchnwith|0=>m.+1|n'.+1=>matchmwith|0=>ackermannn'1|m'.+1=>ackermannn'(ackermannnm')endend.(*
 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を使って定義する方法を説明していきます。

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

Fixpointmyfun(x:X)(y:Y):Z:=matchxwith...|ConXia0...akx0...xn=>matchywith...|ConYjb0...bly0...ym=>gij(myfunx0)...(myfunxn)(myfunxy0)...(myfunxym)xya0...akb0...bl...end...end.(* Error: Cannot guess decreasing argument of fix. *)

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

手順

1.関数名を書き換える

Fixpointmyfun_rec(x:X)(y:Y):Z:=(* 関数名変更 *)matchxwith...|ConXia0...akx0...xn=>matchywith...|ConYjb0...bly0...ym=>gij(myfun_recx0)...(myfun_recxn)(myfun_recxy0)...(myfun_recxym)xya0...akb0...bl(* 再帰呼び出し部分も関数名変更 *)...end...end.

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

2.`fix`文を入れる

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

Fixpointmyfun_rec(x:X)(y:Y):Z:=matchxwith...|ConXia0...akx0...xn=>letfixmyfun_rec'xy:=(* 追加 *)matchywith...|ConYjb0...bly0...ym=>gij(myfun_recx0)...(myfun_recxn)(myfun_recxy0)...(myfun_recxym)xya0...akb0...bl...endinmyfun_rec'xy(* 追加 *)...end.

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

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

Fixpointmyfun_rec(x:X)(y:Y):Z:=matchxwith...|ConXia0...akx0...xn=>letfixmyfun_rec'xy:=matchywith...|ConYjb0...bly0...ym=>gij(myfun_recx0)...(myfun_recxn)(myfun_rec'xy0)...(myfun_rec'xym)(* この部分 *)xya0...akb0...bl...endinmyfun_rec'xy...end.

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

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

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

Definitionmyfun:=myfun_rec.

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

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

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

equation

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

Lemmamyfun_equationxy:myfunxy=matchxwith...|ConXia0...akx0...xn=>matchywith...|ConYjb0...bly0...ym=>gij(myfunx0)...(myfunxn)(myfunxy0)...(myfunxym)xya0...akb0...bl...end...end.Proof.bycase:x;case:y.Qed.

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

帰納原理

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

Lemmamyfun_ind(P:X->Y->Prop):...->(foralla0...akx0...xnb0...bly0...ym,Px0(...)->...Pxn(...)->(*
 第二引数はgij内部のmyfun xi (...)と同じ形になるように。
 gij中に記述がない場合は仮定しなくてよい。
 場合によっては命題を(forall y, P xi y)の形にするのも可。
 *)P(ConXia0...akx0...xn)y0->...P(ConXia0...akx0...xn)ym->(* 仮定はgijの内部でmyfun x yjの記述があるものだけでよい *)P(ConXia0...akx0...xn)(ConYjb0...bly0...ym))->...->forallxy,Pxy.Proof.move=>...Hij...xy.elim:x=>[...|a0...akx0...xnIHx0...IHxn|...]iny*;elim:y=>[...|b0...bly0...ymIHy0...IHym|...]....-exact:Hij.(*
 (Hij (IHx0 ...) ... (IHxn ...) IHy0 ... IHym)
 の形で書けるはずなのでexactで通ると思います。
 *)...Qed.

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

実用例

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

Pascalの三角形

Fixpointpascal_recnm:=matchnwith|0=>1|n'.+1=>letfixpascal_rec'nm:=matchmwith|0=>1|m'.+1=>pascal_recn'm+pascal_rec'nm'endinpascal_rec'nmend.Definitionpascal:=pascal_rec.Lemmapascal_equationnm:pascalnm=matchnwith|0=>1|n'.+1=>matchmwith|0=>1|m'.+1=>pascaln'm+pascalnm'endend.Proof.bycase:n;case:m.Qed.Lemmapascal_ind(P:nat->nat->Prop):(forallm,P0m)->(foralln,Pn.+10)->(forallnm,Pn.+1m->Pnm.+1->Pn.+1m.+1)->forallnm,Pnm.Proof.move=>H0mHn0Hnmnm.elim:n=>[|nIHn]inm*;elim:m=>[|mIHm]=>//.-exact:Hnm.Qed.

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

Fixpointpascal2_recnm:=matchnwith|0=>1|n'.+1=>(fixpascal2_rec'nm:=matchmwith|0=>1|m'.+1=>pascal2_recn'm+pascal2_rec'nm'end)mend.

Ackermann関数

Fixpointackermann_recnm:=matchnwith|0=>Sm|n'.+1=>letfixackermann_rec'nm:=matchmwith|0=>ackermann_recn'1|m'.+1=>ackermann_recn'(ackermann_rec'nm')endinackermann_rec'nmend.Definitionackermann:=ackermann_rec.Lemmaackermann_equationnm:ackermannnm=matchnwith|0=>Sm|n'.+1=>matchmwith|0=>ackermannn'1|m'.+1=>ackermannn'(ackermannnm')endend.Proof.bycase:n;case:m.Qed.Lemmaackermann_ind(P:nat->nat->Prop):(forallm,P0m)->(foralln,Pn1->Pn.+10)->(forallnm,Pn.+1m->Pn(ackermannn.+1m)->Pn.+1m.+1)->forallnm,Pnm.Proof.move=>H0mHn0Hnmnm.elim:n=>[|nIHn]inm*=>//;elim:m=>[|mIHm].-exact:Hn0.-exact:Hnm.Qed.

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

まとめ

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

この例は2変数関数ですが、多変数関数でも同様に考えることができます。 ↩
内部関数myfun_rec'の引数xは実は引数として受け取る必要はないため、xの値は外部変数とし、yの値だけ受け取る1変数関数として定義してもいいです。 ↩ ↩²
myfun_rec'は外部で1回しか使わないため、let fixではなく単にfixで定義してそのまま引数を渡してもいいです。 ↩ ↩²

Go to list of users who liked

Go to list of comments

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

URL: https://qiita.com/nekonibox/items/3d483edf4eb46adbfae7