型付き対称λ計算と古典論理
Symmetric λ-Calculus and Classical Logic
上田 やよい浅井 健一

ueda.yayoi@is.ocha.ac.jp

asai@is.ocha.ac.jp

お茶の水女子大学

平成 22 年 2 月 13 日

概要れるようになっている。CPS 変換や評価文脈などの手法が提案されてきているが、CPS 変換はプログラ

対称λ計算 (Symmetric λ-Calculus, SLC) [Filinski

ムの構造が大きく変化し、また評価文脈はプログラム
1989] は、項と継続が完全に対称な形をしており、項を の構造自体は大きく変えないが「評価文脈」という新扱うのと全く同じ様に継続を扱うことができる。阪上 しい概念を扱えるようにする必要がある。
らの型付き対称λ計算 [2008] では、簡約規則を small
残りの計算である継続と、現在計算している項とstep semantics で定式化し直し、λC 計算 [Felleisen を統一的に扱う理論としては、Fillinski の対称λ計
and Hieb 1992] や λµ 計算 [Parigot 1992] を SLC に 算 (Symmetric λ-calculus, SLC) がある [3]。阪上ら変換できることが示された。

は SLC を small-step で定式化し直し、Felleisen の上田の先行研究 [2009] では、SLC の型に論理積とλC 計算 [2] と Parigot の λµ 計算 [6] が SLC に変換

論理和を導入した。しかしこの体系では、型として論できることを示した。上田らの先行研究 [9] では阪上理式を与えているものの、base case が整数型である

らの SLC に対して論理和型と論理積型を導入した。

ために論理学的な意味を考えることが難しかった。

SLC では関数が対偶の型を同時に持っていることが特徴的である。このため SLC は古典論理だと思われてきたが、その証明は成されていなかった。

本研究では、SLC の型定義に false (⊥) 型を加える
ことで、SLC の型規則が古典論理学に対応していることを示す。またその一例として排中律や二重否定の型を持つ項を導出する。

本研究では、まず SLC の定式化をし、Progress,
Preservation の証明や Call-By-Value の導入及びその簡約の一意性、停止性などの性質を紹介する。さら1

序論に SLC に ⊥ 型を導入した体系 SLC⊥ について、その型規則を古典論理で表すことができ、健全であるこ計算理論において、λ計算と直観主義論理が対応しとを示す。その上で SLC⊥ の型規則を用いて、古典ており、カリーハワード同型が示せることは周知の事

論理の形式体系 NK の推論規則を RAA (背理法) を含実である。しかし古典論理と計算理論の関係は、長らめて表現できることを示す。さらに、二重否定の除去(¬¬A ⊃ A) や排中律 (A ∨ ¬A) を実際に SLC⊥ で導最初に古典論理とのカリーハワード同型を示したの 出する。
本論文の構成は以下の通りである。まず 2 章では古は Griﬃn である。1990 年に [4] において call/cc がPeirce’s Law に、コントロールオペレータ C が二重否 典論理と形式体系 NK を紹介する。3 章では SLC のく解明されなかった。

定の法則と対応することが示された。その後 Parigot

定式化及び Call-By-Value の導入と停止性などの各が λµ 計算と古典論理の自然演繹が対応することを示

種性質の紹介をする。4 章では SLC に対して型 ⊥ をした [6]。さらに古典論理の sequent 計算と対応する

加えた SLC⊥ を導入する。5 章では SLC⊥ の型規則体系を Curien, Herbelin [1] や Wadler[10, 11] が提唱を古典論理で表し、SLC⊥ の健全性を示す。最後に 6した。

章では SLC⊥ で古典論理の推論規則が表せることを一方、近年では例外処理など非局所的な制御を扱うために「プログラムの残りの計算」を表す継続が使わ示し、その例として二重否定や排中律を実際に SLC⊥で導出する。

Γ, A ` A

A, B, C ::= ⊥ | X | ¬A | A ∧ B | A ∨ B | A ⊃ B
図 1: 古典論理式の構文

2

古典論理
古典論理の論理式は図 1 の定義で表される。

A、B 、C を任意の論理式とする。X は命題変数である。¬A は A の否定を表す。A ∧ B は A と Bの論理積である。A ∨ B は A と B の論理和である。

A ⊃ B は含意であり「A ならば B 」と読む。各論理Γ`A Γ`BΓ ` A ∧ B ∧E
∧I
1
Γ`A∧B
Γ`A
Γ ` A ∨I
1
Γ`A∨B
Γ`A∨B

体系 NK を用いる。図 2 にその推論規則を示した。

Γ ` A ∧ B ∧E
2Γ`BΓ ` B ∨I
2
Γ`A∨B

Γ, A ` CΓ`CΓ, B ` C∨E

Γ, A ` B
Γ`A⊃B Γ`A
⊃I
⊃E
Γ`A⊃B
Γ`B

演算子は図 1 で左にあるものほど結合力が強い。
推論規則として、古典論理を自然演繹で表した形式

Axm

Γ, ¬A ` ⊥
RAA
Γ`A

(
)
Γ`⊥
⊥E
Γ`A

ここでは [5] による定式化を用いている。
仮定となる論理式の集合を Γ で表し、そのもとで論理式 A が成り立つとき Γ ` A と表す。Γ は空集合でもよい。また A とは関係のない論理式を含んで

Γ, A, A ` B
Γ`B
Weak
Cont
Γ, A ` B
Γ, A ` B

いても構わない。図 2 の最下段は仮定 Γ に関する規則である。Weak は B とは関係のない仮定 A を加え

図 2: 古典論理の形式体系 NK

る規則、Cont は仮定に同じものが含まれる場合に片方を消去する規則である。Γ を集合として扱うため、 立つと推論する規則である。⊃ E は、同じ仮定 Γ のもInterchange の規則はない。Γ, A ` B では A の位 とで A ⊃ B, A が成り立つならば B が成り立つと推置は関係なく、仮定に A が含まれていればよい。
論する規則である。モーダスポネンスとも呼ばれる。
各規則は「上段が成り立つならば、下段が推論される」と読む。特に Axm は上段に何もないので、前提なしに Γ, A ` A を導くことができる。
以下、各規則について注釈を加える。

Axm は、仮定に論理式 A が含まれているならば、Aは無条件に成り立つとする規則である。古典論理の証
明の base case となる規則である。

RAA は、推論の仮定で矛盾が生じた場合、仮定に含まれる ¬A を消去し、A を推論する規則である。一√般には背理法と呼ばれ、「 2 は無理数」の証明に使われる背理法と全く同じものである。
() をつけて書かれている規則 ⊥E は、直観主義論
理の推論規則である。古典論理は「直観主義論理の体系に背理法 (RAA) を加えたもの」が定義であるため、∧I は、同じ仮定 Γ のもとで A と B が成り立つな 厳密には ⊥E も古典論理の導出規則に含まれる。しから、Γ のもとで論理積 A ∧ B が成り立つと推論する し実際には、⊥E の上段の仮定に Weak で ¬A を加え規則である。∧E1 はその逆で、A ∧ B が成り立つのな ると RAA と全く同じ推論を表していると言えるので、ら A も B も真であるはずなので、A が成り立つと推 本論文では ⊥E を RAA で代用する。（余談であるが、論する規則である。∧E2 も 同様である。
RAA を ⊥E で代用することはできない。またその点が∨I2 は、A が成り立つならば任意の論理式 B につ 古典論理と直観主義論理の違いでもある。）
いて A ∨ B が成り立つと推論する規則である。∨I1
論理演算子 ¬A は、適宜矛盾を表す ⊥ を用いても同様である。∨E は、ある仮定 Γ のもとで A ∨ B A ⊃ ⊥ と読み替え、⊃ I 及び ⊃ E を用いて推論する。
⊃ I において B を ⊥ と考えると、ある仮定のもととで C が成り立つならば、Γ のみのもとで C が成り で矛盾 ⊥ が導かれたら仮定のどれかが間違っている、
立つと推論する規則である。
つまり A ⊃ ⊥ (¬A) を推論する。⊃ E でも同様に B⊃ I は、ある仮定のもとで B が成り立つならば、 を ⊥ と考え、同じ仮定のもとで A と A ⊃ ⊥ (¬A)
仮定に含まれる任意の論理式 (図 2 では A) を取り出 が導かれたら矛盾する、つまり ⊥ を推論する。
が成り立ち、かつ Γ と A のもとで C が、Γ と B のもし、残りの仮定 (図 2 では Γ) のもとで A ⊃ B が成り

¬(A ∧ B) ≡ ¬A ∨ ¬B

ドモルガンの法則1¬(A ∨ B) ≡ ¬A ∧ ¬B
A ⊃ B ≡ ¬B ⊃ ¬A
A ⊃ (B ⊃ C) ≡ (A ∧ B) ⊃ C

ドモルガンの法則2A ≡ ¬¬AA⊃A
A ∨ ¬A

対偶律
移入律

dx ⇒ xe ↑ (dge ⇒ 1 ↑ g)
(begin) ;(pop) ;
(βf ) ;(pop) ;(β) ;(end) ;

二重否定の法則
同一律
排中律

図 3: 恒真式の例

2.1

恒真式

h dx ⇒ xe ↑ (dge ⇒ 1 ↑ g) | •int i
h dx ⇒ xe | dge ⇒ 1 ↑ g | •int i
h 1 ↑ (x ⇒ x) | •int i
h 1 | x ⇒ x | •int i
h 1 | •int i1
図 5: SLC 実行例を保持している必要がある。そのため、SLC の計算

図 2 で推論される論理式のうち Γ が空のものを恒真式と呼ぶ。A ∨ ¬A、¬¬A ⊃ A などがそれにあたる。本論文で使用する恒真式を図 3 に示した。≡
は「同値」を表す論理演算子で、A ≡ B の定義は

(A ⊃ B) ∧ (B ⊃ A) である。ここでは、左右の論理

状態は h 項 | 継続 i の二つ組か h 項 | 関数 | 継続 i の三つ組で記述される。
図 5 に SLC 式の例とその実行例を示した。一行目は(λf.f 1)λx.x を SLC の項で表したものである。λ抽
象 λf.f 1 は SLC の項の関数 dge ⇒ 1 ↑ g に、λx.x は

dx ⇒ xe に対応する。g は SLC での関数用の変数で、λ計算では一般に変数 f で表されるものである。↑ は恒真式に関して、次の補題を特に断りなく使用する。
SLC での項の関数適用を表している。1 ↑ g はλ計算式が等価であることを意味するために使用している。

Lemma 2.1 論理式 C[A]（C 中に A が現れる）につ で変数 f に 1 を渡す f 1 に、dx ⇒ xe ↑ (dge ⇒ 1 ↑ g)
いて、A ≡ B ならば、C に現れる任意の A を B に はλ抽象 λf.f 1 に λx.x を渡す (λf.f 1)λx.x に相当置き換えた論理式 C[B] は、C[A] ≡ C[B] を満たす。 する。なお、SLC では関数適用の関数と引数の位置が入れ替わっている。
二行目では、一行目の項と初期継続 •int で SLC の計

3型付き対称λ計算
対称λ計算 (Symmetric λ-Calculus, SLC) は「項e」「関数 f 」「継続 c」から成り、項と継続を双対的に計算する計算言語理論である。その型 (図 4) も双対的に定義されており、項を +T 型と表すのに対して、それを受け取る継続を ¬T 型と表す。関数は項と継続をつなぐ中立の型で、論理学での対偶の関係にある型を同時に持つ。Non-Deterministic SLC では実算状態の二つ組を作っている。•int は直感的には空の継続に相当する。三行目では、項から関数 dge ⇒ 1 ↑ g を取り出して注目し、関数を中心にその時を項を右側に、継続を左側に分けている。四行目では関数 dge ⇒ 1 ↑ gのβ簡約が起こり、項にあった関数 x ⇒ x が変数 gに代入されている。五行目では、再び項から関数を取り出している。取り出された関数 x ⇒ x は恒等関数であるので 1 をそのまま返す。

行規則も完全に対称形である。本論文では阪上の体系[8] に論理積型と論理和型、すなわち項の組と継続の組を導入したものを扱っている。
SLC では項と継続を双対的に計算するため、実行の際には現在の「項」「継続」と注目している「関数」

3.1

構文

型付き対称λ計算の構文は、項 e、継続 c、関数 fから成り、n, •T を除くと関数を中心とする対称形である (図 6)。他のλ計算に比べて関数が項から独立している点が特徴的であり、それに伴う構文や規則が存

S

T, A, B::= +T| {+A→+B
¬A←¬B
| ¬T

(項 e の型)(関数 f の型)
(継続 c の型)::= int | A ∧ B | A ∨ B | A → B | A − B

図 4: 型付き対称λ計算 SLC 型定義

在する。
例えば、通常のλ計算では関数適用を M M のよ
うに式を並べて書くが、SLC では e ↑ f のように、
関数 f に項 e を渡すと記述する。従って、関数に関数を渡したい場合には、df e のように関数にタグをつけ、一時的に項として扱って関数に渡す。受け取った

数とは逆に、仮引数 y を右側に、関数の本体の継続

e ::= n | x | (e, e) | df e | e ↑ f::= g | x ⇒ e | (x1 , x2 ) ⇒ e | dge ⇒ e | e |h | c ⇐ y | c ⇐ (y1 , y2 ) | c ⇐ bhc | c
c ::= •T | y | (c, c) | bf c | f ↓ c

fc を左側に書く。
簡便のため、SLC で扱う変数 x, y, g, h をまとめて var という記号で表している。なお、関数用の変数

g と h は SLC の双対性を示すために２種類記述しているが、どちらも関数 f を表す変数なので実質的にvar::= x | y | g | h
図 6: SLC 構文

1 ↑ dy ⇐ ye ↑ (x ⇒ x)
図 7: SLC 式の例

は同じものである。

3.2

型規則

SLC の型は図 4 のように定義される。SLC の型には大きく３種類あり、項の型 +T 、継続の型 ¬T 、関数の型 {+A→+B¬A←¬B から成る。+T は「+T 型を返す項」という意味である。それに対し ¬T は「+T 型の項を受け取る継続」という意味を持つ。項の型についてい関数を項ではなく関数として使えるようにするには、 る記号 + は項型であることを明示するためのもので、dge ⇒ e のように関数の仮引数部分にパターンマッチ 論理学上の意味はない。関数の型 {+A→+B で使われ¬A←¬Bを書く。e の中で変数 g を用いることで、渡された関 ている矢印 →、← は、どちらも SLC 上での含意を数を使えるようになる。図 5 では、これらの式を用い 表す。2 章の ⊃ と意味は同じで、「+A ならば +B 」て関数 x ⇒ x を関数 dge ⇒ 1 ↑ g の本体の中で使え 「¬B ならば ¬A」と読む。その意味は「+A 型の項をるようにしている。

さらにこの構文では、関数適用 e ↑ f の f の部分に関数適用をそのまま書くことは出来ないため、関数受け取り +B 型の項を返す関数」あるいは「¬B 型の継続を受け取り ¬A 型の継続を返す関数」である。
両者は論理学での対偶の関係にあたる。

を返す項 e を一時的に関数として扱うためのタグ e

図 4 の T などで定義されている型は、SLC の式のを導入している。後述する実行規則 (exc) (3.3 節) を形を表すものである。int は整数 n の型で、SLC の用いて、必要なときに e の実行に移る。これらを用い型の base case である。A ∧ B は項の組 (e, e) の型

た SLC 式の例を図 7 に示した。
以下、SLC の構文について注釈を加える。

であり、論理学の論理積に相当する。A ∨ B は継続の組 (c, c) の型であり、論理学の論理和に相当する。
SLC の構文は、項 e、関数 f 、継続 c から成る。 A → B は関数の項扱い df e の型であり、論理学の含
項 e は、整数 n、変数 x、項の組 (e, e)、関数の項 意に相当する。A − B は関数の継続扱い bf c の型で扱い df e、関数適用 e ↑ f から成る。関数 f には、関 ある。− は「含意の対偶の否定」を表す論理演算子
数用の変数 g 、λ抽象 λx.M に相当する x ⇒ e、そ で、A − B は ¬(¬B ⊃ ¬A) と定義される。
れに関数のパターンマッチをつけた dge ⇒ e、項の組
SLC の型導出規則を図 8 に示した。これらの型規のパターンマッチをつけた (x1 , x2 ) ⇒ e、項の関数扱
い e が含まれる。
ここまでが項に関する構文である。以下は継続につ

則は論理学の推論規則に則ったものである。環境 Γ のもとで式 M が型 S を持つとき、Γ ` M : S と表す。

Γ は変数の型定義 var : S の集合である。図中には示いての構文であり、項の構文と対称形を成している。 していないが、Weak と Cont は自由に用いてよい。
継続 c は、初期継続 •T 、変数 y 、継続の組 (c, c)、関数の継続扱い bf c、関数適用 f ↓ c から成る。初期
継続 •T には、任意の型 T を与えてよい。継続の関TVar は変数の導出規則である。SLC で扱う変数は全て、この規則により導出される。

TAnd は項の組を導出する規則、TOr は継続の組を導出する規則である。論理学で ∧ を推論する規則になっており ↓ で表される。継続を扱う関数として、変 則ったものである。SLC の型定義 (図 4) より継続の数 h、λ抽象 x ⇒ e の双対にあたる c ⇐ y 、それに 型は ¬T の形でなければならないので、TOr で導出さ数適用は、項の関数適用とは関数と引数の位置が逆に関数のパターンマッチをつけた c ⇐ bhc、継続の組のパターンマッチをつけた c ⇐ (y1 , y2 )、継続の関数扱
い c がある。継続を扱う関数 c ⇐ y は、項を扱う関れた型は ¬A ∧ ¬B からドモルガンの法則を用いて ¬を前に出した形となっている。継続の組の型が ∨ で表現されるのはこのためである。

Γ ` n : +int

TInt

Γ, var : S ` var : STVarΓ ` •T : ¬T TInitΓ ` e1 : +A Γ ` e2 : +BΓ ` c1 : ¬A Γ ` c2 : ¬B
TAndTOr
Γ ` (e1 , e2 ) : +(A ∧ B)Γ ` (c1 , c2 ) : ¬(A ∨ B)
Γ, x : +A ` e : +BΓ ` x ⇒ e : {+A→+B
¬A←¬B

TFun

Γ, y : ¬B ` c : ¬A
Γ ` c ⇐ y : {+A→+B
¬A←¬B

TFun

Γ ` f : {+A→+B
Γ ` e : +AΓ ` f : {+A→+B
Γ ` c : ¬B
¬A←¬B
¬A←¬B
TApp
TApp
Γ ` e ↑ f : +BΓ ` f ↓ c : ¬A
Γ ` f : {+A→+B
Γ ` f : {+A→+B
¬A←¬B
¬A←¬B
TFClo
TFClo
Γ ` df e : +(A → B)Γ ` bf c : ¬(A − B)Γ ` e : +(A → B)Γ ` e : {+A→+B¬A←¬B
Γ, x1 : +A, x2 : +B ` e : +T+(A∧B)→+TΓ ` (x1 , x2 ) ⇒ e : {¬(A∧B)←¬T

TCFun

TPFun

Γ ` c : ¬(A − B)
Γ ` c : {+A→+B
¬A←¬B

TCFun

Γ, y1 : ¬A, y2 : ¬B ` c : ¬T
+T →+(A∨B)Γ ` c ⇐ (y1 , y2 ) : {¬T ←¬(A∨B)

TPFun

Γ, g : {+A→+B¬A←¬B ` e : +T

Γ, h : {+A→+B¬A←¬B ` c : ¬T
TFFun+(A→B)→+T+T →+(A−B) TFFunΓ ` dge ⇒ e : {¬(A→B)←¬TΓ ` c ⇐ bhc : {¬T ←¬(A−B)
図 8: SLC 型規則(begin)(lef t)e : +Th (e1 , e2 ) | c i; h e | •T i
; h e1 | x1 ⇒ (x1 , e2 ) | c i(right)(pop)h (e1 , e2 ) | c ihe↑f |ci; h e2 | x2 ⇒ (e1 , x2 ) | c i; he|f |ci(push)(exc)(β)

he|f |ci
h e | e0 | c i
h e | x ⇒ e0 | c i; he|f ↓ci; h e0 | dge ⇒ e ↑ g | c i; h e0 [e/x] | c i

(βp )
(βf )

h (e1 , e2 ) | (x1 , x2 ) ⇒ e0 | c i
h df e | dge ⇒ e0 | c i; h e0 [e1 /x1 , e2 /x2 ] | c i; h e0 [f /g] | c i

(βf )
(βp )
(β)

h e | c0 ⇐ bhc | bf c i
h e | c0 ⇐ (y1 , y2 ) | (c1 , c2 ) i
h e | c0 ⇐ y | c i; h e | c0 [f /h] i; h e | c0 [c1 /y1 , c2 /y2 ] i; h e | c0 [c/y] i(exc)(push)

h e | c0 | c ihe|f |ci; h e | h ↓ c ⇐ bhc | c0 i
; he↑f |ci(pop)(right)(lef t)he|f ↓cih e | (c1 , c2 ) i
h e | (c1 , c2 ) i; he|f |ci; h e | (c1 , y2 ) ⇐ y2 | c2 i
; h e | (y1 , c2 ) ⇐ y1 | c1 i

(end)

h e | •T i

; e : +T

図 9: SLC 実行規則 (Non-Deterministic)

TFun は項の関数を導出する規則、TFun は継続の関 る。三つ組は、中央の関数に注目して SLC 式全体を数を導出する規則である。論理学の含意の推論に相当 項と継続に分け、関数の実行に移ろうとしている状態する。項の関数、継続の関数ともに、項中心に書かれを表す。二つ組は、項または継続の中から新たに中央た型 +A → +B と継続中心に書かれた型 ¬A ← ¬Bに関数を取り出そうとしている状態を表す。

の両方を表示する。

二つ組や三つ組をつくる際、項、継続、関数の型はTApp は項の関数適用を導出する規則である。論理

図 10 の型規則を満たさなければならない。二つ組は学ではモーダスポネンスに相当する。TApp では関数

+T 型を持つ項 e と +T 型を受け取る継続 c : ¬T での型を項中心に考え +A → +B 型の関数に +A 型のつくられる。三つ組は +A 型を持つ項 e と +A 型の項項を渡すと +B 型の項を返すと考える。TApp も同様を受け取って +B 型の項を返す (または ¬B 型の継続だが、関数の型を継続中心に考えている点で異なる。 を受け取って ¬A 型の継続を返す) 関数 f : {+A→+B¬A←¬B 、
る。関数 f に関数の項扱いを表すタグ d e をつけて+B 型を受け取る継続 c : ¬B からつくられる。
図 9 に SLC の実行規則を示した。以下注釈を加いる他、関数型 {+A→+B¬A←¬B から項型 +(A → B) に変える。

TFClo は関数の項扱いを導出するための規則であ(begin) は +T 型を持つ項 e に対して ¬T 型の初らの型規則は、型の形及び SLC 式の形を変えている 期継続 •T を与え、SLC の実行を始める規則である。
これは二つ組でも三つ組でもない特殊な規則で、後述だけである。
TFClo は関数の継続扱いを導出するための規則であ する (end) で取り出された項に対して用いることはわっている。TCFun はその逆をする規則である。これる。関数 f に関数の継続扱いを表すタグ b c をつけて許さない。

いる他、型が関数型 {+A→+B¬A←¬B から継続型 ¬(A − B)に変わっている。¬(A − B) は論理演算子 − の定義(lef t) は項の組から左側を取り出して実行するための規則である。実行が終わったら、右辺の中央により ¬¬(¬B → ¬A) に等しい。従って、この型規則現れている関数 x1 ⇒ (x1 , e2 ) で元の組の形に戻す。

は ¬B → ¬A からその二重否定を推論する規則と言(right) は項の組の左側を取り出して実行するためのえる。TCFun はその逆の導出を行う規則である。

規則である。(pop) は項の中から関数を取り出し、そTPFun は項の組のパターンマッチがついた関数を導 の実行に移ろうとする規則である。(push) は取り出出するための規則である。直感的には、環境に含まれる した関数を実行せずに継続側に押しやり、さらに項の変数 x1 : +A, x2 : +B で項の組 (x1 , x2 ) : +(A ∧ B)

中を実行するための規則である。(exc) 1 は関数扱いさをつくり、それを TFun で関数の形にしたものに相当れている項を左側に取り出し、実行しようとする規則

する。TPFun は TPFun の継続版で、継続の組のパターである。実行が終わったら、右辺の中央に現れているンマッチがついた関数を導出するための規則である。 関数で元の関数適用の形に戻す。(β) はλ抽象のβ簡

TFFun は関数の項扱いのパターンマッチがついた関 約と全く同じである。その時の項 e を変数 x で束縛数を導出するための規則である。直感的には、環境に し関数の本体 e0 に代入する。これを図中では e0 [e/x]含まれる変数 g : {+A→+B¬A←¬B を TFClo で dge : +(A → と表している。(βp ) は項の組のパターンマッチのつB) の形に変えて、TFun を適用したものに相当する。 いた関数をβ簡約するための規則である。e1 , e2 をそ
TFFun は TFFun の継続版で、関数の継続扱いのパター れぞれ x1 , x2 で束縛し、e0 に代入する。この簡約にンマッチがついた関数を導出するための規則である。 より、組になっていたふたつの項を e0 の中で別々にTInt は整数 n を導出する規則、TInit は任意の型 使えるようになる。(βf ) は関数の値扱いのパターンの初期継続を導出する規則である。
図 5, 図 7 に示した式は、図 8 の規則に従って型を` e : +T ` c : ¬T
TProg1`he|ci

導出することができ、どちらも +int 型となる。

3.3

実行規則

項と継続を Dual に計算する SLC では、その実行に際してその時点での項と継続、関数を保持している必要がある。従って SLC の計算状態は h 項 | 継続 iの二つ組か、h 項 | 関数 | 継続 i の三つ組で記述され` e : +T1

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

`he|f |ci
図 10: SLC 計算状態
1 (exchange) の省略形

TProg2

数 dge ⇒ 1 ↑ g を (pop) で中央に呼び戻す。今度は項1 ↑ dy ⇐ ye ↑ (x ⇒ x)の形とパターンマッチが一致しているので、(βf ) で(begin)
(pop)
(exc)

; h 1 ↑ dy ⇐ ye ↑ (x ⇒ x) | •int i
β簡約を行うことができる。パターンマッチによって; h 1 | dy ⇐ ye ↑ (x ⇒ x) | •int i
引数 dy ⇐ ye のタグ d e が外れ、以降の式で y ⇐ y; h dy ⇐ ye ↑ (x ⇒ x) | dge ⇒ 1 ↑ g | •int i を関数として扱えるようになっている。y ⇐ y は項

(push)(pop)(β); h dy ⇐ ye ↑ (x ⇒ x) | (dge ⇒ 1 ↑ g) ↓ •int i の関数 x ⇒ x と対を成すもので、継続の恒等関数で; h dy ⇐ ye | x ⇒ x | (dge ⇒ 1 ↑ g) ↓ •int i ある。従って (β) でこの関数のβ簡約を行うと、その; h dy ⇐ ye | (dge ⇒ 1 ↑ g) ↓ •int i
ときの継続 •int がそのまま返ってくる。

(pop)
(βf )

; h dy ⇐ ye | dge ⇒ 1 ↑ g | •int i; h 1 ↑ (y ⇐ y) | •int i

(pop)
(β)
(end)

; h 1 | y ⇐ y | •int i; h 1 | •int i;1

図 9 の実行規則について以下の定理が成り立つことを、c, f , e 及び簡約規則による場合分けでそれぞれ示すことができる。

Theorem 3.1 (Progress)
図 9 の実行規則について

図 11: SLC 実行例

1. ` h e | f | c i であるならば、ある c0 , f 0 , e0 が存在し、h e | f | c i ; h e0 | f 0 | c0 i または

h e | f | c i ; h e0 | c0 i である。

マッチをつけた関数をβ簡約するための規則である。
引数の df e のタグを外した状態で関数の本体 e0 中の変数 g に代入する。e0 の中では f を項ではなく関数

2. ` h e | c i であるならば、それは h e | •T i(e : +T ) という形であるか、ある c0 , f 0 , e0 が存在して、h e | c i ; h e0 | f 0 | c0 i である。

として扱うことができるようになる。

(βp ) と (βf ) は、項の形と仮引数のパターンマッチ
が一致しなければ適用できない。項がパターンと一致しない場合は (push) で中央の関数を継続へ押しやり、

Theorem 3.2 (Preservation)
図 9 の実行規則について項からさらに関数を取り出して実行する。(push) の代わりに (push) を用いて中央の関数を項側へ押しやり、継続から新たな関数を取り出してもよい。

1. ` h e | f | c i のとき、h e | f | c i ; h e0 | f 0 | c0 iならば ` h e0 | f 0 | c0 i であり、h e | f | c i ;h e0 | c0 i ならば ` h e0 | c0 i である。

以上が項に関する実行規則である。残りは継続に関するものであるが、これらは全て項の実行規則を継続側に移したものである。基本的に、対応する項の規則
名にをつけたものが継続の規則名になっている。

2. ` h e | c i のとき、h e | c i ; h e0 | f 0 | c0 iならば ` h e0 | f 0 | c0 i である。

一つだけ異なる規則 (end) は、継続が初期継続の

なお、図 9 に示した実行規則は非決定的である。こみの場合に初期継続に項を渡して実行を終了する規の規則は自由度がかなり高く、(pop) と (push) を無限則である。これも (begin) と同様特殊な規則であり、 に繰り返したり、(begin) で実行を始めた直後に (end)(end) を用いた後は (begin) で再び実行を始めること で実行を終了することができる。
は許さない。
図 9 の実行規則を用いて、図 7 の SLC 式を実際に実行すると、図 11 のようになる。

3.4

Call-By-Value SLC

1 ↑ dy ⇐ ye ↑ (x ⇒ x) は +int 型であるので、まず3.3 節で示した実行規則は非決定的であり、自由度(begin) で ¬int 型 (int 型を受け取る継続の型) の初 が極めて高かった。ここでは SLC に評価戦略 Call期継続を与えて SLC の計算状態をつくり、(pop) で By-Value (CBV) を導入し、SLC の性質についてよ
項から関数を取り出す。この関数はこのままではβ簡 り詳しく検証していく。
約できないので、(exc) で の中身の実行に移る。中一般に Call-By-Value とは、β簡約を行う際にその央に現れた関数 dge ⇒ 1 ↑ g は、項の形と仮引数の 引数をそれ以上簡約できない形、つまり値 (value) ま
パターンマッチが合っていないので (push) で一旦継で簡約してから、β簡約を行うものである。SLC では、続に移動し、さらに項の内側の実行に移る。恒等関数

β簡約が項と継続の２種類存在する。Call-By-Valuex ⇒ x のβ簡約が終わったら、先程継続に移した関SLC は、項のβ簡約を行う際には引数を値まで計算

(begin)e : +T;h e | •T i

(lef tv )(rightv )(pop)

h (e1 , e2 ) | c ih (v1 , e2 ) | c ihe↑f |ci;;;

h e1 | x1 ⇒ (x1 , e2 ) | c i
h e2 | x2 ⇒ (v1 , x2 ) | c ihe|f |ci(pop0pv ) h [v ↑ (c0 ⇐ (y1 , y2 ))] | (c1 , c2 ) ih [v ↑ (c0 ⇐ bhc)] | bf c i(pop0f v )(pushv )he|f |ci;;;

h v | c0 ⇐ (y1 , y2 ) | (c1 , c2 ) i
h v | c0 ⇐ bhc | bf c i
he|f ↓ci(excv )(βv )h v | e0 | c i
h v | x ⇒ e0 | c i;;

h e0 | dge ⇒ v ↑ g | c i
h e0 [v/x] | c i(βpv )(βf )(βf v )h (v1 , v2 ) | (x1 , x2 ) ⇒ e0 | c i
h df e | dge ⇒ e0 | c i
h v | c0 ⇐ bhc | bf c i;;;

h e0 [v1 /x1 , v2 /x2 ] | c i
h e0 [f /g] | c i
h v | c0 [f /h] i(βpv )(βv )h v | c0 ⇐ (y1 , y2 ) | (c1 , c2 ) i
h v | c0 ⇐ y | c i;;

h v | c0 [c1 /y1 , c2 /y2 ] i
h v | c0 [c/y] i(excv )
(push0f v )(push0pv )h v | c0 | c i
h v | c ⇐ bhc | c i
h v | c0 ⇐ (y1 , y2 ) | c i;;;

h v | h ↓ c ⇐ bhc | c0 i
h [v ↑ (c0 ⇐ bhc)] | c i
h [v ↑ (c0 ⇐ (y1 , y2 ))] | c i(popv )
(endv )

hv|f ↓ci
h v | •T i;;

hv|f |ci
v : +T0

if e1 6= v
if e2 6= v

if e 6= v

if c 6= bf c
if c 6= (c1 , c2 )

図 12: Call-By-Value SLC 実行規則::= x | n | (v, v) | df e |[v ↑ (c ⇐ (y1 , y2 ))] | [v ↑ (c ⇐ bhc)]
e ::= v | (e, e) | e ↑ fv

f::= g | x ⇒ e | (x1 , x2 ) ⇒ e | dge ⇒ e | e |h | c ⇐ y | c ⇐ (y1 , y2 ) | c ⇐ bhc | c

c ::= •T | y | (c, c) | bf c | f ↓ cvar::= x | y | g | h
図 13: Call-By-Value SLC 構文+T →+(A∨B)Γ ` c ⇐ (y1 , y2 ) : {¬T ←¬(A∨B) Γ ` v : +TΓ ` [v ↑ (c ⇐ (y1 , y2 ))] : +(A ∨ B)

TPCont+T →+(A−B)Γ ` c ⇐ bhc : {¬T ←¬(A−B) Γ ` v : +TΓ ` [v ↑ (c ⇐ bhc)] : +(A − B)

TFCont

図 14: Call-By-Value SLC 追加型規則
従って、項 e とは別にそれ以上簡約できない式、値 vを定義する。値 v は、整数 n、変数 x、(e, e) の関数

し、継続のβ簡約は（継続の）引数が値継続になって適用を含まない形 (v, v)、関数の項 (値) 扱い df e、コ

いなくてもβ簡約を行うものとする。また、継続の計

ンテキスト [ ] から成る。関数適用を含む組 (e, e) は算よりも項の計算が優先される。つまり、継続の計算項として扱う。項の関数のβ簡約は引数が値 v になっは項が値になってから行う。通常、λ計算の Call-By-てから行われるので、項の変数 x は値 v に含める。
Value と言うと Right-to-Left と Left-to-Right の２ 本節で追加されているコンテキスト [ ] は、継続の式
種類存在するが、本論文の CBV は正確には Right- の形と関数のパターンマッチが合うまで、その関数のto-Left CBV にあたる。なお SLC では項の関数適用 実行を凍結するためのものである。コンテキストの型の位置が通常のλ計算とは逆になっているため、実際 規則を図 14 に示した。関数が継続のパターンマッチには SLC 式の左側から順に実行することになる。

付き関数に、引数が値に制限されていることと、導出
CBV SLC の構文を図 13 に示した。CBV では項の された SLC 式に [ ] がついていること以外は、項の関数に与える引数をそれ以上簡約できない形にする。 関数適用 TApp と全く同じである。コンテキストの具体的な役割は、実行規則と併せて解説する。

CBV SLC の実行規則を図 12 に示した。図 9 の実行規則が元になっているが、項のβ簡約と継続の計算
は項が v になってから行うよう、さらに実行手順が一意になるよう変更してある。図 9 から変更のある規則は、規則名に添字 v をつけて表している。

(lef tv ) 及び (rightv ) は e1 及び e2 が値 v でない
ときに限り適用する。(rightv ) は組の左側が値である

定理 3.3 から次の系が得られる。

Corollary 3.4 Call-By-Value SLC において、` e : +T ならばその簡約列は一意である。
また、Call-By-Value SLC について以下の定理が得られる。これは論理関係 (Logical Relation) の手法を用いて示すことができる。（紙面の都合上ここでは詳しく触れない。）

場合のみ適用できるものとし、左側が値でない場合はTheorem 3.5 (CBV SLC の停止性)
Call-By-Value SLC において、 ` e : +T である(pushv ) は項が値でないときに限り適用する。値なならば h e | •T i ; v と有限ステップで到達できる v
らば、β簡約をするか継続の計算に移る。(excv ) でが存在する。
e0 の中身の計算に移るのも、項が値の場合である。
β簡約はすべて項が値 v になってから行う。継続のβ簡約でも同じである。なお (βf ) のみはもともと 3.5 慣用表現

左側を先に計算する。

項が値 df e のときのみ適用される規則なので、Call-

By-Value でも規則に変化がない。

一般に、論理式の型を与える計算理論には、論理以降、継続に関する規則は全て、項が v である状

和型の項をつくるプリミティブ inl, inr が存在する。

態で実行を行う。Call-By-Value SLC では、一度項か

SLC にはそのようなプリミティブが存在せず、明示ら取り出した関数を再び項に戻すことは許されないた的に論理和型の項を定義してはいないが、TPFun でめ、(push) はコンテキストに関わる特別な条件下での導出される関数に TApp で項を関数適用させることみ使用することになる (後述)。また継続の組の中身をで、論理和型の項を導出することができる。特に関数計算する規則 (lef tv ) 及び (right) は Call-By-Value

SLC では使用しない。これは、この二つの規則を加えると簡約の一意性 (定理 3.3) が失われるためである。(lef tv ) と (right) がないので、継続の組の中身
はパターンマッチ付き関数で組から取り出されない限り計算されることはない。
新たに追加された規則 (pop0f v ), (pop0pv ), (push0f v ),(push0pv ) はコンテキスト [] に関わる規則である。(βf v )及び (βpv ) で継続の式の形がパターンと一致しなけれ

y1 ⇐ (y1 , y2 ) は、前提なしで導出できる上、項中心に型を考えると +A 型の項を受け取って +(A ∨ B) 型の項を返す関数であることから、SLC では慣用的にinl と表記している。
このような慣用表現を図 15 にまとめた。

f st 及び snd は項の組の片方を取り出す関数である。+(A ∧ B) 型を受け取って +A 型または +B 型を返す。継続を中心に考えると ¬A 型または ¬B 型
を受け取って ¬(A ∧ B) 型を返す関数になる。項とはば、継続 c の実行に移る。Call-By-Value では関数を対称に ¬(A ∧ B) 型を持つ継続は明示的に定義されて項に戻すことは許されないため、現在の値 v と関数をいないが、f st や snd を用いて論理積型の継続を導まとめてコンテキスト [ ] として値扱いし、c の実行に出することも可能である。

inl 及び inr は f st、snd と対を成す関数であり、本ある。c を実行してパターンマッチと継続の式の形が 来は継続の組から片方を取り出す関数である。従って合うようになったら、(pop0f v ) 及び (pop0pv ) でコンテ
キスト中の継続の関数を取り出し、その実行に移る。
+A→+(A∨B)
inl = y1 ⇐ (y1 , y2 ) : {¬A←¬(A∨B)
Call-By-Value SLC について、以下の定理が簡約規+B→+(A∨B)
inr = y2 ⇐ (y1 , y2 ) : {¬B←¬(A∨B)
則による場合分けで得られる。
+(A∧B)→+A
f st = (x1 , x2 ) ⇒ x1 : {¬(A∧B)←¬A+(A∧B)→+B
Theorem 3.3 (簡約の一意性)
snd = (x1 , x2 ) ⇒ x1 : {移れるようにする規則が (push0f v ) 及び (push0pv ) で

Call-By-Value SLC において、
1. ` h e | f | c i ならば、その簡約の仕方は一意である。
2. ` h e | c i ならば、その簡約の仕方は一意である。

[f1 , f2 ] ={f1 , f2 }¬(A∧B)←¬B+(A∨B)→+T(f1 ↓ y, f2 ↓ y) ⇐ y : {¬(A∨B)←¬T+T →+(A∧B)= x ⇒ (x ↑ f1 , x ↑ f2 ) : {¬T ←¬(A∧B)
図 15: SLC 慣用表現

そこで、本論文では SLC の型定義に ⊥ を加えたΓ ` e : +A
体系
SLC⊥ を導入し、SLC⊥ と古典論理との関係にInlΓ ` e ↑ inl : +(A ∨ B)
ついて考える。⊥ は「その型を持つ値は存在しない」という型を表す。従って ⊥ 型の値は定義されない。
Γ ` e : +(A ∧ B)
Γ ` e : +B
Inr
Snd
SLC⊥ の型定義を図 17 に示した。SLC (図 4) の定Γ ` e ↑ snd : +BΓ ` e ↑ inr : +(A ∨ B)
義に ⊥ と命題変数 X が加わっている。古典論理との関連を調べることが目的であるので、整数型 int はΓ ` f1 : {+A→+T
Γ ` f2 : {+B→+T
¬A←¬T
¬B←¬T
FPair
除いてある。SLC⊥ の構文は図 6 から整数 n を除い+(A∨B)→+TΓ ` [f1 , f2 ] : {¬(A∨B)←¬T
たものである。型規則は図 8 から TInt を除いたものになる。実行規則は図 9 と変わらない。
→+A→+AΓ ` f1 : {+TΓ ` f2 : {+T¬T ←¬A¬T ←¬A
SLC⊥ では SLC と同様にして次の定理が成り立つ。
FPair+T →+(A∧B)Γ ` {f1 , f2 } : {¬T ←¬(A∧B)
Theorem 4.1

Γ ` e : +(A ∧ B)Fst
Γ ` e ↑ f st : +A

図 16: SLC 慣用表現 型規則
その型は ¬(A ∨ B) 型を受け取って ¬A 型または ¬B
型を返す形になる。この対偶を取って項を中心に考えると、+A 型または +B 型を受け取って +(A ∨ B) 型

SLC⊥ において Progress が成り立つ。
Theorem 4.2
SLC⊥ において Preservation が成り立つ。
SLC と同様、SLC⊥ についても CBV を定義するを返す関数になる。これらを項の関数適用で用いるとことができる。CBV SLC⊥ について、CBV SLC と+(A ∨ B) 型の項を導出することができる。
[f1 , f2 ] はいわゆる match 文に相当する関数であ同様にして次が成り立つ。

る。項を中心に考えると f1 、f2 は受け取る型は違うが返す型は同じであるので、一つの継続を共有するこ

Theorem 4.3
CBV SLC⊥ の簡約の仕方は一意である。

とができる。それを表した関数が (f1 ↓ y, f2 ↓ y) ⇐ yCorollary 4.4である。この関数は、現在の継続 (¬T 型) を切り取っ CBV SLC で ` e : +T の簡約列は一意である。
⊥て二つの関数の後ろにコピーする。従って +A 型の項を受け取っても +B 型の項を受け取っても、この Theorem 4.5関数でつくられた継続の組のうち適当な方を選べば実行を完了することができる。[f1 , f2 ] の型は ¬T 型の継続を受け取って ¬(A ∨ B) 型の継続を返す関数である。これを項中心の型で読み替えると +(A ∨ B) 型の

CBV SLC⊥ で ` e : +T ならばその実行は停止する。
SLC⊥ と古典論理の関係を調べる際には、SLC⊥ の
項型 +T の T を古典論理による論理式と見なす。

SLC⊥ の型定義では項型の中に ¬ は現れないが、関数を項扱いするときに使う型 T → ⊥ を ¬T と解釈すとからも [f1 , f2 ] を match 文と見なすことができる。
る。これは古典論理や直観主義論理において、¬T を{f1 , f2 } は [f1 , f2 ] の継続版である。[f1 , f2 ] は項T ⊃ ⊥ と見なすのと全く同じことである。ただし、に対する match 文であったが、{f1 , f2 } は継続に対→+⊥関数の型 {+T¬T ←¬⊥ を ¬T と解釈はしない。あくまでする match 文と考えることができる。
も、論理式の ¬T と見なすのは「項」型の T → ⊥ で慣用表現を用いた SLC 式の導出規則を図 16 にまとある。このように厳格な区別をするのは、型規則中にめた。inl らについては紙面の都合上項の規則のみの→+⊥表れるすべての {+T¬T ←¬⊥ を ¬T と解釈すると、論理掲載だが、継続に対する規則も考えることができる。
項を受け取って +T 型の項を返す関数になる。このこ

4SLC⊥ の導入

SLC の型定義は base case が整数型であり、論理学的な意味を与えることが難しい。また、否定記号 ¬が継続の型にしか与えられない、つまり ¬T 型は書け
るが +(¬T ∨ T ) 型は SLC では書くことができない。

S ::= +T

(項 e の型)→+T| {+T(関数 f の型)
¬T ←¬T| ¬T(継続 c の型)
T, A, B ::= ⊥ | X | A ∧ B | A ∨ B | A → B | A − B

図 17: SLC⊥ 型定義

学上は正当な推論でも SLC⊥ の型規則には当てはまらないことがあるからである。

SLC⊥ と古典論理の関係を調べるにあたって、SLC⊥
に対していくつか制限を加える。
まず、初期継続は •⊥ : ¬⊥ のみ導出するものとする。SLC⊥ (SLC) では本来、TInit ではどのようなΓ, A ` A

Axm

Γ`A Γ`B
∧I
Γ`A∧B

Axm
Γ, ⊥ ` ⊥⊃IΓ ` ¬⊥Γ ` ¬A Γ ` ¬B∧I
Γ ` ¬A ∧ ¬BDM2
Γ ` ¬(A ∨ B)

型の初期継続を導出しても構わないが、論理学的には
任意の論理式の否定を導出することはできないからである。さらに、導出する項 e : +T は実行する前の項のみついて考える。これは (begin) で実行を始めると継続に初期継続 •T が現れ、項 e に代入される可能性を避けるためである。
これらの制限により、項 e が +⊥ 型を持つならば、
Γ, x : +⊥ ` x : +⊥ または Γ ` e ↑ f : +⊥ (Γ 6= Φ)であることが言える。

5

SLC⊥ の論理学的解釈

Γ, A ` B
Γ, ¬B ` ¬A
⊃I
⊃I
Γ`A⊃B
Γ ` ¬B ⊃ ¬A
Γ ` A⊃B Γ ` A
Γ ` ¬B ⊃ ¬A Γ ` ¬B
⊃E
⊃E
Γ`B
Γ ` ¬A

Γ`A⊃B
(なし)
Γ`A⊃B

Γ ` ¬B ⊃ ¬A
DNG
Γ ` ¬¬(¬B ⊃ ¬A)MINΓ ` ¬(A − B)

Γ`A⊃B
(なし)
Γ`A⊃B

Γ ` ¬(A − B)MIN
Γ ` ¬¬(¬B ⊃ ¬A)
DNG
Γ ` ¬B ⊃ ¬A

この章では 3.2 節の SLC⊥ の型規則 (図 10 から

TInt を除いたもの) が古典論理で表せることを見ていく。2 章の形式体系 NK 及び補題 2.1 を用いて、SLC⊥ の型規則が表現できることを示す。補題で用いる恒真式を図 18 に再掲した。証明図中では図 18 に示した規則名を用いている。SLC⊥ の型規則を NK で表したものを図 19 に示した。各証明図の配置は図 8に則っている。

SLC⊥ の関数には２種類の型（含意とその対偶）が存在するが、図 19 では、項の規則（左側）では関数

Γ, ¬A, ¬B ` ¬T⊃I
Γ, A, B ` T
Γ, ¬A ` ¬B ⊃ ¬T⊃I
⊃I
Γ, A ` B ⊃ TΓ ` ¬A ⊃ ¬B ⊃ ¬T
IMP⊃I
Γ ` ¬A ∧ ¬B ⊃ ¬T
Γ`A⊃B⊃T
DM2
IMPΓ`A∧B ⊃TΓ ` ¬(A ∨ B) ⊃ ¬TΓ, ¬B ⊃ ¬A ` ¬T⊃I
Γ ` (¬B ⊃ ¬A) ⊃ ¬T
DNG
Γ ` ¬¬(¬B ⊃ ¬A) ⊃ ¬T
Γ, A ⊃ B ` T⊃IMINΓ ` (A ⊃ B) ⊃ TΓ ` ¬(A − B) ⊃ ¬Tの型として「A ⊃ B 」を用い、継続の規則（右側）では「¬B ⊃ ¬A」を用いている。このため SLC⊥ の型

図 19: NK による SLC⊥ の型規則

導出木を NK で表す際には、図 19 の証明図の他に、

CNT を用いて含意を対偶に変えたり、対偶を含意に戻 TFun は NK の ⊃ I で表される。TApp、TApp は NK
したりという操作を加える必要がある。
の ⊃ E で表される。TFClo、TCFun は SLC⊥ 上の式
TVar は NK の Axm で表される。TInit は NK で 変形であり、論理学的な意味はない。TFClo、TCFun⊥ に関する Axm と ⊃ I で表される。TAnd は NK の は DNG と MIN で表すことができる。TPFun、TPFun∧I で表される。TOr は NK では ∧I で ¬A∧¬B を導 は NK で ⊃ I を二回用いて A ⊃ B ⊃ T を導出した
出した後、DM2 を適用して表すことができる。TFun、 後、移入律 で引数部分を A ∧ B に変えたものと考えられる。TPFun ではさらに DM2 を用いる。TFFun は¬(A ∨ B) ≡ ¬A ∧ ¬B
A ⊃ B ≡ ¬B ⊃ ¬A
A ⊃ (B ⊃ C) ≡ (A ∧ B) ⊃ C

DM2
CNT
IMP

A ≡ ¬¬A
A − B ≡ ¬(¬B ⊃ ¬A)

DNG
MIN

NK の ⊃ I の特別な場合と考えられる。引数は SLC⊥の型定義に合わせて TFClo と同様の変換を行っている。TFFun も同様である。
以上より、次の定理が得られる。

Theorem 5.1 SLC⊥ の型規則は、古典論理の形式
体系 NK で表すことができる。

図 18: 恒真式

SLC⊥ における古典論理

6

Theorem 6.2
SLC⊥ において ` e : +T ⇔ T は古典論理での恒真

5 章では、SLC⊥ の型規則を古典論理の形式体系 NK 式である。
で表せることを示した。本章では、古典論理の形式体
例として、図 21 に +(A ∨ (A → ⊥)) の導出木を示系 NK を SLC⊥ の型規則で表せることを示す。
した。この図は、古典論理での A ∨ ¬A の証明図 (図22) と図 20 に従ったものである。

6.1

SLC⊥ 項での古典論理

古典論理の形式体系 NK (図 2) を SLC⊥ の型規則で表したものを図 20 に示した。ここでは古典論理の型を持つ「項」を導出することを考えるので、型規則も項中心に記述している。

6.2

考察：継続の役割

6.1 節では項の型に注目し、その型が古典論理の推論規則を表せることで古典論理との対応を示した。しTInit は言わば > を導出するための規則である。 かし 6.1 節ではほとんど項に関する規則しか使ってい論理学において > を導出することには特には意味を ない。残りの継続に関する規則には、どのような意味成さない。しかし SLC⊥ の構文上、ダミー値 (ダミー があるのだろうか。
6.1 節では特に触れなかったが、図 20 の DNeg の導変数) が必要となる場合があるので、その際にはこの出には継続の規則が使われている。図 25 にその証明規則を用いる。
TVar は NK の Axm を表す。TAnd は NK の ∧I を、 図を示した。式中でも継続の関数 · · · ⇐ y や継続の
Fst、Snd は ∧E1 、∧E2 を表す。Inl、Inr は NK の 関数適用 ↓ が用いられているが、導出木中でも当然、∨I1 、∨I2 を表す。

それらに関する規則が使われている。また、これも特FPair が用いられている中段の証明図は、NK の に言明していないが inl 及び inr の本体は継続のパ∨E を表したものである。Γ, x1 : +A ` e1 : +C と ターンマッチ付き関数であるので、厳密にはこの関数
Γ, x2 : +B ` e2 : +C からそれぞれ関数を導出し、そ を導出するために TPFun が必要である。
古典論理式を SLC⊥ で証明するにあたり、必ずしれらを関数のペアにして e : +(A ∨ B) を渡している。
も図20 の規則に則る必要はない。例えば、図 20 では
計算理論的には match 文に式を渡す様子を表していRAA を関数 fDN で表しているが、継続を用いると図TFun、TFFun は NK の ⊃ I を、TApp は ⊃ E を表 23 のように表せる。導出木左上の Γ, y : ¬A ` e : +⊥す。⊃ I を表す規則が二種類あるのは、SLC⊥ では項 から、最下段の +A 型の項を導く形である。ここでと関数を明確に区別しており、それらに対する構文や は、変数 y の型 ¬A は古典論理の ¬A として扱う。
こちらの方が直感的には NK の導出規則に近い。
規則が異なるためである。

るものと言える。

図中の id は恒等関数 x ⇒ x : {+A→+A
TFClo は主に +(A → ⊥) 型の項、つまり古典論¬A←¬A (y ⇐ y で理での ¬A 型を導出するために用いる。DNeg は RAA もよい) を値扱いした dx ⇒ xe : +(A → A) のことであり、論理学的には > と等価である。型 ID は関を表すための公理である。Γ, fx : {+A→+⊥¬A←¬⊥ ` e : +⊥から TFFun と TFClo で Γ ` ddfx e ⇒ ee : +((A → 数の値扱い A → A を表す。紙面の都合上、このよう⊥) → ⊥) を導出し、DNeg の関数と TApp で関数適用 な略記をしている。これらは、項 e を変数 y の有効させることで +A 型の項を導出できる。ここで用い範囲に入れるためのダミー値である。また、図 23 のられている命題変数 A は図 17 の T の定義を満たし

RAA を用いるには継続の変数 y を用いて +⊥ 型の項

e を導くことになるので、図 20 に従うだけでは導出の関数は inl などと同様、SLC⊥ の型規則 (図 8 から はできず、継続に関する規則を用いることになる。
本論文ではあまり扱っていないが、直観主義論理のTInt をのぞいたもの) で前提なしで (Γ が空集合でも) 導出することが可能である。この関数は式が長い 導出規則 ⊥E を SLC⊥ で表すこともできる。図 24 にそれを示した。右下にある Γ ` e : +⊥ から、最下ので、以降 fDN と略記する。
ていれば、どんな論理式であってもよい。なお DNeg

以上より、次の定理を示すことができる。

段の +A 型の項を導出している。これは、図 23 の変
数 y が項 e に現れない場合と考えることができる。

Theorem 6.1
SLC⊥ の型規則で、古典論理の形式体系 NK を表す

導出された項では、ダミー値やダミー変数がなく、eことができる。

e : +⊥ の導出に仮定 y : ¬A を使っていない。このが y の有効範囲から外れている。つまり、図 24 では

Γ, x : S ` x : STVarΓ ` •⊥ : ¬⊥ TInitΓ ` e : +(A ∧ B)Fst
Γ ` e ↑ f st : +AΓ ` e1 : +A Γ ` e2 : +B
TAnd
Γ ` (e1 , e2 ) : +(A ∧ B)

Γ ` e : +AInl
Γ ` e ↑ inl : +(A ∨ B)
Γ, x1 : +A ` e1 : +CΓ ` x1 ⇒ e1 : {+A→+C
¬A←¬C

TFun

Γ ` e : +(A ∧ B)Snd
Γ ` e ↑ snd : +BΓ ` e : +BInr
Γ ` e ↑ inr : +(A ∨ B)

Γ, x2 : +B ` e2 : +CΓ ` x2 ⇒ e2 : {+B→+C¬B←¬C+(A∨B)→+CΓ ` [x1 ⇒ e1 , x2 ⇒ e2 ] : {¬(A∨B)←¬C

TFun
FPair

Γ ` e : +(A ∨ B)

Γ ` e ↑ [x1 ⇒ e1 , x2 ⇒ e2 ] : +C
Γ, x : +A ` e : +B

Γ, g : {+A→+B¬A←¬B ` e : +CΓ ` f : {+A→+B
Γ ` e : +A
¬A←¬B
TApp
Γ ` e ↑ f : +B

TFFun
TFun
+(A→B)→+CΓ ` x ⇒ e : {+A→+B
Γ ` dge ⇒ e : {¬(A→B)←¬C¬A←¬BΓ ` f : {+A→+B
¬A←¬B
TFClo
Γ ` df e : +(A → B)TApp

Γ ` (dge ⇒ dy ⇐ y 0 e ↑ g) ↓ •⊥ ⇐ y : {¬((A→⊥)→⊥)←¬A+((A→⊥)→⊥)→+A

DNeg

図 20: SLC⊥ における古典論理 NK の導出規則+(A∨(A→⊥))→+⊥※紙面の都合上 Γ = g : {¬(A∨(A→⊥))←¬⊥ , x : +A と略記している箇所があるTVarΓ ` x : +AInl
Γ ` x ↑ inl : +(A ∨ (A → ⊥))TApp+(A∨(A→⊥))→+⊥
g : {¬(A∨(A→⊥))←¬⊥ , x : +A ` x ↑ inl ↑ g : +⊥TFun+(A∨(A→⊥))→+⊥
g : {¬(A∨(A→⊥))←¬⊥ ` x ⇒ x ↑ inl ↑ g : {+A→+⊥
¬A←¬⊥
TFClo
+(A∨(A→⊥))→+⊥
g : {¬(A∨(A→⊥))←¬⊥ ` dx ⇒ x ↑ inl ↑ ge : +((A ∨ (A → ⊥)) → ⊥)Inr+(A∨(A→⊥))→+⊥
g : {¬(A∨(A→⊥))←¬⊥ ` dx ⇒ x ↑ inl ↑ ge ↑ inr : +(A ∨ (A → ⊥))
···∗
TVar
+(A∨(A→⊥))→+⊥
Γ ` g : {¬(A∨(A→⊥))←¬⊥+(((A∨(A→⊥))→⊥)→⊥)→+(A∨(A→⊥))` fDN : {¬(((A∨(A→⊥))→⊥)→⊥)←¬(A∨(A→⊥))+(A∨¬A)→+⊥+(A∨¬A)→+⊥g : {¬(A∨¬A)←¬⊥ ` g : {¬(A∨¬A)←¬⊥

DNeg

TVar

··· ∗ ∗∗+(A∨¬A)→+⊥g : {¬(A∨¬A)←¬⊥ ` dx ⇒ x ↑ inl ↑ ge ↑ inr ↑ g : +⊥TApp+((A∨(A→⊥))→⊥)→+⊥` dge ⇒ dx ⇒ x ↑ inl ↑ ge ↑ inr ↑ g : {¬((A∨(A→⊥))→⊥)←¬⊥

∗∗

TFFun

TFClo
` ddge ⇒ dx ⇒ x ↑ inl ↑ ge ↑ inr ↑ ge : +(((A ∨ (A → ⊥)) → ⊥) → ⊥)TApp
` ddge ⇒ dx ⇒ x ↑ inl ↑ ge ↑ inr ↑ ge ↑ fDN : +(A ∨ ¬A)
図 21: SLC⊥ における A ∨ ¬A の導出Axm¬(A ∨ ¬A), A ` A∨I1
Axm¬(A ∨ ¬A), A ` ¬(A ∨ ¬A)¬(A ∨ ¬A), A ` A ∨ ¬A
⊃E¬(A ∨ ¬A), A ` ⊥⊃I¬(A ∨ ¬A) ` ¬A
∨I2
Axm¬(A ∨ ¬A) ` ¬(A ∨ ¬A)¬(A ∨ ¬A) ` A ∨ ¬A
⊃E¬(A ∨ ¬A) ` ⊥RAA` A ∨ ¬A
図 22: NK における A ∨ ¬A の証明図
２つの導出木は、古典論理と直観主義論理の違いをSLC⊥ で端的に示しているものと思われる。
背理法 RAA は、本来成り立たないはずの仮定のもとで推論を行い、矛盾が生じるならその仮定を誤りと結論づけるものである。計算理論で言うと、導出できない（型エラーとなる）はずの式や型を用いて推論を進めなければならない。しかしそのような式や型は事実存在しないのであるから、背理法を用いるための推論自体ができないことになる。

SLC⊥ においても項のみで古典論理を表すことは不可能である。しかし項では表せない背理法の仮定を継続から借りることにより、背理法による推論を可能にしているように思える。図 23 がそれにあたる。
図 23 の左上の Γ, y : ¬A ` e : +⊥ は、項では表せない背理法の仮定を継続の変数 y : ¬A で表し、それを用いてたどり着いた結論と考えられる。継続の型¬A の意味が「+A 型の項を受け取る継続」であることも軽視できない。つまり、¬A 型の継続の存在はす
なわち、+A 型の項の存在を示唆しているように思える。実際、この項に ¬A 型の継続を与えると、それが e 中の変数 y に代入され、いずれは ¬A 型の継続に +A 型の項が渡るであろうことが予想される。
一方図 24 は、図 23 と似た項を導出するが、e : +⊥と変数 y : ¬A は全く関係がなく、導出された項は与えられた ¬A 型の継続を完全に捨ててしまう。この
挙動は、+A 型の項の存在に対して非常に否定的であるように見える。

SLC⊥ と古典論理の関係における継続の意義は、¬A型でありながら +A 型に対して肯定的な仮定を与えることにあると思われる。古典論理と関係する計算理論は、SLC⊥ の他にも多く存在するが、これらにも¬A でありながら A を許容するような構造があるのではないかと推測する。

参考文献[1] Curien, P. and Herbelin, H. “The duality of computation,” Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming(ICFP’00), pp. 233–243 (2000).
[2] Felleisen, M., and Hieb, R. “The Revised Reporton the Syntactic Theories of Sequential Control
and State,” Theoretical Computer Science, Vol. 103,
No. 2, pp. 235–271 (September 1992).
[3] Filinski, A. “Declarative Continuations and Categorical Duality,” Master’s thesis, DIKU Report
89/11, University of Copenhagen (August 1989).
[4] Griﬃn, T. “A Formulae-as-Types Notion of Control,” 17’th Symposium on Principles of Programming Languages (POPL’90), pp. 47–58 (January1990).
[5] 小野寛晰「情報科学における論理」日本評論社 (April
1994).
[6] Parigot, M. “λµ-calculus: An Algorithmic Interpretation of Classical Natural Deduction,” In A.
Voronkov, editor, Logic Programming and Automated Reasoning (LNCS 624), pp. 190–201 (July
1992).
[7] Pierce, B. C. Types and Programming Languages,
Cambridge: MIT Press (2002).
[8] 阪上紗里, 浅井健一「対称λ計算の基礎理論」コンピュー
タソフトウェア, Vol. 26, No. 2, pp. 3-17 (May 2009).
[9] 上田やよい, 浅井健一「型付き対称λ計算における論理
積と論理和の導入」第 11 回 プログラミング及びプロ
グラミング言語ワークショップ, ポスター発表 (March2009).
[10] Wadler, P. “Call-by-value is dual to call-by-name,”
Proceedings of the eighth ACM SIGPLAN International Conference on Functional Programming(ICFP’03), pp. 189–201 (August 2003).
[11] Wadler, P. “Call-by-value is dual to call-by-name,
Reloaded,” In J. Giesl, editor, Term Rewriting
and Applications (LNCS 3467), pp. 185–203 (April2005).

Γ, y : ¬A ` e : +⊥WeakΓ, y : ¬A, x : +ID ` e : +⊥TFun
+ID→+⊥
Γ, y : ¬A ` x ⇒ e : {¬ID←¬⊥Γ, y : ¬⊥ ` •⊥ : ¬⊥ TInitTAppΓ, y : ¬A ` (x ⇒ e) ↓ •⊥ : ¬IDTFunΓ ` (x ⇒ e) ↓ •⊥ ⇐ y : {+ID→+A¬ID←¬AΓ ` id ↑ ((x ⇒ e) ↓ •⊥ ⇐ y) : +AΓ ` id : +ID

IDFun
TApp

図 23: RAA の SLC⊥ での導出木

Γ, y : ¬A ` •⊥ : TInit
TFunΓ ` •⊥ ⇐ y : {+⊥→+AΓ ` e : +⊥
¬⊥←¬A
TApp
Γ ` e ↑ (•⊥ ⇐ y) : +A
図 24: ⊥E の SLC⊥ での導出木

y : ¬A, g : {¬(A→⊥)←¬⊥ , y 0 : ¬⊥ ` y : ¬A+(A→⊥)→+⊥y : ¬A, g : {¬(A→⊥)←¬⊥ ` y ⇐ y 0 : {+A→+⊥¬A←¬⊥+(A→⊥)→+⊥+(A→⊥)→+⊥+(A→⊥)→+⊥y : ¬A, g : {¬(A→⊥)←¬⊥ ` g : {¬(A→⊥)←¬⊥

TVar

TVar

TFun

y : ¬A, g : {¬(A→⊥)←¬⊥ ` dy ⇐ y 0 e : +(A → ⊥)+(A→⊥)→+⊥y : ¬A, g : {¬(A→⊥)←¬⊥ ` dy ⇐ y 0 e ↑ g : +⊥+(A→⊥)→+⊥y : ¬A, g : {¬(A→⊥)←¬⊥ ` dy ⇐ y 0 e ↑ g : +⊥+(A→⊥)→+⊥TFFuny : ¬A ` •⊥ : ¬⊥ TInit
TAppy : ¬A ` (dge ⇒ dy ⇐ y 0 e ↑ g) ↓ •⊥ : ¬((A → ⊥) → ⊥)+((A→⊥)→⊥)→+A TFun
` (dge ⇒ dy ⇐ y 0 e ↑ g) ↓ •⊥ ⇐ y : {¬((A→⊥)→⊥)←¬Ay : ¬A ` dge ⇒ dy ⇐ y 0 e ↑ g : {¬((A→⊥)→⊥)←¬⊥+((A→⊥)→⊥)→+⊥

図 25: SLC⊥ における ¬¬A ⊃ A の導出※紙面の都合上 Γ = y1 : ¬A, y2 : ¬(A → ⊥) と略記している箇所がある

TVar
TFun
Γ, x : +ID ` y1 ⇐ y : {+A→+⊥
¬A←¬⊥
TFClo
Γ, x : +ID ` dy1 ⇐ ye : +(A → ⊥)
TFun
TVar
+ID→+(A→⊥)Γ ` x ⇒ dy1 ⇐ ye : {¬ID←¬(A→⊥)Γ ` y2 : ¬(A → ⊥)TApp
Γ ` (x ⇒ dy1 ⇐ ye) ↓ y2 : ¬ID
Γ, x : +ID, y : ¬⊥ ` y1 : ¬A

y1 : ¬A, y2 : ¬(A → ⊥) ` (x ⇒ dy1 ⇐ ye) ↓ y2 : ¬ID+ID→+(A∨(A→⊥))` (x ⇒ dy1 ⇐ ye) ↓ y2 ⇐ (y1 , y2 ) : {¬ID←¬(A∨(A→⊥))TPFun` id : +ID` id ↑ ((x ⇒ dy1 ⇐ ye) ↓ y2 ⇐ (y1 , y2 )) : +(A ∨ (A → ⊥))図 26: SLC⊥ における A ∨ ¬A の導出 (2)

IDFun
TApp

TFClo
TApp