とあるラムダ計算の計算例
「型を値とする」ラムダ計算なのだが、普通のラムダ計算と違う記号を使うと、視認性が悪くなって目で追いかけるのが大変なので、次のようにする。
- 定数名、関数名は大文字の名前
- ラムダ変数名は小文字と数字の組み合わせ
- それ以外は普通の記法をそのまま使う。
- let式を使う。
- ひつだけ組み込みの演算子を持つ
組み込みの演算子は+だとして、単位元定数Eがあって、次を満たす。
- (x + y) + z = x + (y + z) （結合律）
- E + x = x + E = x （単位律）
- x + y = y + x （可換律）
- x + x = x （ベキ等律）
もともとは型の計算だったので、次のように変換するとそれらしくなる。
- 丸括弧(, )を<, >にする。
- 小文字λがいやなら大文字Λとする。
- ネーミング（大文字小文字の使い方とか）を変える。
- '+' を & に変える。
記法と計算方法
β変換は次の形で使う。
- (λ(x, y).X)(a, b) ⇒ let {x = a, y = b} in X
letの後のブロックはコンテキストと呼ぶ。letの入れ子は、コンテキストの合成でフラット化できる。共通の変数（束縛の左辺の名前）を持たないletの入れ子は、コンテキストの単純マージ（可換なマージ）でフラット化できる。
- let {x = a, y = b} in (let {z = c} in X) ⇒ let {x = a, y = b, z = c } in X
逆に、大きなコンテキストを分割して入れ子として扱ってもよい。
- let {x = a, y = b, z = c } in X ⇒ let {x = a} in (let {y = b, z = c} in X)
コンテキストのマージと分割は、簡単だが重要なテクニックである。
let A in (X + Y) は、(let A in X) + (let A in Y) と変形できるので、演算+に関してletは分配する。
let A in X の略記として、臨時に X/A を使うことにする。X/A/B は (X/A)/B 、つまり let B in (let A in X) の意味。略記 X/A を使うのは、let式の展開を遅延させる（後回しにする）ときである。+に対するletの分配法則は、(X + Y)/A = X/A + Y/A と書ける。
計算すべき式
計算すべき式は次のとおり。
let {
W = λ(w).WB,
FW = λ(f1, f2).(W(f1) + FWB),
BW = λ(b1, b2).(W(b1) + BWB),
LW = λ(l1, l2).(FW(l1, l2) + BW(l1, l2)),
TW = λ(t1, t2).(LW(t1, t2) + TWB)
} in TW(a1, a2)お尻がB（bodyのつもり）である名前（WB, FWB とか）は、それ以上は詮索しない式として扱う。
これを次のように分割しておく。
let {
W = λ(w).WB
}
in
let {
FW = λ(f1, f2).(W(f1) + FWB),
BW = λ(b1, b2).(W(b1) + BWB)
}
in
let {
LW = λ(l1, l2).(FW(l1, l2) + BW(l1, l2))
}
in
let {
TW = λ(t1, t2).(LW(t1, t2) + TWB)
}
in TW(a1, a2)この分割は計算しやすいように定めたが、名前 TW, LW, BW, FW, Wのあいだの参照関係をDAG（Directed Acyclic Graph）に描いたときのorderと関係する。
内側から外側への計算
計算すべき式の一番内側の、
let {
TW = λ(t1, t2).(LW(t1, t2) + TWB)
}
in TW(a1, a2)を計算してみる。
let式は構文的クロージャなので、コンテキストを使って式を展開（置換）する。すると、
(λ(t1, t2).(LW(t1, t2) + TWB))(a1, a2)
今後、適用が分かりにくいときは、明示的な適用演算子として中黒（・）を入れる。こうなる↓
(λ(t1, t2).(LW(t1, t2) + TWB))・(a1, a2)
適用はいったんlet式にするので、
let {t1 = a1, t2 = a2} in (LW(t1, t2) + TWB)再び、展開（置換）する。TWBへの置換は遅延させるので略記を使う。
LW(a1, a2) + TWB/{t1 = a1, t2 = a2}let式 → 適用 → let式 というところが回りくどいが、置換は必ず（構文的）クロージャの展開で起きるとしたほうがスッキリすると思う。
次は、
let {
LW = λ(l1, l2).(FW(l1, l2) + BW(l1, l2))
}
in
LW(a1, a2) + TWB/{t1 = a1, t2 = a2}の計算。クロージャの展開（置換）をして、
(λ(l1, l2).(FW(l1, l2) + BW(l1, l2)))・(a1, a2) + TWB/{t1 = a1, t2 = a2}let式に直して、
let {l1 = a1, l2 = a2} in (FW(l1, l2) + BW(l1, l2)) + TWB/{t1 = a1, t2 = a2}またクロージャ展開して、
FW(a1, a2) + BW(a1, a2) + TWB/{t1 = a1, t2 = a2}ここらへんで、最初に渡した実引数 (a1, a2) が順次“呼び出し先”に渡っていくのが理解できると思う。
次は、
let {
FW = λ(f1, f2).(W(f1) + FWB),
BW = λ(b1, b2).(W(b1) + BWB)
}
in
FW(a1, a2) + BW(a1, a2) + TWB/{t1 = a1, t2 = a2}クロージャ展開して、
(λ(f1, f2).(W(f1) + FWB))・(a1, a2) + (λ(b1, b2).(W(b1) + BWB))・(a1, a2) + TWB/{t1 = a1, t2 = a2}let式にして、
let {f1 = a1, f2 = a2} in (W(f1) + FWB)
+
let {b1 = a1, b2 = a2} in (W(b1) + BWB)
+
TWB/{t1 = a1, t2 = a2}let式を展開（置換）して、一部は後回し、
W(a1) + FWB/{f1 = a1, f2 = a2}
+
W(a1) + BWB/{b1 = a1, b2 = a2}
+
TWB/{t1 = a1, t2 = a2}演算+の結合律と交換律から
W(a1) + W(a1) + FWB/{f1 = a1, f2 = a2} + BWB/{b1 = a1, b2 = a2} + TWB/{t1 = a1, t2 = a2}演算+のベキ等律を使って、
W(a1) + FWB/{f1 = a1, f2 = a2} + BWB/{b1 = a1, b2 = a2} + TWB/{t1 = a1, t2 = a2}ベキ等律を使った変形は重要。
最後の計算、
let {
W = λ(w).WB
}
in
W(a1) + FWB/{f1 = a1, f2 = a2} + BWB/{b1 = a1, b2 = a2} + TWB/{t1 = a1, t2 = a2}これはもう結論書いてしまうと、
WB/{w = a1} + FWB/{f1 = a1, f2 = a2} + BWB/{b1 = a1, b2 = a2} + TWB/{t1 = a1, t2 = a2}略記をlet記法に戻すと、
let {w = a1} in WB
+
let {f1 = a1, f2 = a2}in FWB
+
let {b1 = a1, b2 = a2} in BWB
+
let {t1 = a1, t2 = a2} in TWB外側から内側への計算
let {
W = λ(w).WB
}
in
let {
FW = λ(f1, f2).(W(f1) + FWB),
BW = λ(b1, b2).(W(b1) + BWB)
}
in
let {
LW = λ(l1, l2).(FW(l1, l2) + BW(l1, l2))
}
in
let {
TW = λ(t1, t2).(LW(t1, t2) + TWB)
}
in TW(a1, a2)この式に出てくるlet式のコンテキストを、外から内へと折りたたんで小さくする計算法もあるのでやってみる。
まず、一番外側の W = λ(w).WB という束縛を、内側に展開して埋め込んでしまう。
let {
FW = λ(f1, f2).((λ(w).WB)・(f1) + FWB),
BW = λ(b1, b2).((λ(w).WB)・(b1) + BWB)
}
in
let {
LW = λ(l1, l2).(FW(l1, l2) + BW(l1, l2))
}
in
let {
TW = λ(t1, t2).(LW(t1, t2) + TWB)
}
in TW(a1, a2)この段階で中黒（・）で書かれている適用を展開（β変換）してもいいのだが、そのまま残して先にlet式を折りたたんでいく。
let {
LW = λ(l1, l2).
(
(λ(f1, f2).((λ(w).WB)・(f1) + FWB))・(l1, l2)
+
(λ(b1, b2).((λ(w).WB)・(b1) + BWB))・(l1, l2)
)
}
in
let {
TW = λ(t1, t2).(LW(t1, t2) + TWB)
}
in TW(a1, a2)さらに、
let {
TW = λ(t1, t2).
(
(λ(l1, l2).
(
(λ(f1, f2).((λ(w).WB)・(f1) + FWB))・(l1, l2)
+
(λ(b1, b2).((λ(w).WB)・(b1) + BWB))・(l1, l2)
)
)・(t1, t2)
+
TWB
)
}
in TW(a1, a2)ここで、ラムダ式によるTWの明示的な表現が得られた。TW = λ(t1, t2).K と置いたKを求めよう。Kは次の式。
(
(λ(l1, l2).
(
(λ(f1, f2).((λ(w).WB)・(f1) + FWB))・(l1, l2)
+
(λ(b1, b2).((λ(w).WB)・(b1) + BWB))・(l1, l2)
)
)・(t1, t2)
+
TWB
)内側の (λ(f1, f2).( (λ(w).WB )・(f1) + FWB))・(l1, l2) を計算すると、
(λ(f1, f2).((λ(w).WB)・(f1) + FWB))・(l1, l2)
⇒
let {f1 = l1, f2 = l2} in ((λ(w).WB)・(f1) + FWB)
⇒
((λ(w).WB)・(l1) + FWB/{f1 = l1, f2 = l2})
⇒
((let {w = l1} in WB) + FWB/{f1 = l1, f2 = l2})
⇒
WB/{w = l1} + FWB/{f1 = l1, f2 = l2}同様に、 (λ(b1, b2).( (λ(w).WB )・(b1) + BWB))・(l1, l2) は、
WB/{w = l1} + BWB/{b1 = l1, b2 = l2}その外側は、
(λ(l1, l2).
(
WB/{w = l1} + FWB/{f1 = l1, f2 = l2}
+
WB/{w = l1} + BWB/{b1 = l1, b2 = l2}
)
)・(t1, t2)置換やコンテキストの合成を端折ると、
(
WB/{w = t1} + FWB/{f1 = t1, f2 = t2}
+
WB/{w = t1} + BWB/{b1 = t1, b2 = t2}
)ベキ等律により、
WB/{w = t1} + FWB/{f1 = t1, f2 = t2} + BWB/{b1 = t1, b2 = t2}残っていた + TWB を足したものがKで、一番外側のラムダ抽象を元に戻した λ(t1, t2).K は、
λ(t1, t2).(
WB/{w = t1} + FWB/{f1 = t1, f2 = t2} + BWB/{b1 = t1, b2 = t2} + TWB
)(λ(t1, t2).K)・(a1, a2) を計算すると、
λ(t1, t2).K)・(a1, a2)
⇒
let {t1 = a1, t2 = a2} in K
⇒
let {t1 = a1, t2 = a2}
in
WB/{w = t1} + FWB/{f1 = t1, f2 = t2} + BWB/{b1 = t1, b2 = t2} + TWB
⇒
WB/{w = a1} + FWB/{f1 = a1, f2 = a2} + BWB/{b1 = a1, b2 = a2} + TWB/{t1 = a1, t2 = a2} 略記をlet記法に戻すと、
let {w = a1} in WB
+
let {f1 = a1, f2 = a2}in FWB
+
let {b1 = a1, b2 = a2} in BWB
+
let {t1 = a1, t2 = a2} in TWB
