アッカーマン関数を Coq で定義する方法はいろいろなところで説明があるが、 自分でも定義してみた
Definition ack :=
fix ack1 (m : nat) :=
fix ack2 (n : nat) :=
match m with
| 0 => S n
| S m' =>
match n with
| 0 => ack1 m' 1
| S n' => ack1 m' (ack2 n')
end
end.
この書き方がよい、というわけではないのだが、これを書いたことで、 どういう場合に Coq で定義できる (termination checker を通せる) のかはわかった気がする
アッカーマン関数 ack(m,n) の定義の再帰呼び出しを見直すと、 第1引数 m が確実に減る呼び出しでは第2引数 n が増えることも減ることもあるけれど、 第2引数 n が確実に減る呼び出しでは第1引数は変わらない
上の定義だと、ack1 のところは m が確実に減るのだが、n が増えるか減るかはわからない。 ack2 のところは、m は変わらず、n は減る
ちなみに、m は ack2 の外で定義されているので、ack2 は引数としては m は受け取らない。 受け取らないので m は変えられないけど、ack2 は m が変わらないところで呼び出されるので問題ない
なので、引数の並びが辞書順で減少していく場合は定義できるのではないか
引数の数だけ fix を重ねて、内部の再帰呼び出しでは、 その呼び出しで変化 (減少) するいちばん左の引数に対応する fix で束縛された関数を呼び出せばいい
[latest]