日記 (2020 年 7 月 6 日)
7 月 5 日では、 継続を扱えるように拡張された λc-計算について軽く触れた。
ここで、 λc-計算の簡約規則を思い出そう。
簡約規則は (もともとのラムダ計算に定まっていたものを含めて) 3 種類あり、 評価環境 E と項 M と値 V に対し、
E[(λx.M)V] ⇝ E[M[x:=V]] E[abortM] ⇝ M E[contM] ⇝ M(λx.abortE[x])♤
と定まっていた。
このうち最初の規則は評価環境 E の内側だけの書き換えで済んでいるが、 残りの 2 つの規則は項全体を書き換える必要がある。
このような局所的な書き換えだけでは実現できない簡約規則は、 しばしば簡約の分析を難しくする。
そこで、 できるだけ局所的な書き換え規則だけを用いて、 上と同じ振る舞いが実現できれば便利である。
今日は、 この問題について触れていこうと思う。
これから定める新しい規則と区別するため、 これまでの簡約は単に ⇝ ではなく ⇝G と書くことにする。
まずは abort について考察する。
E[abortM] という項を考え、 E は空でないとする。
このとき、 abortM は、 ある項 N について (abortM)N の形で現れるか、 ある値 V について V(abortM) の形で現れるかどちらかである。
初めに、 前者の (abortM)N の形で現れる場合を考えよう。
今の目的は、 局所的に (abortM)N という形の項を何か別の項に書き換えるという規則を作り、 式 ♤ と同じ振る舞いを実現することである。
式 ♤ を見ても分かるように、 abortM はその外側にある評価環境を完全に破棄する役割がある。
したがって、 (abortM)N において abortM の外側にある N は破棄されるべきである。
そこで、 局所的に、
(abortM)N⊳LrabortM
という書き換えを行えばうまくいきそうだと考えられる。
後者の V(abortM) の形で現れる場合も、 同様に考えて、 abortM の外側にある V を破棄して、
V(abortM)⊳LrabortM
とすれば良さそうである。
これら 2 つの規則を次々と適用していけば、 E[abortM] という項は、 E に相当する部分が全て破棄されて単に abortM に書き換えられる。
そこで、
abortM⊳LoM
という書き換えを最後に行うことにすれば、 式 ♤ が再現できる。
ここで注意すべき点として、 最初の 2 つの書き換え (⊳Lr で書いた) はある大きな項の内部の書き換えだが、 最後のこの書き換え (⊳Lo で書いた) は項全体が abortM という形になって初めて適用されなけれならない。
つまり、 大きな項の真の部分項として現れる abortM に対して ⊳Lo を適用して M に置き換えてはいけない。
次に cont について考察する。
前と同様に、 ある項 N について (contM)N の形で現れる場合と、 ある値 V について V(contM) の形で現れる場合を考える。
前者の (contM)N の形について考察する。
abort の場合を踏まえると、 うまい X をとってこれを contX という形に局所的に書き換えるという規則を定めれば、 この書き換えが次々と伝播して目的が達成されることが期待できる。
そこで、 この X として何が適切かを考えることにする。
我々の目標は (contM)N を contX に局所的に書き換えることで式 ♤ をシミュレートすることであったから、 任意の評価環境 E のもとで、 E[(contM)N] と E[contX] は ⇝G によって同じ項に簡約されるべきである。
定義から、
E[(contM)N] ⇝G M(λx.abortE[xN]) E[contX] ⇝G X(λx.abortE[x])
であるから、
X(λx.abortE[x])=M(λx.abortE[xN])
となるように X を定めれば良さそうである。
まず X は継続関数を引数として受け取る関数であるから、 ラムダ抽象で始めるとするのが自然である。
したがって、 X≡λk.X として、 X をうまく定義することを考える。
k には λx.abortE[x] が渡されるので、 k(xN) という項を考えれば abortE[xN] という形の項が得られる。
目標は M(λx.abortE[xN]) という形であったが、 これは X≡M(λx.k(xN)) とすれば実現できる。
以上の観察により、 局所的に、
(contM)N⊳Lrcont(λk.M(λx.k(xN)))
という書き換えをすれば良さそうであることが分かった。
後者の V(contM) の場合も、 同様にして、
V(contM)⊳Lrcont(λk.M(λx.k(Vx)))
という規則が考えられる。
これら 2 つの規則を次々と適用していけば、 E[contM] という項は、 ある項 X について contX という形に書き換えられる。
そこで、
contX⊳LoX(λx.abortx)
という書き換えを最後に行えば、 式 ♤ が再現できる。
この規則も前と同様に、 部分式の書き換えの最後のみで行わなければならないことには注意すべきである。
これにより、 式 ♤ を再現しそうな局所的な書き換え規則が得られた。
この規則の厳密な定義を書き下す前に、 まずは 「局所的に書き換える」 とはどのような意味なのかを明確にするため、 以下の用語を用意する。
定義 2.1.
計算体系 λc の項の上の関係 ⊳ に対し、 同じく項の上の関係 ⇝ を次を満たす最小の関係として定める。
すなわち、 項 M,N,P に対し、
M⊳N ⟹ M⇝N M⇝N ⟹ λx.M⇝λx.N M⇝N ⟹ MP⇝NP M⇝N ⟹ PM⇝PN M⇝N ⟹ abortM⇝abortN M⇝N ⟹ contM⇝contN
が成り立つ。
このとき、 ⇝ を ⊳ の 「合同閉包 (congruent closure)」 という。
以上のもと、 次のような書き換え規則が定義できる。
定義 2.2.
計算体系 λc の項の上の関係 ⊳Lr を、 項 M,N と値 V に対し、
(λx.M)V ⊳Lr M[x:=V] (abortM)N ⊳Lr abortM V(abortM) ⊳Lr abortM (contM)N ⊳Lr cont(λk.M(λx.k(xN))) V(contM) ⊳Lr cont(λk.M(λx.k(Vx)))
で定める。
さらに、 関係 ⊳Lo を、 項 M に対し、
abortM ⊳Lo M contM ⊳Lo M(λx.abortx)
で定める。
最後に、 関係 ⇝L を、 ⊳Lr の合同閉包と ⊳Lo 自身の合併として定める。
この関係は、 最初に意図していた以下の性質を満たす。
定理 2.3.
計算体系 λc の任意の項 P,Q に対し、 P⇝GQ ならば P⇝L∗Q が成り立つ。
証明.
⇝G の定義により、 ある評価環境 E について、 P は E[(λx.M)V] か E[abortM] か E[contM] の形である。
この E のサイズに関する帰納法によって、 定理の主張を示す。
E≡[] の場合は明らかであるから、 以下では E≢[] の場合を考える。
このとき、 ある評価環境 E が存在して、 ある項 N について E≡E[[]N] であるか、 ある値 V について E≡E[V[]] である。
E≡E[[]N] かつ P≡E[contM] の場合を考える。
このとき、
Q≡M(λx.abortE[x])
である。
また、
P ≡ E[(contM)N] ⇝L E[cont(λk.M(λx.k(+xN)))]♡
が成り立つ。
ところで、
E[cont(λk.M(λx.k(xN)))]⇝G(λk.M(λx.k(xN)))(λy.abortE[y])
であるから、 帰納法の仮定によって、 この簡約は ⇝L を複数ステップ行うことでも可能である。
したがって、 簡約 ♡ の続きは、
⋯ ⇝L∗ (λk.M(λx.k(xN)))(λy.abortE[y]) ⇝L M(λx.(λy.abortE[y])(xN)) ⇝L M(λx.abortE[xN]) ≡ Q
となり、 P⇝L∗Q が示された。
それ以外の場合も同様である。
追記 (2020 年 7 月 7 日)
合同閉包の厳密な定義を追加した。
また、 局所的な置き換えと全体の置き換えの違いを明確にするため、 記号を変えてそれぞれ ⊳ と ⇝ で表すことにした。
参考文献
- M. Felleisen et al (1987) 「A syntactic theory of sequential control」 『Theoretical Computer Science』 52(3):205–237