対称ラムダ計算の定式化
理学専攻情報科学コース

新井祐美（指導教員：浅井健一）

1 はじめにΓg ∪ {g : A ⊃ B} ` g : A ⊃ B

継続とは，計算のある時点における残りの計算を表す．対称ラムダ計算 (Symmetric Lambda Calculus，以下 SLC) とは，項と継続が対称になっており，項を扱うのと同様に継続を扱うことができる計算体系である．
1989 年に Filinski によって初めて提唱され [1]，阪上らによって small-step semantics で定式化し直された [2]．
また，上田ら [3] によって，種々の性質が示されつつある．本稿では，これまでに示されてきた SLC の性質の正しさを裏付けする一手法として，定理証明系 Coqによる定式化を試みている．
具体的には，上田らによる非決定性 SLC の syntax，types，typing rule，reduction rule を Coq で定義し，型付きの言語が正当であるために必要な性質の１つである
preservation の証明を定式化した．次に，call-by-value
SLC の停止性を示すため，値，項，関数，継続のそれぞれが停止するという論理述語を定義し，論理関係の手法によるこの証明が Coq によって定式化可能であるかを検証している．

2 非決定性 SLC
本稿で定式化した非決定性 SLC について述べる．

2.1 Syntax
項関数
継続
項のパターン
継続のパターン

efc
pq

FFFF
F

n | x | e ↑ f |d f eg | p ⇒ e |c ⇐ q | e | c• | y | f ↓ c | bfc
x | dgey | bgc

SLC では項，関数，継続の３つを組み合わせて計算状態を表しており，それらは相互に再帰する構造になっている．項についての λ 抽象を表す p ⇒ e，継続についての λ 抽象を表す c ⇐ q に現れる p, q は束縛変数に相当し，項（継続）型の変数または項（継続）として扱う関数型の変数になる．
本稿では，まず p, q をデータ型として定義し，それを用いて e, f, c を相互再帰させる形で定義している．
2.2

TypesTA, BF||
F+A
(types of expressions e)
A ⊃ B (types of functions f )¬B(types of continuations c)⊥ | > | int | A ∧ B | A ∨ B | A → B | A − B

SLC では，型も e, f, c それぞれについて定義されている．A, B は neutral type とし，３つの型をより細分化する．例えば，項として扱う関数 d f e は，型規則によると +(A → B) のように表される．本稿では，e, f, cの型と neutral type を互いに相互再帰するデータ型として定義し，次に述べる型規則を，項型・関数型・継続型が相互再帰する，Prop 型を返す述語として定義した．
2.3

Typing rule

本稿で定式化した SLC の型規則を一部抜粋する．

Γ x ∪ {x : +A} ` x : +ATVarΓ ` x x : +A Γ ` e : +B
TFun1
Γx ` x ⇐ e : A ⊃ B

TFVar

Γy ∪ {y : ¬B} ` y : ¬B TVarΓ ` c : ¬AΓ `y y : ¬BΓy ` c ⇒ y : A ⊃ B

TFun1

Γ ` e : +A Γ ` f : A ⊃ B
Γ ` f : A ⊃ B Γ ` c : ¬BTApp
TAppΓ ` e ↑ f : +BΓ ` c ↓ f : ¬B` e : +A c : ¬A
TProg1` he | ci` e : +A

` f : A ⊃ B c : ¬B
TProg2` he | f | ci

型付け規則も項と継続が対称形を成すように定義されている．ある SLC 式に型がつくということは，それを構成する e, f, c すべてに型がつくということで表現される．
SLC では，環境は上記のように１つであり，Γ には項，関数，継続すべての変数が定義されているが，Coqによる定式化にあたり，環境は項，関数，継続それぞれについて１つずつ用意した．これにより定式化の複雑さが緩和されている．なお，本稿において Γ x の表
記は，環境の中から x の束縛を除いてあることを意味する．また，2.5 節に記した各種の定理・補題の証明を定式化する際，簡約等の操作の前後における環境の中身を比較する必要があったため，変数は EVar（項の変数を表す）等のタグを付けた自然数で表し，昇順になるように定義している．

2.4 reduction rule
small-step semantics による表記．
(begin)(pop)(push)(exc)(βR1 )(βR2 )(βR1 )(βR2 )(exc)(push)(pop)(end)

e : +int
he ↑ f | cihe | f | cihe | e0 | cihe | x ⇒ e0 | cihe | dge ⇒ e0 | cihe | c0 ⇐ y | cihe | c0 ⇐ bgc | cihe | c0 | cihe | f | cihe | f ↓ cihn | • i{{{{{{{{{{{{h e| • ihe | f | cihe | f ↓ cihe0 | (dge ⇒ e ↑ g) ↓ ci
he0 [R~x 7→ e]| ci
he0 [R~dge 7→ e]| cihe| c0 [R~y 7→ c]i
he| c0 [R~bgc 7→ c]ihe ↑ (g ↓ c ⇐ bgc)| c0 ihe ↑ f | cihe | f | cin

簡約規則は，SLC の計算状態を２つ受け取り Prop 型を返す述語として定義した．

2.5 定理・補題
補題 2.1 (weakening)（継続については省略）Γ x ` e : +T
Γ x ∪ {x : +A} ` e : +TΓg ` f : T 1 ⊃ T 2
Γg ∪ {g : A ⊃ B} ` f : T 1 ⊃ T 2

証明 e, f, c の型の導出に関する mutual recursion による．
補題 2.2 (項に関する代入補題)
Γ x ∪ {x : +A} ` e : +T 0 , f : T 1 ⊃ T 2 , c : ¬T 3 のとき，` e0 : +A ならば Γ x ` e[e0 /x] : +T 0 , f [e0 /x] : T 1 ⊃T 2 , c[e0 /x] : ¬T 3 ．

証明 e, f, c の型の導出に関する mutual recursion による．
補題 2.1 および 2.2 を用いて，以下の定理が証明できる．
定理 2.1 (Preservation)
SLC 式 h. . . i1 について，` h. . . i1 が成り立つとき，h. . . i1 { h. . . i2 ならば，` h. . . i2 である．
証明

簡約規則についての場合分けによる．

定理 2.1 の証明が Coq によって定式化可能であることが示されたことにより，非決定性 SLC が well-typedな言語であることを保証する１要素が得られた．

3

call-by-value SLC

前節で定義した SLC に call-by-value 評価戦略を導入する．これによって，ある SLC 式の簡約結果は一意に定まることになる．
はじめに構文について述べる．call-by-value では，関数に渡される引数はすべて値になるまで簡約されてから渡される．よって，構文には値 v が導入され，v, e, f, cの４つが相互再帰するデータ型へと変更した．非決定性 SLC では項として扱われていた自然数 n，変数 x，項型の関数 d f e が値として扱われるようになり，さらに context [v ↑ (g ↓ c ⇐ bgc)] が値として新たに定義されている．
次に，簡約規則の変更点であるが，call-by-value では，引数は β 簡約の前に評価されているはずであるから，SLC の簡約規則もそれに従い変更される．例えば，非決定性 SLC の簡約規則のひとつである (exc) は，項の部分が値の形をしていなければ適用されなくなる，という具合である．
また，構文に context が追加されたことに伴い，簡約規則にもそれに関する規則が追加されている．

3.1

定理・補題・系

定義 3.1 （CBV SLC の停止性論理述語）
call-by-value SLC において，停止性を示す論理述語は以下のようになっている．
1.

(a) Rv+int (n) は自明
f(b) Rv+(A→B) (d f e) ⇐⇒ RA⊃B(f)(c) Rv+(A−B) ([v ↑ (g ↓ c ⇐ bgc)])⇐⇒ Rv+A (v) かつ Rc¬B (c)+T 型の項についての論理述語は，¬T 型が +T 型よりも小さな型でなければ，停止性を表す述語として適当であると言えない．
一方 Coq では，停止することが保証されない定義は定式化することができないようになっている．つまり，定義 3.1 を Coq によって定式化し，次に述べる主定理の証明を Coq 上で行うことができれば，CBV SLC の停止性を保証することが可能となる．
3.2 CBV SLC の停止性
定理 3.1 (Termination)
Γ = xi : +T i , y j : ¬T j , gk : Ak ⊃ Bkfであり，Rv+Ti (vi ), Rc¬T j (c), RAk ⊃Bk ( fk ) について，ρ =[vi /xi , c j /y j , fk /gk ] とする．このとき，以下が成り立つ．
1. Γ ` v : +T ⇒ Rv+T (vρ)
2. Γ ` e : +T ⇒ Re+T (eρ)
f3. Γ ` f : A ⊃ B ⇒ RA⊃B( f ρ)

4. Γ ` c : ¬T ⇒ Rc¬T (cρ)

系 3.1 (Normalization)
call-by-value SLC において，` e : +int ならば，e {∗ nであるような n が一意に存在する．

4 まとめと今後の課題
項と継続を同じように扱うことが可能である対称ラムダ計算の Coq による定式化を試みた．非決定性 SLCについては，定理 2.1 および定理 2.2 の証明の定式化を行い，SLC が well-typed な言語であることを保証する条件の１つを得た．
また，非決定性 SLC を，評価戦略 call-by-value を導入した call-by-value SLC に書き換え，停止性論理述語の定式化を試みた．
今後の課題としては，CBV SLC の停止性論理述語の定式化手法の検討が第一に挙げられる．
定義 3.1 は，値，項，関数，継続についての論理述語が非常に複雑な相互再帰によって定義されている．
単純型付きラムダ計算とは異なり，SLC では常に項と継続の２つ組，または項，関数，継続の３つ組で計算状態が表されるため，簡約が行われる際のそれらの状態遷移の関係を含めて正しく定式化しなければならな
い．ただし，定義 3.1 の定式化さえ実現できれば，定理 3.1 の証明を定式化することは可能であると予測される．

2. Re+T (e) ⇐⇒ ∀Rc¬T (c).he | ci {∗ nf
3. RA⊃B( f ) ⇐⇒ ∀Rv+A (v).∀Rc¬B (c).hv | f | ci {∗ n

4.

Rc¬T (c)⇐⇒∀Rv+T (v).hv | ci {∗ n

本稿では，定義 3.1 の Coq による定式化が可能であるかを検証している．上田らによってその正当性は十分に検証されているが，定義が複雑なため，定理証明器による定式化が実現されれば，その正当性がより強力に保証されることになる．
定義 3.1 は型に関する論理述語によるため，ある述語を定義する述語は，もとの述語よりも小さな型に関するものでなければならない．しかし，定義 3.1.1〜4は互いに再帰する形で記されており，例えば 3.1.2 の参考文献[1] Filinski, A.: Declarative Continuations and Categorical Duality, in DIKU report 89/11, University ofCopenhagen (1989).
[2] 阪上紗里, 浅井健一：対称 λ 計算の基礎理論, コンピュータソフトウェア, 第 26(2) 巻 (2009).
[3] Ueda, Y. and Asai, K.: Reinvestigation of Symmetric
Lambda Calculus, in DIKU report 11/01 (2011).