型付き対称ラムダ計算の基礎理論
阪上紗里(指導教員：浅井健一)

はじめに

1

2.2

継続を扱うための新しい言語体系を定義したので、ここに報告する。継続とは「残りの計算」を表すものであり、現在着目している式の次の計算からプログラムの終わりまでの計算のことを言う。本稿ではこの継続を扱うための基礎体系として、Filinski の体系 [2] に基づいた型付き対称ラムダ計算 (Symmetric λ Calculus,SLC) を定式化した。この SLC により、項と継続を対等に扱うことが出来るようになった。次に継続を扱うための C オペレータを含んだ Felleisen の ΛC 計算 [1]を紹介し、今回定式化した SLC の中に ΛC 計算の埋め込みが可能であること、及びそれらの間の対応関係について言及する。

2

Call-by-value 対称ラムダ計算 (SLC)

2.1

Syntax と型

本研究の SLC(ここでは簡約が決定性のある Call-byvalue の Right-to-left 戦略に基づいたもの) を紹介する。まず Syntax と型について述べる。SLC の Syntax
は (項) と (関数) と (継続) で構成されることが特徴的である。

(値) v(項) e(関数) f(継続) c(値継続) k(型) T(項型) Te(関数型) Tf(継続型) Tc::= x | df e | n | [(y ⇐ c ↓ y) ↑ v]::= v | f ↑ e::= x ⇒ e | y ⇐ c | e | c::= k | c ↓ f::= y | bf c | •::= T → T 0 | T − T 0 | int::= +T
0→+T::= { +T¬T 0 →¬T0::= ¬T(値) は変数 x と、値として表すために d e でくくられた関数、および整数である n、そしてコンテキスト[(y ⇐ c ↓ y) ↑ v] で構成される。コンテキストについては後ほど説明する。最終的にプログラムは v のいずれかが返ってくる。(項) は値 v か、通常の関数呼び出し f ↑ e である。(関数) について説明する。まずx ⇒ e は通常の関数であり、e の中に現れる x を、受け取った項に置き換えた e を返すものである。同じように y ⇐ c は、継続側の関数ととらえることができ、c の中に現れる y を、受け取った継続に置き換えた cを返すものである。e は評価をすると関数になる項を表している。c は評価をすると関数になる継続を表している。(継続) は値継続 k と、 c を行う前に f を計算する c ↓ f である。(値継続) は継続側の値であり、変数 y と、値として表すために b c でくくられた関数、及び初期継続 (空の継続) を表す • で構成される。
T は 中立の型。 Te は項に対する型である。 Tc は継続に対する型で、¬T 0 とは T 0 型を受け取る継続の型を表す。Tf は関数型で、後ほど型規則のところでその特徴を述べる。

簡約規則

プログラムは途中 h c | e i 又は h c | f | e i という形で実行される。c はその時の継続、f は関数、e は項を表し、継続と項とが対称に現れていることがわかる。以下に簡約規則と簡約の挙動を簡単に説明する。

(begin)(pop)

e ; h•|eihc|f ↑ ei ; hc|f |ei(pushv ) h c | f | f 0 ↑ e i ; h c ↓ f | f 0 ↑ e i(exchv ) h c | e | v i(βv ) h c | x ⇒ e | v i; hc|x ⇒ x ↑ v|ei; h c | e[v/x] i(βv ) h c | y ⇐ c0 | v i ; h c0 [c/y] | v i(exchv ) h c | c0 | v i; h c0 | [(y ⇐ c ↓ y) ↑ v] i(context) h bf c | [(y ⇐ c ↓ y) ↑ v] i ; h c | f | v i(popv )
hc ↓ f |vi ; hc|f |vi(end )

h•|vi ; v

(begin) は計算したい項 e が与えられると、初期継続• のもとで計算を行うことを表している。冒頭に述べた簡約戦略に基づき、(pop) を用いて 3 つ組にし、項部分が v になるまで (pushv ) を使って関数を継続におしやる。3 つ組の項部分が v になると、関数部分によって簡約が進む。関数部分が e の場合 (exchv ) が適用され、まず e を先に計算したあとで v を適用させる (exch は exchange の略)。関数部分が x ⇒ e の場
合通常の関数呼び出し (β 簡約) が (βv ) によって行われる。関数部分が y ⇐ c の場合 (βv ) が適用され、現在の継続を関数部分に適用させた新たな継続が返る。
関数部分が c0 の場合 (exchv ) が適用され、後ほど適用したい c と v をパッケージ化した、Filinski がコンテキストと呼んでいるものに変換する。パッケージ化をせず h c0 | y ⇐ c ↓ y | v i のように変換すると、(βv )と (popv ) が適用されて元に戻ってしまう。コンテキストはこれを防ぎ、 c0 の継続部分を先に計算するようにしている。そして c0 が bf c に簡約されてはじめて、(context) により [ ] がはずれ c と v が適用される。実行中に h c ↓ f | v i のように２つ組の項部分がv になった場合は、(popv ) が適用され、継続から関数を関数部分に引き戻して簡約が進む。最終的にプログ
ラムは • に値が渡されることで、評価が終わることを(end ) が表している。簡約中に df e がでてきた場合、f としてよい。
2.3型規則型規則に関してはスペースの関係で省略するが、自然な型規則が与えられている。その中の関数型が特殊な形をしているので、ここで説明することにする。関→+T 0数型 Tf は { +T
¬T 0 →¬T で表される。これは +T 型の項を受け取って +T 0 型の項を返す関数の型 +T → +T 0と、¬T 0 型の継続を受け取って ¬T 型の継続を返す関数の型 ¬T 0 → ¬T を同時に表している。項側から見た場合は一般的な関数の型であることは理解できる。
例えば +T1 → +T２ 型をもつ関数 f は、+T1 型の項を +T2 型の項に変換し、その後に ¬T2 型を持つ継続に結果を返す。これを継続側からみた場合を考えよう。
例えば下の y ⇐ c のような ¬T2 → ¬T1 型を持つ関数 f は、継続側の関数適用である c ↓ f の型規則を見ると、¬T2 型の継続 c を ¬T1 型の継続、すなわちT１ を受け取るような継続に変換し、その後に +T1 型を持つ項を受け取る。以上のことから、関数 f は２つの型を併せ持つことがわかる。

Γ, y : ¬T2 ` c : ¬T1
1 →+T2Γ ` y ⇐ c : { +T¬T2 →¬T1

1 →+T2Γ ` f : { +T¬T2 →¬T1Γ ` c : ¬T2

Γ ` c ↓ f : ¬T1

SLC は さ ら に 型 付 き 言 語 の 基 本 的 性 質 で あ る
Progress と Preservation が成り立ことがわかっている。このことから SLC は継続を議論する上での土台としてふさわしい言語と言える。
この節で定式化した SLC が継続計算を議論・表現するのに適していることを示すため、次の節で単純型付き λ 計算に継続を扱うコントロールオペレータ C を追加した Felleisen の ΛC 計算を紹介し、その次の節では ΛC 計算が SLC に自然に埋め込めていることを示す。

3

Call-by-value ΛC 計算

3.1

SyntaxV::= x | λx. M | C(項) M(フレーム) F(評価文脈) E::= V | M M 0::= M [ ] | [ ] V::= [ ] | E[F ](値)3.2の関係が成り立つ。s1 ≈ s2 は s1 と s2 を実行するとどちらも同じ結果になることを表す。ここで ΛC 計
算における評価文脈である E が SLC の継続部分に対応し、ΛC 計算の redex を含んだ項 M が SLC の項部分に対応していることがわかる。私たちが意図した継続と項が明確に分かれて現れている。変換後の計算はh Tc [[E]] | Te [[M ]] i から行うこととする。
その他の変換規則は以下である。

Te [[x]] = x
Te [[λx. M ]] = dx ⇒ Te [[M ]]e
Te [[M N ]] = Tf [[M ]] ↑ Te [[N ]]Te [[C]] = dy ⇐ (• ↓ (x ⇒ x ↑ (d ⇐ ye)))e
Tf [[M ]] =Te [[M ]]Tc [[[ ]]] = •Tc [[E[F ]]] = Tc [[E]] ↓ TF [[F ]]TF [[M [ ]]] = Tf [[M ]]TF [[[ ] V ]] = x ⇒ (x ↑ Te [[V ]])(x : fresh)

コントロールオペレータ C の変換、 Te [[C]] について述べる。コントロールオペレータ C はそのときの継続を渡すものだが、Te [[C]] を変換すると、まずその時の継続が • によりリセットされ、その時の継続を y に渡すようにして、呼び出された際に関数に渡すように変換されている。このようにしてコントロールオペレー
タ C の挙動も変換できる。
これらの定義から、以下が成り立つことを示した。
補題 4.1 h • | Te [[E[M ]]] i ≈ h Tc [[E]] | Te [[M ]] i
これは E の構造に関する帰納法により証明できる。
定理 4.2 ΛC 計算の式 M の、一回簡約を M ; N と表すと、T [[M ]] ≈ T [[N ]] が成り立つ。
これは以下の代入補題を用いて証明できる。

簡約規則

補題 4.3 Te [[M ]][Te [[V ]]/x] = Te [[M [V /x]]](1) E[(λx. M ) V ] ; E[M [V /x]]E[C V ] ; V (λx. A (E[x]))(2)(1) の簡約規則は、通常の関数呼び出し (β 簡約) である。(2) がコントロールオペレータ C の挙動である。
これは継続を関数に変換し、それを V に渡すように表されている。その継続が実際に適用されると、 E[x]が実行された後、終了する。ここで A とは Abort のdefことで、A M 0 = C (λ . M 0 ) と定義され、それまでの継続を捨てて M 0 が返る。
これらに対して、自然な型規則が与えられているが、ここでは省略する。

4SLC への変換

4.1

変換規則

ΛC 計算でかかれたプログラムを SLC に変換するための変換規則 T を以下に定義する。
T [[E[M ]]] = h • | Te [[E[M ]]] i
SLC のプログラム E[M ] は変換後、初期継続のもとで計算されるように上の様に定義される。これは下に示す補題 4.1 により h • | Te [[E[M ]]] i ≈ h Tc [[E]] | Te [[M ]] i

代入補題は、M の構造に関する帰納法より証明できる。
以上により SLC に ΛC 計算を埋め込むことができる。

5

まとめ

本稿では継続を直感的に扱うための SLC の定義、 及び SLC への ΛC の埋め込みと、両者の対応関係について紹介した。紙面の都合で省略したが、本研究では非決定性の SLC を定式化し、その型付き言語としての基本的性質も証明している。さらに Call-by-value Leftto-right ΛC 計算の埋め込み、及び Call-by-name λµ計算の埋め込みを実現し、それぞれの対応関係も同様に示すことができている。今後は dual 計算との関連から論理学的観点からの見解を深めたい。

参考文献[1] Felleisen, M., and R. Hieb “The Revised Reporton the Syntactic Theories of Sequential Control and State,” Theoretical Computer Science,Vol. 103, No. 2, pp. 235–271 (September 1992).
[2] Filinski, A. “Declarative Continuations and Categorical Duality,” Master’s thesis, DIKU Report
89/11, University of Copenhagen (August 1989).