古典論理のカリー・ハワード対応のためのラムダ計算

「call/ccと古典論理のカリー・ハワード対応」では、型付きラムダ計算にcall/ccを追加して古典論理との対応づけをしたけど、公理の追加ではなく推論規則を追加する形で古典論理との対応づけをしたい。
(本文中、証明図の中の式の位置や大きさが変になっているところがあるけど、直すのが面倒なので変なままになっている)

ラベル付きブロック

call/ccの説明に使ったラベル付きブロック構文を使って考える。次のような構文だった。

:α{
 ...
 jump α t;
 ...
}

まず「jump α t」を見る。「jump α t」を実行するとそこには実行が戻ってこないので、型は $\bot$ である。そしてtの型をAとしておくと、jumpに関する推論規則を次のようになるだろう。
$\frac{\large{t \quad :A \qquad \quad \alpha \quad : ? }}{\large{{\rm jump}\: \alpha \: t \quad : \bot}}$
この式は¬除去則
$\frac{\large{A \qquad \neg A }}{\large{\bot}}$
と似ている。そうするとラベルαの型は¬Aとするのが良いだろう。これは継続の型が¬A (=A→ $\bot$ )だったこととも合っている。

$\frac{\large{t \quad :A \qquad \quad \alpha \quad : \neg A }}{\large{{\rm jump}\: \alpha \: t \quad : \bot}}$

一方、ラベル付きブロックの構文はラムダ式に似ている

λx.(
  ...
)

ラムダ式についての推論規則は
$\frac{\large{\begin{array}{c}[x \quad : A ]{}_{\small{1}} \\ \vdots \qquad \\ t \qquad : B \end{array}} }{\large{\lambda x .t \qquad : A \to B}}\small{1}$
というものだった。ブロックの場合は、変数の代わりにラベルが仮定されたので、推論規則によってラベルに関する仮定を消せば良い。

$\frac{\large{\begin{array}{c}[\alpha \quad : \neg A ]{}_{\small{1}} \\ \vdots \quad \\ t \qquad : A \end{array}} }{\large{ :\alpha \{t\} \qquad : A }}\small{1}$

ここに現れた推論規則「¬Aを仮定してAを導けるなら、Aを導いてよい」というのは、call/ccの型「(¬A→A)→A」を推論規則に直したものになっている。
このように、公理ではなく推論規則の形で型付きラムダ計算に機能を追加できたけど、さらに変更を加える。

別の新しい規則

「直観主義論理の「自然さ」(3)古典論理のシーケント計算と自然演繹」の後半で、自然演繹を古典論理にする別のやり方を書いた。それは、結論に複数の論理式を置けるようにした上で、次の二つの規則を追加するというものだった。
一つは、結論に任意の論理式を追加してよい、という規則。

$\frac{\large{\begin{array}{c} \vdots \\ \{P_1, \ldots, P_n \} \end{array}}}{\large{ \{\bot, P_1, \ldots, P_n \} }}$

(矛盾からは任意の式を導いてよいので、 $\bot$ を追加する規則さえあればよい)
もう一つは、同一の結論は一つにまとめてよい、という規則。

$\frac{\large{\begin{array}{c} \vdots \\ \{A , A, P_1, \ldots, P_n \} \end{array}}}{\large{ \{A, P_1, \ldots, P_n \} }}$

一見しただけではわかりにくいけど、この二つの規則はjumpとブロックの規則に対応している。これは推論規則をシーケントの形で書くとわかりやすい。
jumpとブロックの規則から型の部分を取り出してシーケントの形で書くと次のようになる。
jump
$\frac{\large{\cdots \Rightarrow A \qquad \neg A \Rightarrow \neg A }}{\large{\ldots , \neg A \Rightarrow \bot}}$
ブロック
$\frac{\large{\ldots , \neg A \Rightarrow A}}{\large{\qquad \qquad \qquad \ldots \Rightarrow A}}$
新しい規則をこれに合わせて書くとこうなる。
jump (新しい式を結論に追加してよい)
$\frac{\large{\cdots \Rightarrow A}}{\large{\cdots \Rightarrow \bot , A}}$
ブロック (同一の式を一つにまとめてよい)
$\frac{\large{\ldots \Rightarrow A, A}}{\large{ \ldots \Rightarrow A}}$
左側にあった¬Aを右側に移して¬を外した形に(だいたい)等しい。

なので、jumpとブロックの規則をこちらの規則の形に書き直す。ついでにjumpとブロックのシンタックスも変える。jump α t の代わりに[α]tと書き、:α{t}の代わりにμα.tと書くことにする。

ジャンプ構文についての規則は次のようになる。

$\frac{\large{ \{s \quad : A \qquad \cdots\} }}{\large{ \{ [\alpha ] s \quad : \bot \qquad \alpha \quad : A \qquad \cdots \} }}$

ブロック構文(ミュー式?)の規則は次のようになる。

$\frac{\large{\{ t \quad : A \qquad \alpha \quad : A \qquad \cdots\} }}{\large{\{\mu \, \alpha . t \quad : A \qquad \cdots \} }}$

( $\cdots$ と書いてあるのは、ほかのラベル。以下では $\cdots$ や{ }は適当に省略する)。

これでラムダ計算を拡張した別の計算体系ができた。これは

Michel Parigot「λμ-calculus: An Algorithmic Interpretation of Classical Natural Deduction」(1992)

に出てくるラムダミュー計算(λμ計算)と見た目は同じものだけど、推論規則が違っている。
たとえばcall/ccは、ここで説明した規則ではλy.μα.(y(λx.[α]x))と定義できる。
$\frac{\frac{\frac{\frac{\frac{\large{ [ x \quad : A]{}_{\small{1}} \qquad \qquad }}{\large{ \{ [\alpha ]x \; : \bot \qquad \alpha \; : A \} }}}{\large{ \{ \lambda x . [ \alpha ] x \; : A \to \bot \qquad \alpha \; : A \}}}{\small{1}} \qquad {\large{ [ y \; : (A \to \bot) \to A ]{}_{\small{2}} }}}{\large{ \{ y(\lambda x . [ \alpha ] x) \; : A \qquad \alpha \; : A \} }}}{\large{ \mu \alpha .(y(\lambda x . [ \alpha ] x)) \; : A }}}{\large{ \lambda y . \mu \alpha .(y(\lambda x . [ \alpha ] x)) \; : (( A \to \bot) \to A) \to A }}{\small{2}}$
一方、Parigotの論文では、call/ccにあたるものが　λy.μα.[α](y λx.μδ.[α]x)になっている。
さらにもう少し変更を加える。
上の規則の元では、ブロック部分に対する証明図は次のようになる。

$\frac{\frac{\large{s \quad : A}}{\large{\begin{array}{c} [\alpha ] s \quad : \bot \qquad \alpha \quad : A \\ \vdots \\ \quad t \quad : A \qquad \qquad \alpha \quad : A \end{array}}}}{\large{\quad \mu \, \alpha . t \quad : A}}$

ラベルが現れてから最後のμ式の規則になるまで、ラベルには推論規則は適用されない。でも自然演繹の証明では、複数ある式のどれに対して演繹規則を適用してもよい。つまりこのままでは、ラムダミュー計算の証明図と自然演繹の証明図がきちんと対応していないことになる。
そこで、ラベルの式に対しても自由に演繹規則を適用してよいことにして、ジャンプ規則を拡張する。その前に新しい表記を導入しておく。

文脈、あるいは継続

通常のラムダ計算では項の書き換えはその項の内部だけを考慮すればよかったけど、ブロック構文・ジャンプ構文の書き換えでは項の外側も考慮する必要があるので、新しい表記を導入する。

例えば項sは、λx.(Left s, x)という項の一部になっている。この場合、λx.(Left s, x)からsを取り除いたものを
λx.(Left {}, x)
と書くことにする(つまり項を取り除いた部分を{}で示す)。また、
E = λx.(Left {}, x)
としたとき、もとの項をE{s}と書けることにする。このときEは項sの外側を表している。
このEのことをsの文脈あるいは継続と呼ぶ(このE{}自体がさらに別の項の一部になっている場合も考えるので、部分文脈・部分継続と呼んだ方がよいかもしれない)。

この表記を使うと、ブロック規則は次のようになる。

まず、ブロック規則を適用できるのは、証明が次のような形になっているとき。前の規則と違ってラベルに対しても演繹規則を適用してもよい。

$\frac{\large{s \quad : A}}{\large{\begin{array}{c} [\alpha ] s \quad : \bot \qquad \alpha \quad : A \\ \vdots \\ \quad t \quad : B \qquad \qquad E \{ \alpha \} \quad : B \end{array}}}$

演繹機則の適用によってラベルαは項E{α}の一部になっている。また前のブロック規則とは違って、ラベルの型とブロックの型は同じでなくてもよい。
ブロック規則は、この形の式があったときに、まず項tの中に出てくる[α]sを[α]E{s}と書き換える(つまりラベルに適用した推論規則を項sに適用した形にする)。そいて書き換えたものをt'として、
μα.t' : B
が結果として導かれる。よって規則は次のようになる。

$\frac{\frac{\large{s \quad : A}}{\large{\begin{array}{c} [\alpha ] s \quad : \bot \qquad \alpha \quad : A \\ \vdots \\ \quad t \quad : B \qquad \qquad E \{ \alpha \} \quad : B \end{array}}}}{\large{\mu \, \alpha . t \left[ [ \alpha ]s \leftarrow [ \alpha ] E \{ s \} \right] \quad : B}}$

ブロック規則自体は下の部分だけど、ラベルの導入部分も書いておいた。
この規則は実質的には、 $\frac{\frac{\large{A}}{\large{\begin{array}{c} \bot \qquad A \\ \vdots \\ B \qquad B \end{array}}}}{\large{B}}$ という証明を、 $\frac{\frac{\large{\begin{array}{c} A \\ \vdots \\ B \end{array}}}{\large{\begin{array}{c} \bot \qquad B \\ \vdots \\ B \qquad B \end{array}}}}{\large{B}}$ に書き換えた上で、元のブロック規則を適用した場合に等しい。そのため、最終的に得られた項が、まず項[α]E{s}を作ってからその後にブロック規則を適応した項と区別がつかない。そのため正確にはラムダミュー計算の証明図と自然演繹の証明図が対応していない。[α,E{α},s]みたいな表記を導入してもよいのだけど、その場合sがE{}のスコープに入っていることに注意がいる。

ブロックとジャンプの書き換え規則

新しい表記を導入したので、ブロックとジャンプについての書き換え規則を書くことができる。
まずブロック構文μの規則は次のようになる。

${ E \left\{ \mu \alpha . t \right\} \quad \Rightarrow \quad \mu \alpha .\left( E \left\{t \left[ [ \alpha ]s \leftarrow [ \alpha ] E\{ s \} \right] \right\} \right) }$

ただし、Eはラムダ式全体を表す(Eの外側には何もない)。これはμを一番外側に移動させている。したがって一番外側にあるμに対しては書き換えはおこなえない。また、外側に移動させるときに、元は外側にあったラベルと名前が重なってしまう場合がある。そのときは、あらかじめラベルの名前を変更してから外側に移動させる。そのあたりは、変数名の書き換えと同じようにすればよいはず。

一方、ジャンプ構文[ ]の規則は次のようになる。ただし、この規則は他の書き換えとは異なり、必ず使えるわけではなく使える条件がある。

$\mu \alpha . ( E \left\{ [ \alpha ]s \right\}) \quad \Rightarrow \quad s$

書き換えで、ジャンプ元の[α]からジャンプする先μαまでの中間にある部分を消している。この消している部分のλ項のスコープに[α]が入っている場合、書き換えはおこなえない。例えば
μα.(…λx.( …[α]s…))
となっている場合には、書き換えはおこなえない。この条件は、Schemeなど普通のプログラミング言語のでは関数適用されるまでラムダ項の内部にはさわれないので必ず成り立つ。でも、一般のラムダ計算の書き換えではどこから書き換えてもよいので、この条件を考慮する必要がある。
また普通の実行順序では(call-by-valueでもcall-by-nameでも)、まずブロックμを評価してから[ ]を評価してジャンプするという実行順序になるけど、別に先に[ ]を評価してもかまわない。

このように書き換え規則を定義すると、古典論理の自然演繹の証明図の書き換えの対応関係をつけることができる。対応関係を観察すると、なぜ古典論理に対応させたラムダ計算では、なぜ複数の簡約結果が生じるようになる(合流性を満たさなくなる)のかとか、なぜ項の同じ部分が繰り返し簡約できるようになったのかの理由がわかってくる。
(「古典論理のカリー・ハワード対応での証明の書き換えと簡約」につづく)