難解な本
チャイティンの本を2冊持っています。「数学の限界」と「知の限界」です。いずれも難解です。というか、説明が不足しているように思います。なぜ、そうなるのか？中途の思考が省略されているのです。これらの本は講義録から文字お越しをしたようです。それが原因かもしれません、私が興味があるのはゲーデルの不完全性定理のLispによる証明です。この度、本を読みなおしつつ、他の人の解説も読み直しました。なんとなくわかったような気がしました。そのことを書き記そうと思います。
手抜きの証明器
チャイティンは本の中で(valid-proof? x)という関数について述べています。xはS式でありそれが証明可能ならその証明を返し、証明できないならnilを返すように思います。そうは説明していないのですが、多分そういうことです。でも、その具体的な実装はここでは必要ありません。
(defun valid-proof-p (x)
;; un implemented
)
すごく手抜きなコードです。？はLispの慣習に倣ってpとしました。
次に(is-unprovavle x)について考えてみます。これは前述の(valid-proof-p x)を利用します。「S式ｙが証明できないとは、すべてのS式に対して、(valid-proof? x)がｙと等価とは限らないという表現でよいのです。」とチャイティンは説明しています。どうせ手抜きですから、(valip-proof-p x)がnilを返さなければよいということにしてしまいます。
(defun unprovable-p (x) (not (valid-proof-p x)))
すごく手抜きです。大丈夫なのかな？
さらに本では(value-of x)という関数が必要とされています。これは説明からするとLispに古くからある(eval x)のことに思えます。そういうことにしてしまいましょう。
自己言及
「クレタ人はうそつきだ」とクレタ人は言った
これがアイディアの根本です。本では (value-of (('x) ('x)) )と表現されています。ここでxは関数です。関数に関数を適用させます。問題は一般的にLispにおいて関数の名前空間と大域変数の名前空間とは別だということです。関数に関数を食わせるにはfuncallを使わないといけません。
(funcall #'x #'x)
SchemeのようにファーストクラスのタイプのLispだと関数空間と変数空間が同一空間です。ですから
(eval '(x x))
と表せます。islispではこれができません。(funcall #'x #'x)で表現することにしましょう。
いよいよ核心
自己言及をするコードは証明不能と主張する関数gを定義してみます。チャイティンの作ったLispは極めて特殊です。
本のコードを読むもののさっぱりわかりません。どうもこういうことを言っているようです。
(defun g (x)
`(unprobable-p (funcall ,x ,x)))
関数gに関数gを適用するとどうなるのでしょうか？
> (funcall #'g #'g)
(UNPROBABLE-P (FUNCALL <function> <function>))
なぜ、クアジクオートを漬かるのでしょう？ (unprobable-p x)は未実装だから動作しませんからね。だからなのかな？
ところで(unprovbable-p )の引数着目します。これをevalしたらどうなるのかな？残念ながらこれはうまくいきません。funcallの引数のと表示されているものは、関数の実体です。これだとevalできません。仕方ありません、また、funcallを使うことにしましょう。
> (let ((f (funcall #'g #'g))) (funcall (elt (elt f 1) 1) (elt (elt f 1) 2)))
(UNPROBABLE-P (FUNCALL <function> <function>))
いよいよクライマックス
ここまでやるととっかかりがつかめてきました。上述の２つの結果を見比べてください。あらまあ、不思議、まったく同じですね。
> (funcall #'g #'g)
(UNPROBABLE-P (FUNCALL <function> <function>))
> (let ((f (funcall #'g #'g))) (funcall (elt (elt f 1) 1) (elt (elt f 1) 2)))
(UNPROBABLE-P (FUNCALL <function> <function>))
> (equal (funcall #'g #'g) (let ((f (funcall #'g #'g))) (funcall (elt (elt f 1) 1) (elt (elt f 1) 2))))
T
関数gは不動点関数となっています。計算は終わりません。これは何を意味しているのでしょう？
関数gは自己言及しているs式は証明不能であると主張しています。でも、これは不動点になっていて計算は終わりません。もしも証明不能だったとしてもそれを確認することができません。また、関数gの主張が間違っているとしても不動点になっていて計算は終わりません。関数gの主張が正しい、あるいは間違いのいずれであったとしても確かめようがありません。
ヘルプミー
このように書き連ねてきたものの、私はこれがチャイティンの言っていることを正しく再現しているのかどうか？自身がありません。これでいいのでしょうか？ どなたか助言をいただければ幸いです。
それにしてもLispで表したコードは不完全性定理の証明と言えるのでしょうか？ アイディアの概要を示してはいるものの、ゲーデルが行った厳密な証明とは異なるもののように思えてなりません。
どなたら助言をいただければ幸いです。
コードはここにあります。https://github.com/sasagawa888/eisl