アッカーマン関数のAgdaでの定義
Agdaは現在開発真っ最中の言語で、昨日停止判定を合格しなかったプログラムが、今日の最新版では合格していたりすることが結構あります。例えば、ヒビルテさんのところの2006年3月25日*1に「アッカーマン関数の停止性を認識できない」と書かれていますが、現在のAgda 2 では以下の定義で停止判定に楽勝で合格します。
ack : (m n : Nat) -> Nat
ack zero n = s n
ack (s m) zero = ack m (s zero)
ack (s m) (s n) = ack m (ack (s m) n)
もちろん、自然数のデータ型は
data Nat : Set where
zero : Nat
s : Nat -> Nat
で定義しています。
Agdaの停止判定の機構については、聞いてみたところ、いまだに「foetus と本質的に変化はないはず」といわれました*2。実際に、Abel がfoetusで停止判定に合格しない人工的な再帰関数の例としてあげている*3以下の関数 f, g は、Agda2においても停止判定に合格しませんでした。
h : (x y : Nat) -> Nat
h zero zero = zero
h zero (s y) = h zero y
h (s x) y = h x y
mutual
f : (x y : Nat) -> Nat
f zero z = zero
f (s x) zero = zero
f (s x) (s y) = h (g x y) (f (s (s x)) y)
g : (x y : Nat) -> Nat
g zero y = zero
g (s x) zero = zero
g (s x) (s y) = h (f x y) (g x (s (s y)))
関数 h は、人間の目には、任意の x : Nat に対して h(x)=0 はとなるのは明らかです。
foetus の停止判定メカニズムは、この場合に関しては「コンストラクターの数が減る=非循環的定義」と見なしてよいようです。そのため g の定義で、g (s x) (s y) を (g x (s (s y))) を使用して定義している部分で y に関してコンストラクター s が増えており、これが停止判定に合格しない原因となります。ちなみに、最後の行をg (s x) (s y) = h (f x y) (g x (s y))に書き直すと、停止判定に合格します（当たり前ですが）。
補足
コメント欄でお教えいただいた通り、2007年12月1日に、ヒビルテさんがアッカーマン関数の停止性についてすでに書かれていました。事実誤認をお詫びいたします。
・・・っていうか、オレ、その記事12月1日の当日にブックマークしているじゃん・・・（汗）。
