セミナーをやって良い点でもあり辛い点でもあるのは、終わった後で
- 「こういう説明ならもっと分かりやすかったのでは」
- 「あーいう順序で話すほうが合理的だった」
- 「あそこは省略すべきだった」
- 「駄洒落がスベッた」
- 「せっかく考えていたギャグを言い忘れた」
などなど、反省つうか後悔が、夏場（今、冬だけど）の入道雲のように湧き湧きしてくることです。
本人（檜山）はかなり強調しているつもりでも、それでもハッキリとは伝わらない事項がいくつかあったようです -- 別な機会（セミナー第1回も含め）で、檜山が何にこだわっているかを承知していれば話は別かもしれませんが。まーともかく、可能な限りアフターフォローします。
本エントリーは、「技術者／プログラマのためのラムダ計算、論理、圏」セミナーとなるべく独立に読めるようにしたつもりですが、次の資料をザッと眺めたほうがいいとは思います。
- http://www.chimaira.org/archive/slide20090124-6s.pdf
- http://www.chimaira.org/archive/slide20090219-6s.pdf
内容：
- あなたの隣にいる関数達
- 汎用コンピュータという関数
- リアルワールドのラムダ計算
- 計算のリアリティを心と身体で感じたい
あなたの隣にいる関数達
「強調したつもりでも必ずしも伝わってなかった事項」のひとつに関数概念があるでしょう。僕がなにげに「関数」と言ったら、プログラミング言語で書いたサブルーチンを意味していることはほとんどありません。僕やあなたが生きて暮らしているこの世界に、机や椅子や猫や植木と同等の資格で実在している計算機構／計算主体のことです。いや、机や椅子と一緒といっちゃうと言い過ぎかもしんないけど、理念的なモデル化作業を経れば、そこいらじゅうに関数がウジャウジャいるのは確かです*1。
計算するのは人間や計算機だけでありません。大気変動もDNAも量子現象も、計算機構を提供します。計算機構／計算現象があれば、そこに関数が在るのです。特に計算機（普通のコンピュータ）に注目しても、計算機の内部で動く関数を云々する前に、計算機そのもの（計算システム全体）を1個の関数とみなすことが先だと僕は思うのです。
さてまずは、Nは自然数（natural number）全体の集合、つまり N = {0, 1, 2, ... } とします。以下の対応で、ビット列と自然数は同じものだとみなします。
| ビット列 | 整数(2進数) | 整数(10進数) | 1引くと |
|---|---|---|---|
| '' | 1 | 1 | 0 |
| '0' | 10 | 2 | 1 |
| '1' | 11 | 3 | 2 |
| '00' | 100 | 4 | 3 |
| '01' | 101 | 5 | 4 |
| '10' | 110 | 6 | 5 |
| '11' | 111 | 7 | 6 |
コンピュータのメモリがいくらたくさんあっても、有限長のビット列を蓄えられるだけなので、いかなるメモリ状態も1個の自然数です。
ですから、プログラムの実行は、全メモリの初期状態aに対して、プログラムが走り終わった後の全メモリ状態bを対応させる関数 f(a) = b で表現できます。初期状態を変化させれば終状態もいろいろでしょうから、f:N→N なる自然数1引数関数がプログラムを表現します。
ただし、特定機械のメモリ状態（所詮は有限）の表現にすべての自然数を使う必要もないので、自然数の部分集合X（X⊆N）があって、f:X→N でもかまいません。そもそも、プログラムは例外で停止したり、無限走行することがあるので、NやX全体で値がキチンと定義されている保証は全然ありません。よって、プログラムを表現する関数は部分関数 -- 定義域全域で定義されているとは限らない関数です。僕のスライドでは、部分関数（全域関数を排除しません）を f:N⊃→N のような書き方をすることにしてますが、なんかメンドーなので今日は f:N→N で済ませます。
汎用コンピュータという関数
汎用コンピュータでは、1つの機械（ハードウェア）で色々なプログラムを動かすことができますから、色々な関数（計算可能な部分関数） f:N→N を色々な引数値（メモリの初期状態）で評価（実行）できるのです。そして、ここが重要なんだけど、その汎用コンピュータ自体も1つの関数で表現できるのです。
いま、汎用コンピュータを表す関数をmとしましょう。セミナーでは主にEと書いていたやつです。machineのmね。「mも普通の関数だよ」ってことで小文字にしてみました。現在のコンピュータでは、コード領域とデータ領域（コード以外の領域）にわけて*2、コード領域にプログラムコードをロードします。通常、コード領域はプログラム実行中に書き換えできません。この状況をモデル化して、mは、コード領域のメモリ初期状態（ロードされたプログラムそのもの）とデータ領域のメモリ初期状態の２つの引数を取るとします。
m(c, d) = r とは、「マシンmで、コードcをデータdに対して実行したら、結果がrだった」ということです。結果rは、コードc（ロードしたプログラム）が走り終わった後のデータ領域のメモリ状態です。コード領域は実行のあいだ不変です。
ここで、任意の関数f:N→N を登場させます。ちゃんと述べれば、fは計算可能な1引数部分関数です。くどいですが、関数fはまだコンピュータのなかにいるわけではなくて、あなたの隣にいたり、概念の世界に棲んでいるものです。リアルワールド（あるいはイデアルワールド）の関数fを、プログラミングしてコンパイルして出来たコードをφとします。ギリシャ文字を使ったことに他意はなくて、a←→α, f←→φ, s←→σ のような対応を取りたいだけです。
実行可能なコードφは、リアルワールド（あるいはイデアルワールド）の関数fを忠実に表現しているはずです。φはfからある手順により決まったものです。よって、ｆにハット^を付けた書き方 f^ も採用します。
φ = f^ が、リアルワールド（あるいはイデアルワールド）の関数fをマシンm上で再現するとは、
- f(x) = m(φ, x)
ということです。あるいは、
- f(x) = m(f^, x)
ちょっと注意： 正確に書くなら、f^ ではなくて f^() なんですが、「定数値関数と定数はしばしば同じものとみなす」原理を発動して、以下、f^() を f^ と略記します*3。
リアルワールドのラムダ計算
※ このセクションは、紙と鉛筆を持ちながら読むことを強くお奨めします。
等式 f(x) = m(f^, x) こそ、僕がこだわり続けて、「基本等式」とまで呼んだものです。基本等式を繰り返し使うと、マシンm（セミナー時口頭では実行エンジンE）を繰り返し使う状況も表現できて：
- g(x, y) = m(m(g^^, x), y)
などと書けます。このような入れ子の式だと、mが何度も登場して丸括弧が煩雑になります。そこで、mを中置演算子「・」で書いてもよいと約束して、括弧もできるだけ省略すると：
- f(x) = f^・x
- g(x, y) = (g^^・x)・y
- h(x, y, z) = ((h^^^・x)・y)・z
さらに括弧を少なくするために、(A・B)・C は A・B・C と書いてもいいとすると、
- f(x) = f^・x
- g(x, y) = g^^・x・y
- h(x, y, z) = h^^^・x・y・z
四則演算でも、一番よく使う演算は省略するという原則があって、掛け算 a×b は単に ab と書いてしまいます。同じ理由で A・B を AB（紛らわしいときは空白を入れて A B）と書いてしまうと、
- f(x) = f^ x
- g(x, y) = g^^ x y
- h(x, y, z) = h^^^ x y z
f, g, hなどの関数に、引数の個数分だけハットを付けたものを、対応する大文字で書くなら、
- f(x) = F x
- g(x, y) = G x y
- h(x, y, z) = H x y z
大文字のF, G, H の正体を確認するために、大きなラムダ計算（セミナー資料を参照）を遂行してみましょう。
F = f^
= Λ<x| f(x)>
= <| λx.f(x)>G = g^^
= Λ(Λ<x, y| g(x, y)>)
= Λ<x| λy.g(x, y)>
= <| λx.λy.g(x, y)>H = h^^^
= Λ(Λ(Λ<x, y, z| h(x, y, z)>))
= Λ(Λ<x, y| λz.h(x, y, z)>)
= Λ<x| λy.λz.h(x, y, z)>
= <| λx.λy.λz.h(x, y, z)>
実を言うと、f^ は f^() の略記だったので、今度はちゃんと () を付けてみると：
F = f^()
= <| λx.f(x)>()
= λx.f(x)G = g^^()
= <| λx.λy.g(x, y)>()
= λx.λy.g(x, y)H = h^^^()
= <| λx.λy.λz.h(x, y, z)>()
= λx.λy.λz.h(x, y, z)
F, G, Hにセミフォーマルな小さなラムダ式を代入して、先に出した等式（ドットは省略せずに残します）を再掲すると：
- f(x) = (λx.f(x))・x
- g(x, y) = (λx.λy.g(x, y))・x・y
- h(x, y, z) = (λx.λy.λz.h(x, y, z))・x・y・z
計算のリアリティを心と身体で感じたい
ここまでの話は確かにラムダ計算の説明になっています。基本等式 f(x) = (λx.f(x))・x は、左右をひっくりかえして等号を矢印にすれば、(λx.f(x))・x ⇒ f(x) なのでベータ変換です。しかし、しかしですね、これらは単に機械的な記号計算の手順ではないのです！ そもそも僕は今日このエントリーで、記号計算の話なんかコレッポッチもしてないですよね。f(x) = (λx.f(x))・x の左辺も右辺もリアルな関数のリアルな組み合わせで構成されています。ドットはマシンmの短縮記号だし、小文字λは、ハットの結果を（大きなラムダ計算内で）表すための表記法です。マシンmやハット^（ハットはときに大文字Λでも書く）は、単なる記号ではなくて、実在する関数や、関数に対して行う具体的なオペレーションです。
ラムダ計算の教科書やコースのほとんど（僕が知る限りすべて）は、ラムダ計算をまずは形式的な記号計算として導入します。記号計算に慣れれば、実在感も生まれる、と、そいういうスタンスですね。僕は「記号操作に慣れてから意味を考える」ことに挫折したので、最初から意味を持つリアルワールドからスタートしたかったのです。
僕のスタンスでは、ラムダ式は実在の直接的な記述であり、ラムダ計算は現に起きている現象に関する実際的な推論に使います。単なる記号ゲームではないのです。
もちろん、記号ゲームとしてのラムダ計算もあるわけですが、それは記号計算マシンの機械語だと思えばいいでしょ、ってことね。関数コードがビット列だろうが、中学生でもわかる数式だろうが、多少のトレーニングを要する記号表現だろうが、それは構文の違いに過ぎません。関数コード構文のバリエーションとして、実在する各種CPUの機械語とか、実在する各種プログラミング言語の構文とか、あるいは伝統的なラムダ式とかがあります、ってそれだけのことです。
教科書にあるラムダ構文／計算手法に一切触れないにしても、計算現象の法則としての f(x) = (λx.f(x))・x は至るところで観測できるわけです。僕が、記号ゲームとしてのラムダ計算を省略してもなお、法則としてのベータ変換を述べたかった、というのはこういう背景と動機です。
自然や社会の現象を扱うのに、なぜ抽象論を使うのでしょう？ 抽象論を何に使うのでしょう？ それはリアリティを記述するためであり、現にある具体物達をより良く理解するためです。
技術者／プログラマの多くは「関数」をプログラミング言語構文／実行機構のなかで理解していると思います。でもそれだけで閉じていると、実在や概念を直接的にモデル化する行為のなかで関数を使う発想につながりにくいかもしれません。みんなが生きていて、色があって動いているこの世界を、関数概念を使ってモデル化してみませんか。
