Diary?
2009-02-20
Fri
(01:02)
というわけで、檜山セミナーの感想というか個人的なまとめをやってみる。何でこんな時間におっ始めるのかというと、明日仕事から帰ってくる頃には自分のノートが判読不能になって、ヒエログリフの解読作業から始めないといけなくなるから。
セミナーは前半戦と後半戦に分かれていて、前半戦では「大きなラムダ計算」と檜山さんが定義したラムダ計算のインフォーマルスタイルを入り口に、もうちょいフォーマルな（セミフォーマルな）ラムダ計算に変換する訓練と、「絵算」による幾何学的な操作によるラムダ計算の理解が主眼。後半戦はチューリングマシンの停止性問題の解説。
まずは前半戦の方だが、まずは大きなラムダ計算の定義。大きなラムダ計算では、ラムダ式を以下のように記述する。
<x, y | x + y> # 引数を二つ取り、両者を足し合わせるこのときのルールは
- 自由変数（引数リストにない変数）は使用できない
- ラムダ式自体を入れ子にすることはできない
の二つ。さらに以下の三つの規則は自明のものとして何の断りもなく使ってしまってよい。
α変換: <x|f(x)> = <y|f(y)> # 束縛変数の名前は取り替え可能
β簡約: <x|f(x)>(a) = f(a) # ぶっちゃけ関数適用だわな
η変換: <x|f(x)> = f # これもみたまんま蛇足ながら Python で書いてみようか。仮に関数の同値性が == 演算子でわかるとして（いやこれは不可能なんだけどね原理的に）、
lambda x: f(x) == lambda y: f(y)
(lambda x: f(x))(a) == f(a)
lambda x: f(x) == fちなみにセミナーでちょっと話のでた（ってか俺が話を振った） Io はちゃんとしたラムダ式の記法が無いので、上記のものでいうとβ変換にあたるものを直に記述できない。例えば以下の式の値は何になると思う?
method(x, x + 1)(2)答えは 3 じゃなくて 2 なんだこれが。とんでもない言語ですね。
話が大幅にずれたので軌道修正しよう。大きなラムダ計算のラムダ式の一例として、次のようなものを考える。
<x, y | 2 * x + y + 3>これをフォーマルな（小さな）ラムダ式に書き換えるとこうなる。
λx. λy. (A (A (M 2 x) y) 3)A は加算で M は乗算な。まあ S 式だと思えば。で、関数本体をフォーマルにするとかったるいので、セミフォーマルなラムダ式を使うことにする。
λx. λy. (2 * x + y + 3)何が違うんじゃと言われるかもしれないけど、フォーマル & セミフォーマルな方は引数の数が常に一つ以下になるよな。というかそれが本来のラムダ式で、インフォーマルな方はλx. λy. λz... というものを引数を複数受け付けて視覚・直観的にわかりやすくしているものと思っていいかも。というか実際のプログラミング言語のラムダ式って、ぶっちゃけ大きなラムダ式だよな普通。例えば Hakell の場合、ラムダ抽象は以下のどっちでもいい。
\x -> \y -> x + y
\ x y -> x + yこっから先は前のセミナーの内容が頭に入ってないとワケワカメかもしれない。まずは単純な例として、以下のような大きなラムダ式を考える。
f = <x, y| x + y>こいつのボディ部分をセミフォーマルな形式に変換してみよう。
f^ = <x|λy. (x + y)>もういっちょ。
f^^ = <|λx. λy. (x + y)>この ^ 記号は前回のセミナーで出てきた f^E の省略記法ね。それで ^ が増えれば増えるほどセミフォーマルな形式になっていくと。そしてこのλ.という定義に変換していくことを「ラムダ抽象」という。そして前回でてきた E で評価（Eval）すれば、
f(x, y) = E(f^(x), y) = E(E(f^^(), x), y)という事になる（実際には E の種類は複数あるけど、ここでは省略）。とりあえずラムダ抽象と式の評価についての理解はいいかな。それじゃ今回のセミナーの特徴だったと思う絵算について触れてみる。まずは次の図を見てくれ。
これは何かと言うとラムダ抽象の操作を図にしたもので、左の図は「x, y の二つの引数を f に渡して出力 f(x, y) を得る」様の図で、右の図は「実行エンジン E 経由に f^(x) と y を渡して以下略」な。そしてこの実行エンジンがなにをしくさっているのかが次の図だ。
これは檜山さんが「関数コードの実行エンジンEがズルすることが可能」と書いていた部分にあたると思う。おお、リアルワールドとスノーグローブの世界が地続きになった。
前半戦はこのあたりの事を実際に手を動かしてトレーニングしたりして、それで後は後半戦の停止性問題なわけだが、これ今まで見聞きした停止性問題の説明で一番わかりやすかったかな。以下の記述はいろいろ端折り気味だけど、大体のニュアンスはこんな感じだった。
まず最初に「プログラム」とは何かの定義から。コンピュータにおける一般的なプログラムとは、記憶装置上にロードされて実行され、記憶装置の次の状態を返す（状態遷移させる）ものだとする。いや、一切記憶装置の状態に影響を与えないプログラムもあるだろうけど、それは元の状態と同じ状態がたまたまプログラムの実行結果だったとしておく。
それで記憶装置の状態というのはメモリだろうがハードディスクだろうが単なるバイナリデータ、つまり 0 と 1 の羅列で、これは一意な数値として表現可能だ。そうなるとこの場合のプログラムの動作である「記憶装置の状態を変化させる」というものは、「数値を受け取って数値を返す関数」だと定義してよい。無限ループや例外の場合、記憶装置の状態は不定だ。
ここで停止性問題に切り込もう。ここで「関数のバイナリ表現とその引数を受け取り、その関数が停止するなら true を、無限ループや例外を起こす場合は false を返す」もの凄い関数「G」があると仮定する。
この仮定の元で、以下の関数を考えてみよう。
int f(int x) {
if (G(x, x)) {
while (true) {}
}
return 0;
}任意の数値に対して G を呼び、その結果が true であれば無限ループに陥り、そうでなければ 0 を返す関数なのだが、こいつの引数として「コンパイルされてバイナリデータ（=数値）になった f それ自身（f'）」を渡したらどうなるかな?
- G(f', f') が true の場合、 f(f') は停止するので f(f') は停止しない
- G(f', f') が false の場合、 f(f') は停止しないので f(f') は停止する
明らかにこれはおかしい。つまりこれは仮定が間違っており、つまりは G なんて存在しないということだ。そしてその一方で、このような関数が存在しないということを証明する事ができる。この「我々は決して知ることのできない事があるという事を知ることができ、それはとても不思議な事だ」というニュアンスの言葉が今回のセミナーの結論というか締めの言葉だったわけ。
……で、これと絵算がどう繋がるのか実はセミナーが終わった時点では今ひとつピンと来てなかったんだけど、その後にたけをさんに話を振ってみて返ってきたのが
たぶん、ラムダ抽象（f を f^ にする操作）が入ることでコード（関数）とデータ（値）が同じ整数/バイナリにエンコードできるようになって、その2つが一緒くたに扱えるようになったからパラドックスも発生するようになったってことですかね
という答えで、これと「実行エンジン E のズル」を合わせて考えると、何となく繋がりが見えてきた気がする。どんな観点から見てもスノーグローブとリアルワールドなどの入れ子世界同士がまったく同じ原理で動いている限りは実行エンジン E のズル = 上位層世界との接合が出てきてしまう。それでこのチューリングマシンの停止性問題に出てくるパラドックスというのは自己言及性というかメタ巡回性の問題（数学屋・論理屋じゃないのでこの辺の用語は適当）で、リアルワールドとスノーグローブの区別がつかない（メタ巡回）プログラム実行環境ではプログラムの停止性を汎用的に検出することは不可能（パラドックスに陥る）……何か書いてて怪しくなってきたけど、こんな氷原表現にしかならんなあ。
って、書いてるうちに 03:43 とか無茶苦茶な時間になっちまった。
(21:43)
いろいろ書こうと思ったが、何を書いても陳腐な文面にしかならなかったので今はただ R.I.P. とだけ。
