セミナー当日、質問に答える時間が取れず大変申し訳なかったので、ここで答えます。（[追記 date="2009-02-02"]写真入れた。[/追記]
関数は確かに抽象的ですが、「いま目の前にある」とか「隣の椅子に座っている」と考えてください。もっと抽象度の高いものがウジャウジャ出てくるので、関数はリアルでファミリアーなんだと思わないと、雲をつかむような感覚になってしまいますからね。
（小さな）ラムダ式はソースコードじゃなくて、むしろオブジェクトコードと考えてください。記号計算機械の機械語です。機械が十分高水準なんで、機械語も人間可読ですが、ソースコードじゃありません。強いて言えば、ソースコードは大きなラムダ式のほうです。
Eはインタプリタ＝実行（評価）エンジン＝機械です。Eに食わせる機械語コードがf^(a)とかf^()です。関数f^は確かにオブジェクトコードを吐きますが、ラムダ抽象化オペレータがよりコンパイラに近いでしょう。ラムダ抽象化オペレータは次回の話題です。
- f(x, y) <-> E(f^(x), y)
<->は上に書いた「同じように働きだす」の意味で。やかましく言わないならイコールと思っていいのかもしれない。
関数のイコールは色々ありますが、ブラックボックスと捉えるなら、同じ入力に同じ結果を返すならイコールです。仮に内部構造が見えていて構造が違っていても、入出力が同じならイコールです。
これを見ると、f^はfと第一引数をまとめてコンパイルしたようなものに見える。f^をfのコード化という。
はい、そうです。f^に引数が残っていれば、残った引数全部に具体値を渡せばオブジェクトコードが出てきます。
Eが1種類のみなら、f^がデータとしての関数として一意になりそう。ちょっと気持ちいい。
無数のEが存在しますが、通常は、Eを一つ選んで固定して話をします。
セミナーの最後のほうで書いた、足し算関数を「三重丸の+ → 三重線 → E → 二重線 → E → 一本線」とあらわした図(ああわかりにくい)で2箇所出てくるEは同じものなのか？
役割としては同じですが、型（プロファイル）まで考えるちょっとだけ違います。以下、整数をZと書いて、足し算をsと書きます。s:Z, Z → Z が足し算関数のプロファイルです；その意味は「整数2引数で戻り値も整数」。このとき、s^ = <x | λy.s(x, y)>, s^^ = <| λx.λy.s(x, y)> で、それぞれのプロファイルは s^:Z → ZZ, s^^: I → (ZZ)Z （Iはユニット型）です。指数で表したデータ型はso-called「関数型」ですが、我々の文脈（計算機のハナシ）では、「関数コードの型」です。
2つのEを、E1, E2と区別すると；
- E1(s^^(), a) = s^(a)
- E2(s^(a), b) = s(a, b)
ですから、E1とE2のプロファイルは：
- E1: (ZZ)Z, Z → ZZ
- E2: ZZ, Z → Z
ですね。オダンゴを囲む丸はλに対応し（三重丸は2回λされています）、線の本数で後から渡すべき引数の個数がわかります。是非、絵を描いて考えてみてください（「簡略オダンゴ図」も多少は参考になるか？）。オダンゴ図のちゃんとした説明と練習は次回のネタです。
[インフォーマルなラムダ計算の計算規則は]あたりまえのことを言っている。
どうしようもなく「あたりまえ」なのです。この自明な規則をフォーマルなラムダ計算でも再現するようにします。経験と直感から自明な事実を、人為的に計算機構を構成するさいの指導原理にするわけです。
イータ規則の左辺は(大きな)ラムダで、右辺は関数そのもの。ラムダ(実装)と関数(ブラックボックス)は一応別のものと思うんじゃなかったっけ？インフォーマルなので気にしない？
小さなラムダ式と関数は別物です。完全に区別してください。しかし、大きなラムダ式と（あなたの目の前にいる）関数は同一視することがあります。
小さいラムダは機械への命令で、大きいラムダは人間への命令であるといった、誰(何)が実行するのかという点を今まであまり意識したことがなかったあたりが分からない原因かな?
小さいラムダ式は機械への命令と解釈していいです。大きいラムダ式は、人間が実在や現象を記述するために使うと思ってください。もちろん、大きいラムダ式は、人間が行う計算と推論の道具に使えます。
スノーグローブ現象は計算機をからめて語られていたけど、純粋数学的にもでも起こるようなことなのか。
今回は、計算機と計算現象を素材にしました。が、数学でも論理でも物理でも至るところに出現します。圏論的には、モノイド積とその随伴関手（指数）を扱っているので、論理の演繹定理、（古典的であれ現代的であれ）テンソル計算、結び目理論のライデマイスター移動やその拡張、量子テレポーテーションなども同様な現象として括れます。
ラムダ計算というものを考える動機。数学でも必要になってくるものなのか。
計算技法として使うのはインフォーマルラムダ計算のほうでしょう。例えば：
ただし、上で述べたような、モノイド閉圏の典型例としての意義は大きいと思います。また、バエズによると（間接伝聞）、2002年フィールズ賞受賞者のウラジーミル・ヴォエヴォドスキー(Vladimir Voevodsky）が、ホモトピー・ラムダ計算（the homotopy lambda calculus）なるものを作り始めているそうです。
関数の存在。f(x): xが有理数なら1、無理数なら0。といったものはラムダであらわせなさそう。そういうものは関数として存在してるといっていいか。直感主義？
古典的（古くさいという意味ではない！）立場では、有理数／無理数の判別も関数です。（「直感」じゃなくて）直観主義だと、有理数／無理数の判別は関数とは認めないかも知れません。僕が想定したのは計算可能な関数だけです。しかし、任意の関数を許しても、特に議論は変わりません。古典的な集合／関数概念を用いて作った集合圏も、デカルト閉圏の例ですから。
