読書会#2に行ってきました。

まぁ色々あったりして16:00くらい開始でした。

今日やった範囲

P.66 5.2.9 から P.71 5.3.5 まで。
P.72, P.73 は各自復習(何!?)するということで、めでたく Chap5 が終わった。
分からないとこなどは Google Group に書き込みをしましょう。

内容

5.2.9

factorial を作るところで補助的に出てきた項 g の中の if を test で書いたらどうなるの? という問題。

まぁ、素直に if then else を test に書き直せばいいんだけど、評価順序の違いによって答えの形式が違ってくるのが嫌なので abstraction でもってガードして最後にダミー変数を食わせましょう。という話。

5.2.10

0、1 とかの数値を Church 数に変換する churchnat という関数を作れ。という問題。

Church 数が再帰の構造をしているので、churchnat も再帰 (fix) を使って作れば OK。

5.2.11

pure lambda で実装された Church 数要素のリストの、全ての要素の和を求める関数を書け。という問題。

ここらへんを解いていると、Lisp で実装してる気分と同じになってくる。同じものなんだから当たり前か。

Representation

pure lambda の世界では Church 数の表現は色々有り得るけど、「振る舞い」だけ見たら全部一緒。
「iszro と問うたら tru と答えるのが c_0 だ。」みたいな感じ。これをダックタイピングと呼んでいいんだっけ??

んで、pure lambda term の集合をその「振る舞いを見れば一緒」という同値関係で割っておいて、普通の自然数の世界との対応を見ると、構造まで含めて一緒だよね。というのが最も言いたいこと。
こういうのは数学では「同型」と言ったりする。

5.3 Formalities

lambda term の meta-variable を使った定義は P.53 でもう扱ったんだけど、改めて集合の言葉で述べる話。
特に内容的には難しいところは無いが、meta-variable と variable の違いなどで感覚的に引っ掛かるようだ。
自分の感覚では meta-variable が 5.3.1 で出てくる (大文字の) T や V に相当する感じ。

5.3.2

Free Variable の定義。
素直なのですぐ理解できる。

5.3.3
FV(t) ≦ size(t) を示せ。という問題。

実は size は lambda term に対して厳密には定義されていないので、自分で上手く定義しなきゃいけないところ。

  • size(x) = 1
  • size(λx.t) = size(t) + 1
  • size(t_1 t_2) = size(t_1) + size(t_2)

これでいいだろう。

Substitution

β reduction で面倒な代入の話。
スコープを越えて変数が移動するため、気を付けないと意図しない変数解放や変数束縛が起きる。その様子を安直な代入の定義からちょっとずつ改善していく話の流れ。P.69 からスタートして P.71 の最後 5.3.5 で一応定義の完成を見る。微妙に残っているのは、変数束縛を避けるための α conversion (名前付け替え) が自然言語でしか定義されていないこと」

[x -> y](λx.x) では変数解放 (束縛変数 x が非束縛変数 y になってしまう) が起きたり、[x -> z](λz.x) では変数束縛 (非束縛変数 x が束縛変数 z になってしまう) が起きたり災難が続く。特に変数束縛を回避する手段として出ている「名前付け替え」がまたなんというか苦しい。α conversion を実装に落とすと、かなりその場対応色の強い実装になりそう。

ちなみに読書会で話題に出した Common Lisp で macro を定義するときの変数束縛を避ける gensym という関数について。使用例を On Lisp から取ろうとしたのですがほど良いサイズのものが無かったので、→Scheme:マクロ:CommonLispとの比較←この記事でも読んでください。

ではお休みなさい。

追記

振り返りの内容で分かんないとこがあったら、ここのコメント欄でも Google group の方でもいいので質問ください。かなりはしょって説明してる気がしてます。