Made with secret alien technology
(case '(What is alien technology?)
(はじめに '(これはLispについての個人的主張である。))
(language '(Lispがなぜ難解かというと、何をやっているか全く分からないから、これにつきる。なぜ括弧が大量に出てくるのか、lambdaとは何か、全く意味不明だ。Lispの歴史について書くと、まずLispは古い言語である。かつて人工知能の研究に使われたが、それはディープラーニングが登場するはるか以前の話である。大学に入っていきなりLispをやっても意味不明だろう。拒否反応を招くことから、Lispをやるのは変人と決まっているらしい。しかし、Lispは計算機科学と深い関わりがある。))
(lambda '(lambdaはラムダ式ともいう。ラムダ式はラムダ計算と関係がある。ラムダ計算によって帰納的関数が定義される。これはつまり、ラムダ式で再帰関数を書くと、計算可能な関数を定義できて、停止問題を一般化できるのだ。そういうわけで計算理論ではlambdaは非常に重要である。
なぜ再帰で計算可能性が定義できるか。直感的にはあらゆるプログラムはラムダ式で書ける。ところで帰納的関数はアルゴリズムそのものである。よって再帰で書けるプログラムは、計算可能なプログラムと同じになるのである。このあたりは、計算理論の本質である。))
(cardinality '(ここでいきなり連続体仮説の話になる。量子系と古典系の境界はどこにあるのか。その答えは、ヒルベルトプログラムにまで遡る。直観的にいえば、量子系はデジタルであり、古典系はアナログである。量子系を計算するということは、アナログからデジタルに変換することを意味する。この作業はユニタリ変換で計算できるが、不確定性原理により全てを同時に知ることはできない。この疑似アナログ=デジタル変換は連続体仮説と関係がある。
チューリング機械の停止問題の証明には、対角線論法が使われるが、濃度の問題はもっと深い、根源的な問題がある。つまり量子系はデジタルで、古典系がアナログなら、両者の濃度は等しいのか、という問題だ。
仮に宇宙が量子コンピューターであり、計算可能であり、チューリング完全だとしよう。そうであるなら、宇宙というチューリング機械のプログラムの濃度は、自然数の濃度と等しくなければならない。しかし、われわれの宇宙は古典系であり、その濃度は実数と等しいはずである。ところで連続体仮説から、両者の濃度の間には別の濃度は存在せず、これ以上の考察は不可能である。(なぜなら、連続体仮説は証明も反証もできないから)
結論としては、量子系と古典系には埋め難い溝があり、両者を統合するのは不可能ということになる。量子重力理論にしろ、量子コンピューターにしろ、両者の溝を埋めることのできない、不完全なものでしかないだろう。結局、この宇宙がそのようにできているからという、不可知論を結論とする他ない。1963年に連続体仮説がZFC独立であると証明されたときから、現在の数学の枠組みでは統合は不可能だ。もし可能性があるとすれば、ZFCとは全く異なる、別の数学体系が必要になる。望みは極めて薄い、としかいえない。))
(本題 '(無慈悲な現実からは目をそらし、Lispの世界に戻ることにする。コードの例を挙げてみよう。ゲーデルの不完全性定理の証明である。これは停止問題に置き換えることができる。コードを書くと、
(g g)
expression (g g)
value (is-unprovable (value-of ((' (lambda (x) ((' (lamb
da (L) (L is-unprovable (L value-of (L (L ' x) (L
' x)))))) (' (lambda (x y) (cons x (cons y nil))))
))) (' (lambda (x) ((' (lambda (L) (L is-unprovabl
e (L value-of (L (L ' x) (L ' x)))))) (' (lambda (
x y) (cons x (cons y nil))))))))))
こんな感じである。なぜ一部だけかというと、これはチャイティンの著書からの引用だからだ。引用はいろいろと面倒なルールがあって、本人の許可など当然取ってないので、どこまでが許容範囲か不明である。削除されてはたまらないので、調子にのって全文引用などは怖くてできない。しかし、自分でコードを書いても、他人のコードの書き直しにすぎないし、全く面白くない。
ゲーデルの対角線論法が、この短いコードで証明できるというので十分な気がするが、ここは別の証明も挙げておく。
厳密性を犠牲にして、強引に書けば、β簡約が非正規であれば反例になる。つまり、
(λx.xx)(λx.xx) → (λx.xx)(λx.xx) → …
である。一行で書けてしまった。
不完全性定理の証明が、たったこれだけのコードで書ける。Lispにいかれる連中の気持ちが分かろうというものだ。もっと再帰を使いたかったが、大量の括弧で読者を威嚇するのはまたの機会に。)))
これで終わるはずだったが、不完全性定理の証明の概略を書くことにする。計算機科学の停止問題の証明を利用する。Lispならdefunを使うのだろうが、日本語のままでも書ける。まず関数「この関数は停止しない()」を定義する。「停止する」というのは、ある入力に対して関数を実行すれば、プログラムの実行が停止するという意味である。この関数は入力がYESなら停止せず、入力がNOなら停止するとする。ここで、関数「この関数は停止しない()」自身をこの関数に入力する。仮にこの関数が停止したとすれば実行結果は、
この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(この関数は停止しない(
……))))))))))))))))))))))))))))))
となり、停止しない。つまりこの関数が停止するとすれば停止せず、停止しないとすれば関数の定義より停止する。これは矛盾である。以上が停止問題の証明だが、これにゲーデル数を導入すれば第一不完全性定理が証明できる。さらに記号を使わずに書けば、
この関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数のこの関数は関数の入力がNOなら停止するという関数の
……以下無限に続く……実行結果の実行結果の実行結果の実行結果の実行結果の実行結果の実行結果の実行結果の実行結果の実行結果……
となり無限に続いて停止しない。自己言及を利用した命題には全て応用できるので、
この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(この文章は必ず終わらない(
……))))))))))
というような応用も可能である。以上は完全に余談であるが、Lispを利用した文体実験としては面白いだろう。