数学基礎論講義をこっそり読む（その５） - Finite Groups Fun 有限群あるいはちょこっと計算ファンの日記

PART A 第４講に入りました。テキストのこの講はかなり駆け足というか猛ダッシュで、クリーネの標準型定理が説明だけなのは肩すかしをくらったような感がありますが、計算論のどの教科書にも載っている内容だからということなのかもしれません。私もちょこちょこ勉強していたところなので、まあいいか。

アッケルマン（Ackermann)関数に関する問題４、５を解いてみます。

まずはp.51の問題４ですが、以前にAckermann関数が原始帰納的（原始再帰的）関数でないことの証明は紹介したことがあったのですが、そういえば帰納的（再帰的）関数であることの証明はやってませんでした。まずは、スマートな証明から。

3変数の再帰的部分関数 $h(x,y,e)$ を次のように定める。

$h(x,y,e)=\begin{cases} y+1, & \mbox{if }x=0 \\ \{e\}(x\dot{-} 1,\ 1), & \mbox{if } y=0 \mbox{ and } x\ge 1 \\ \{e\}(x\dot{-}1, \ \{e\}(x,y\dot{-}1)) , & \mbox{if } y\ge 1 \mbox{ and } x\ge 1} \end{cases}$

これに再帰定理（定理4.9）を適用して得られる $e$ がAckermann関数に一致することになり、再帰的であることが証明されます。ただ、再帰定理を使うと（一見）すごくスマートですが、結局、定義域が全域であることの証明は地味に必要となります。しかも、次の問題５『Ackermann関数のグラフは原始再帰的集合である』を解こうとすると、この証明ではまったく手がかりがありません。そこでいかにも計算してますというような別の証明方法も紹介します。

Ackermann関数 $A(x,y)$ の定義をぐっとにらむと、計算の途中は全て

$A(y_1,A(y_2,A(y_3,\cdots A(y_{n-1},y_n))\cdots)$

という形をしていることに気づきます。そこでこれを整数の有限列 $s=(y_1,y_2,\cdots,y_n)$ で表示することを考えます。計算過程ではこの列の長さも変化します。Ackermann関数の定義はこの整数列に対する操作と解釈できて、

$s'=\begin{cases} (y_1,\cdots,y_{n-2},y_n+1), & \mbox{if }y_{n-1}=0 \\ (y_1,\cdots,y_{n-2},y_{n-1}-1,1), & \mbox{if } y_{n-1}=0 \mbox{ and } y_n=0 \\ (y_1,\cdots,y_{n-2},y_{n-1}-1,y_{n-1},y_n-1) , & \mbox{if } y_{n-1}\ge 1 \mbox{ and } y_n\ge 1} \end{cases}$

と定義します。常に列の最後の２つの数字を見て、列を変形します。例によってちょこっと計算してみます。

(define (ack x y)
  (let ((s (list y x)))
    (let loop ((ss s))
      (display (reverse ss))
      (newline)
      (cond
        ((= (length ss) 1) (car ss))
        (else (let ((y (car ss)) (x (car (cdr ss))) (sss (cdr (cdr ss))))
        (cond
          ((= x 0) (loop (append (list (+ y 1)) sss)))
          ((= y 0) (loop (append (list 1 (- x 1)) sss)))
          (else (loop (append (list (- y 1) x (- x 1)) sss))))))))))

> (ack 2 2)
(2 2)
(1 2 1)
(1 1 2 0)
(1 1 1 1)
(1 1 0 1 0)
(1 1 0 0 1)
(1 1 0 2)
(1 1 3)
(1 0 1 2)
(1 0 0 1 1)
(1 0 0 0 1 0)
(1 0 0 0 0 1)
(1 0 0 0 2)
(1 0 0 3)
(1 0 4)
(1 5)
(0 1 4)
(0 0 1 3)
(0 0 0 1 2)
(0 0 0 0 1 1)
(0 0 0 0 0 1 0)
(0 0 0 0 0 0 1)
(0 0 0 0 0 2)
(0 0 0 0 3)
(0 0 0 4)
(0 0 5)
(0 6)
(7)
7

さて、この計算列ですが、変形の途中で同じパターンは現れることなく、また横の長さの最大は $A(x,y)$ です（∵それ以上長くなるとそもそも値が $A(x,y)$ を超えてしまう）。各要素も最大は $A(x,y)$ ですので、結局この計算列に現れるパターンは有限なので、いつかは停止することがわかります。計算列の変形 $s'=\varphi(s)$ は原始再帰的なので、そのn回の繰り返し $\phi(n,s)=\varphi^n(s)$ も原始再帰的で、 $A(x,y)=\phi(\mu n\quad \mathbf{length}(\phi(n,(x,y)))=1,\quad (x,y))$ となるため、再帰的かつ全域関数となります。

さて、p.52 問題５『Ackermann関数のグラフは原始再帰的集合である』です。そのグラフとは

$G=\{(x,y,z)\mid z=A(x,y)\quad \}$

ですが、 $A(x,y)$ が原始再帰的でないのになんで、zが増えたぐらいで原始再帰的になるの？というところが不思議なところです。しかし、そのzに計算回数に関する情報がそっくり含まれているというのがミソになっています。実際、先の計算列に対する考察から、繰り返し回数は $z^z$ を超えることがないため、[tex:G=\{(x,y,z)\mid z=\phi(\exist n