TAPL (1)

Types and Programming Languages (The MIT Press)

型無しλ計算の部分(7章まで)は、大筋は理解出来たと思う。Church数と戯れてみたり。call-by-nameやcall-by-value等のevaluation戦略は実はλ計算の用語だったんですね。初めて知った。

de Bruijn式表記を採り入れる事で発生する"shift"という操作が最初分からなくて苦労したけど、要はbound & free variableのstructureを保存したままreductionを行う為に必要なだけだと気づくまでに時間がかかった。そう書いてあるんですけどね、馬鹿なんですよ...。次は型付きλ計算。