TaPL読書録 #5
今回は6章まるごと。
アルファ変換を許可する、というのは第5章で学んだが、しかし変数名が重複してるんだっけ？という疑念は常につきまとう。特に理論的な部分ではなく実装するという観点においては「標準の」の表現を定めておいたほうがいいとうことで デブルーイン ド・ブラウンの de Bruijn index という概念を導入してがんばるよ、という章である。
p.57
手法(4) の「明示的代入」とはなにか？がよくわからなかった。"explicit assignment" か？と思いググってみたがそれっぽいのが見つからず……( "explicit assignment lambda calculus" でぐぐった)。その場では放置したが後日論文から引けばいいのか、と思って著者から検索したら以下がヒット。 explicit substitution だったらしい。
http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-54.pdf
p.59
\w. y w -> \. 4 0 なのが初見殺しっぽい。ラムダ内なのでシフトが起きていて、名前付け文脈Τにおいて y = 3 なのに 4 になっている。
p.59 演習 6.1.5
ここの問題により「同じ名前がでてきても大丈夫であること」が確認できたとの声あり。
p.59 最終段落
[1 -> s](\. 2) の元になる de Bruijn index を用いない表現を考えられるか？という問題で僕が「これでしょ〜」って提示したのが間違ってて死亡。
提示したのは T: z => 2 という名前付け文脈における \x. -> x z だったのだけどこれはラムダ内に入るときにシフトが起きるので T: z => 1 における、 \x. -> x z が正しい(直後に書いてある)。
演習問題としてはやるだけが多かったのでさくさく進み、やるだけじゃないのが出てきたときはみんな「わからん」と言っていたのでアレだった。
さくっと答え合わせしたものを以下に書いておく
ex 6.2.3 -> スルーした
ex 6.2.6 -> 代入しても中でラムダができた場合との増減で相殺するからそうなるんじゃないの、とのこと
ex 6.2.8 -> スルー
ex 6.3.1 -> 「0があってもラムダがあるのでセーフ」という走り書きが残っている
ex 6.3.2 -> ラムダの数をLとした場合に de Bruijn index i と de Bruijn level l について l = L - i として変換すればﾖｻｿｳ
次回7章全部。7章の末尾には「実装したからといって、理解したとは限らない」という挑戦的な文言が載っていることに注意。
