あおむけマカロニ - oto-oto-oto’s diary

えらく時間がたってしまったが、1月24日、「技術者／プログラマのためのラムダ計算、論理、圏」セミナーに行ってきた。

で、自分なりにわかったこと、わからなかったことをメモしてみる。
ウソ、間違いがあるはずなので、ご指摘いただけると大変ありがたいです。

関数

関数: ブラックボックス、抽象的な「存在」
ラムダ式: 関数の実装(の詳細)=ソースコード、具体的な「存在」
E: ラムダ式のコンパイラ? インタプリタ? ラムダ式(と実引数)を放り込んだら、抽象的な存在であるところの関数と同じように働きだすもの。

というイメージを持った。

f^という書きかた

f(x, y) <-> E(f^(x), y)

という対応で、f^の定義とする。実にいい加減な理解だ。<->は上に書いた「同じように働きだす」の意味で。やかましく言わないならイコールと思っていいのかもしれない。
これを見ると、f^はfと第一引数をまとめてコンパイルしたようなものに見える。f^をfのコード化という。
第一引数だけじゃなくて、2個まとめてとか、1つも取らずにとかでコード化するといったことも考えられて、その場合は当然、Eが違ったものになる。
Eが1種類のみなら、f^がデータとしての関数として一意になりそう。ちょっと気持ちいい。

質問し損ねたこと

セミナーの最後のほうで書いた、足し算関数を「三重丸の+ → 三重線 → E → 二重線 → E → 一本線」とあらわした図(ああわかりにくい)で2箇所出てくるEは同じものなのか？
関係ないかもしれないけど、「evalは何でも返し得るから型推論できねー」ってトーク@Ruby会議2008を思い出した。

大きなラムダ式

インフォーマルなラムダ。
自由変数なし、入れ子原則禁止。

<x, y|x + y>

こんな感じに書く。

アルファ規則 <x|f(x)>  = <y|f(y)>
ベータ規則   <x|f(x)>a = f(a)
イータ規則   <x|f(x)>  = f

ベータ規則って、計算の定義だよなぁ。この日のセミナーでは、関数はやるけど計算はやらないという話だったけどちょっと逸脱。
で、イータ規則。意味的には「引数xを取ってf(x)を返す関数はf」で、あたりまえのことを言っている。

質問し損ねたこと

イータ規則の左辺は(大きな)ラムダで、右辺は関数そのもの。ラムダ(実装)と関数(ブラックボックス)は一応別のものと思うんじゃなかったっけ？インフォーマルなので気にしない？
と疑問に思ったんだけど、今資料みたらちゃんと書いてあった。

しばしば、大きなラムダ式と関数そのものが同一視される（区別しなくなる）

ふむふむ。

スノーグローブ

恥ずかしながら、あまりわからなかったです。
小さいラムダは機械への命令で、大きいラムダは人間への命令であるといった、誰(何)が実行するのかという点を今まであまり意識したことがなかったあたりが分からない原因かな?

以下、思ったけどまとまらないのを適当に。

スノーグローブ現象は計算機をからめて語られていたけど、純粋数学的にもでも起こるようなことなのか。
型
ラムダ計算というものを考える動機。数学でも必要になってくるものなのか。
関数の存在。f(x): xが有理数なら1、無理数なら0。といったものはラムダであらわせなさそう。そういうものは関数として存在してるといっていいか。直感主義？

ラムダが関数のデータ化という見方や、データとしての関数と実行エンジンの対で考えるというのは新鮮だった。参加してよかった。

とっ散らかったメモだけど、参加した証拠として書いてみた。
今回はあまり絵も書けなかったし、自然演繹とデカルト閉圏の話も興味あるので次があればまた行きたいです。
id:m-hiyamaさん、ありがとうございました。