ロジャースの不動点定理

関数$ Fが計算可能ならば不動点を持つ

定理 ref 『C言語による計算の理論』.icon p.61

どんな計算可能1変数全域関数$ fに対しても$ k入力プログラム$ Rが存在して以下が成り立つ

$ Rのコードを$ rとすると、$ rと$ f(r)は$ k変数部分関数に解釈すれば同じである

さくっというと

任意の1変数関数$ fについて、

そのコード$ rと、$ f(r)は同じである

証明

目的は$ S^1_k(v,v)と$ f(S^1_k(v,v))が等しいということをいいたい

ここで$ vは定数的なもの #??

$ f(S^1_k(v,v))は

S-m-n定理のもので、

「$ k引数関数」のコード

第一引数の$ vもコードで、第2引数は「$ vに渡す末尾の引数」

https://gyazo.com/e693a9d0cdb1575b17cc23354f2aef8d

$ g(x_1,x_2,\cdots,x_k,v):=\mathrm{comp}(f(S^1_k(v,v)),\lang x_1,\cdots,x_k\rang)

というふうに関数$ gを定義する(右から左に読む)

$ fは任意の1変数全域関数

$ S^1_k(v,v)は不動点になる

具体的には$ r=S^1_k(\mathrm{g},\mathrm{g})が不動点

https://gyazo.com/b8308effc0e4c7e2139369b719533d13

参考