再帰定理とY-combinator - Finite Groups Fun 有限群あるいはちょこっと計算ファンの日記

同じく高橋正子著『計算論』近代科学社のp.51から:

補題1.6.10
$\rm{comp}_n(z,\vec{x})$ を $z$ が $n$ 個の引数 $\vec{x}\in N^n$ を取る計算プログラム $P$ のコードとしたとき，その計算結果を返す関数とする( $z$ がプログラムのコードでなかったり，計算が止まらないときは未定義とする）.
このとき任意の帰納的な全域関数 $f:N\to N$ に対して，ある自然数 $c$ が存在して，
$\quad\quad\rm{comp}_n(c,\vec{x})=\rm{comp}_n(f(c),\vec{x})$

$\rm{comp}_n(z,\vec{x})$ は，それ以前に詳しく定義されている部分帰納的関数で， $z$ を動かすことで（部分）帰納的関数を枚挙するものになっている．ただし， $z$ がプログラムのコード（ゲーデル数を使ったプログラムのコード化）でない場合は未定義なので，かなりスカスカした感じである．

テキストではひっそりと再帰定理と書いてあるが，特にそれに関しては言及がない．あくまで次のRiceの定理を証明するための補題との位置づけである．
それにしてもこの補題の主張はかなり奇妙な感じがする．というのは， $c$ および $f(c)$ がプログラムのコードでない場合は，定義域全域で未定義の関数が等しいといっているだけに思えるからである．もし， $c$ として，定義域が空でない部分帰納的関数のプログラムコードになっているものが存在するとなるとかなりすごい主張なのであるが， $f$ が任意なので $f(c)$ がそのようなプログラムコードになっている一般的な保障などはありそうにない．ただし， $f$ をうまく取れば， $c$ が全域で定義された帰納関数のコードになる場合がある．そのひとつの例を次に述べるが，この定理（Kleeneに拠る）が再帰定理と呼ばれる理由になっている．

$N^{n}$ 上の全域で定義された帰納的関数 $g(\vec{x})$ と $N^{n+2}$ の全域で定義された帰納的関数 $h(\vec{x},y,z)$ を任意に選んでおく．
$f$ として $N^{n+1}$ 上の部分帰納的関数のプログラムコード $P$ を $N^{n+1}$ 上の部分帰納的関数のプログラムコード $f(P)$ に移す次のようなものを取る：
$\quad\quad\rm{comp}_{n+1}(f(P),\vec{x},0)=g(\vec{x})$
$\quad\quad\rm{comp}_{n+1}(f(P),\vec{x},y+1)=h(\vec{x},y,\rm{comp}_{n+1}(P,\vec{x},y))$
このように $f$ を定義しておき(Pが帰納的関数のコードでない場合でも，上の定義をそのまま適用すれば， $f(P)$ は部分帰納的関数のコードになる.よって， $f$ は全域で定義されている)，補題を適用すると，
$\quad\quad\rm{comp}_{n+1}(c,\vec{x},y)=\rm{comp}_{n+1}(f(c),\vec{x},y)$
なる自然数 $c$ が存在する． $\phi(\vec{x},y)\equiv\rm{comp}_{n+1}(c,\vec{x},y)$ と定義すると, $f$ の定義と，補題の関係式より
$\quad\quad\phi(\vec{x},0)=\rm{comp}_{n+1}(f(c),\vec{x},0)=g(\vec{x})$
$\quad\quad\phi(\vec{x},y+1)=\rm{comp}_{n+1}(f(c),\vec{x},y+1)=h(\vec{x},y,\rm{comp}_{n+1}(c,\vec{x},y))=h(\vec{x},y,\phi(\vec{x},y))$
が成立する．すなわちこれは $\phi$ が， $g$ と $h$ から再帰的に定義された帰納関数であるということになっている（したがって全域で定義されている）．
定理の形からは不動点定理なわけであるが，不動点＝再帰という公式は計算論ではよくある話のようである．

$\lambda$ 計算では，関数を関数に移す写像の不動点を作り出すものということでは，Y-combinatorと呼ばれるものがある．
$\quad\quad Y\equiv\lambda y.(\lambda x.y(xx))(\lambda x.y(xx))$
が，その定義であるが，かなりけったいな代物ではある．この演算子は引数に関数を関数に移す写像 $f$ を取り，結果 $Yf$ は関数となる．この結果の関数がどういう形になるかを計算してみると
[tex:\quad\quad Yf=(\lambda x.f(xx))(\lambda x.f(xx))= f*1(\lambda x.f(xx)))=f(Yf)]
と確かに形式的には $f$ の不動点になるわけだが，内容的には代入の無限後退が起こっており， $\lambda x.f(xx)$ の $xx$ の部分を集合論の言葉で表現しようとすると面倒なことが起こる．そのための理論が $\lambda$ 計算のモデルであり，テキストである『計算論』の主題になっている.

ここでは上の補題とY-combinatorの関連について考察してみる．補題の証明を振り返れば
$\quad\quad\rm{comp}_{n+1}(y,\vec{x},y)=\rm{comp}_{n+1}(a,\vec{x},y)=\rm{comp}_{n}(s_{1,n}(a,y),\vec{x})$

によって， $s_{1,n}(a,y)$ は，『n+1個の引数をとる部分帰納的関数のコード $y$ を与えたとき，最後の引数に自身のコードを代入することで n個の引数をとる部分帰納的関数にしたもの』のコードである．これに $f$ を写像した自然数をn個の引数をとる部分帰納的関数のコードとした計算は，
$\quad\quad\rm{comp}_{n}(f(s_{1,n}(a,y)),\vec{x})$
となる．証明のこの部分から，また $f$ の不動点の存在ということからも， $f$ が『n個の引数をとる部分帰納的関数のコードをn個の引数をとる部分帰納的関数のコードに写像する』ぐらいの制限が無いと実質的には意味をなさないということがわかる．
さて，この計算は $y$ と $\vec{x}$ のn+1個の引数をとる部分帰納関数でもあるから，そのコードを $b$ とすると，
$\quad\quad\rm{comp}_{n}(f(s_{1,n}(a,y)),\vec{x})=\rm{comp}_{n+1}(b,\vec{x},y)$ ．
左辺はきちんときまった計算であり，コード $b$ には何の不思議もない．

さて，コード $b$ はn+1個の引数をとる部分帰納関数であるから， $s_{1,n}(a,y)$ の $y$ のところに代入することで $c=s_{1,n}(a,b)$ が定義できる．
$\quad\quad\rm{comp}_{n}(f(s_{1,n}(a,b)),\vec{x})=\rm{comp}_{n+1}(b,\vec{x},b)=\rm{comp}_{n}(s_{1,n}(a,b),\vec{x})$
より， $\rm{comp}_{n}(f(c),\vec{x})=\rm{comp}_{n}(c,\vec{x})$ が成立するため， $c$ が題意を満たす自然数になっている．ただし，直接 $f(c)=c$ が成立しているわけではない．あくまでコード $f(c)$ とコード $c$ は，n個の引数をとる部分帰納関数としてどちらも同じものを与えるという意味での不動点である．

ここで簡単のために， $n=0$ の場合を考えてみる．このとき $s_{1,0}(a,y)$ は，
$\rm{comp}_{0}(s_{1,0}(a,y))=\rm{comp}_{1}(y,y)$ なのであるが，この右辺を $y(y)$ あるいは $yy$ と書いてしまえば，Y-combinatorに現れる $\lambda x.f(xx)$ の $xx$ との関連が浮かんでくる．対応は，
$s_{1,0}(a,y) \leftrightarrow yy$
$b \leftrightarrow \lambda x.f(xx)$
$c=s_{1,0}(a,b) \leftrightarrow bb=(\lambda x.f(xx))(\lambda x.f(xx))$
となり，再帰定理での不動点 $c$ とY-combinatorの作用の結果である不動点 $Yf=(\lambda x.f(xx))(\lambda x.f(xx))$ がぴったり対応する．
ここでいう対応とは $\lambda$ 計算のモデル理論で厳密に定義されるものである．テキストの前半で展開されている，部分帰納関数の計算プログラムのゲーデル数によるコーディングを使ったこのモデルはたぶん $P_\omega$ の部分モデルになってると思われるが，不勉強ゆえ正確なところはまだ私にはわからない．

*1:\lambda x.f(xx