クリーネの再帰定理＋ Quine が書けることの証明

Ruby

クリーネの再帰定理のプログラマ向け説明（＋証明）を書いてみました。何か間違ってたら教えて！

前提

  • すべてのプログラムは文字列を 1 つ入力して文字列を 1 つ出力する、という世界を考えます。なお、プログラム自体も当然文字列です。
  • プログラムは eval っぽい命令を使っていいことにします。つまり、プログラムpと、pへの入力文字列sを受け取って、pを実行した結果の出力文字列を返す関数 E(p, s) が利用可能です。*1
  • 二つのプログラム p と q が完全に同じように振る舞うとき、p 〜 q と書くことにします*2。これは明らかに推移的。

定理

任意のプログラム f に対し、p 〜 E(f, p) となるようなプログラム文字列 p が存在する。*3

定理の証明

以下のような 3 つの文字列を考えます。

  • h: 入力文字列 x に対し、E(x, x) の結果を出力するプログラム*4
  • e: 入力文字列 x に対し、E(f, E(h, x)) の結果を出力するプログラム
  • p: プログラム e を入力文字列としてプログラム h を実行した時の出力文字列

このとき、

  • 任意の x に対し、E(h, x) 〜 E(x, x)
  • 任意の x に対し、E(e, x) 〜 E(f, E(h, x))
  • p 〜 E(h, e)

が言えます。よって、

  • p 〜 E(h, e) 〜 E(e, e) 〜 E(f, E(h, e)) 〜 E(f, p)

つまり p 〜 E(f, p) 。

Quine が存在することの証明

以下のように f を決めます。

  • f: 入力文字列 x に対し、「x を画面に表示するプログラム*5」を出力するプログラム

このとき、

  • 任意の x に対し、E(f, x) 〜「文字列 x を画面に表示するプログラム」

が言えます。上で示した定理から、

  • p 〜 E(f, p) 〜 「文字列 p を画面に表示するプログラム」

となるプログラム p が存在する、とわかります。

p は「文字列 p を画面に表示するプログラム」と完全に同じように振る舞う、ということはこれはまさに Quine！

よくわからん、Ruby で説明してくれ

h = '->(x) { "->(y) { eval(eval(%1$s).call(%1$s)).call(y) }" % x.dump }'
e = '->(x) { eval(f).call(eval(h).call(x)) }'
p = eval(h).call(e)
f = '->(x) { "->(y) { puts %s }" % x.dump }'

puts "source:"
puts p

puts "---"

puts "result:"
eval(p).call(nil)

call-by-value 対策で h をイータ展開してますが、ほぼ証明と同じ定義です。

$ ruby kleene.rb
source:
->(y) { eval(eval("->(x) { eval(f).call(eval(h).call(x)) }").call("->(x) { eval(f).call(eval(h).call(x)) }")).call(y) }
---
result:
->(y) { eval(eval("->(x) { eval(f).call(eval(h).call(x)) }").call("->(x) { eval(f).call(eval(h).call(x)) }")).call(y) }

無事 Quine しているようです。
「f とか h とか未定義じゃん！」とか「Proc 返すだけで実行してないじゃん！」とか細かいことを言う人はこちら。

h = '->(x) { "->(y) { eval(eval(%1$s).call(%1$s)).call(y) }" % x.dump }'
e = '->(x) { eval(f).call(eval(h).call(x)) }'
p = eval(h).call(e)
f = '->(x) { "->(y) { puts %s + \".call(nil)\" }" % x.dump }'

e = e.sub("f") { f.dump }
e = e.sub("h") { h.dump }
p = eval(h).call(e) + ".call(nil)"

puts p

$ ruby kleene2.rb > quine.rb
$ cat quine.rb
->(y) { eval(eval("->(x) { eval(\"->(x) { \\\"->(y) { puts %s + \\\\\\\".call(nil)\\\\\\\" }\\\" % x.dump }\").call(eval(\"->(x) { \\\"->(y) { eval(eval(%1$s).call(%1$s)).call(y) }\\\" % x.dump }\").call(x)) }").call("->(x) { eval(\"->(x) { \\\"->(y) { puts %s + \\\\\\\".call(nil)\\\\\\\" }\\\" % x.dump }\").call(eval(\"->(x) { \\\"->(y) { eval(eval(%1$s).call(%1$s)).call(y) }\\\" % x.dump }\").call(x)) }")).call(y) }.call(nil)
$ ruby quine.rb
->(y) { eval(eval("->(x) { eval(\"->(x) { \\\"->(y) { puts %s + \\\\\\\".call(nil)\\\\\\\" }\\\" % x.dump }\").call(eval(\"->(x) { \\\"->(y) { eval(eval(%1$s).call(%1$s)).call(y) }\\\" % x.dump }\").call(x)) }").call("->(x) { eval(\"->(x) { \\\"->(y) { puts %s + \\\\\\\".call(nil)\\\\\\\" }\\\" % x.dump }\").call(eval(\"->(x) { \\\"->(y) { eval(eval(%1$s).call(%1$s)).call(y) }\\\" % x.dump }\").call(x)) }")).call(y) }.call(nil)

*1:C 言語みたいに eval がない言語をイメージしている人は、自力で C インタプリタを書いてください。チューリング完全な言語なら eval が書けるはず。

*2:それぞれに同じ文字列を食わせた時、片方が文字列 s を出力するならもう片方も s を出力する。片方が無限ループに陥るならもう片方もなる。なお、同じ振る舞いをすればよくて、字面上一致している必要はないです。

*3:正確には「クリーネの再帰定理」じゃなくて「ロジャーズの不動点定理」らしい。

*4:本当はこの定義だとまずい。E(h, e) が停止しないので、p が定義できない。正確に議論するならイータ展開して、「入力文字列 x に対し、『入力文字列 y に対し、E(E(x, x), y) の結果を出力するプログラム』を出力するプログラム」と定義すべき。

*5:このプログラムは入力文字列を受け取りますが、使わずに捨てます。