古典論理のカリー・ハワード対応での証明の書き換えと簡約

「古典論理のカリー・ハワード対応のためのラムダ計算」のつづき。
(本文中、証明図の中の式の位置や大きさが変になっているところがあるけど、直すのが面倒なので変なままになっている)
直観主義論理の自然演繹の証明図を書き換えによって簡単化することと、ラムダ計算での簡約(リダクション)との間には対応関係があった(「直観主義論理のカリー・ハワード対応」)。同様の対応関係が古典論理の場合でも成り立つ。

ブロックに関係する書き換え

証明に次のような場所があったとする。
$\begin{array}{c} \vdots \\ \{ A \quad A \} \\ \hline A \\ \vdots \\ B \end{array}$ 。この証明は、 $\begin{array}{c} \vdots \\ \{ A \quad A \} \\ \vdots \\ \{ B \quad B \} \\ \hline B \end{array}$ と書き換えることができる。
同様の書き換えをラムダ計算の証明図に対しておこなう。すると
$\begin{array}{c} \vdots \\ t \quad :A \qquad E_1\{\alpha\} \quad :A \\ \hline \mu \alpha . t \left[ [ \alpha ]\bullet \leftarrow [ \alpha ] E_1 \{ \bullet \} \right] \quad : A \\ \vdots \\ E_2 \{ \mu \alpha . t \left[ [ \alpha ]\bullet \leftarrow [ \alpha ] E_1 \{ \bullet \} \right] \} \quad : B \end{array}$ という証明図が、 $\begin{array}{c} \vdots \qquad \qquad \qquad \\ t \quad :A \qquad E_1\{\alpha\} \quad :A \\ \vdots \qquad \qquad \qquad \\ E_2 \{t \} \quad : B \qquad E_2 \{ E_1 \{ \alpha \}\} \quad : B \\ \hline \mu \alpha . E_2 \{t \left[ [ \alpha ] \bullet \leftarrow [ \alpha ] E_2 \{ E_1\{ \bullet \} \}\right] \} \end{array}$ に書き換わる。ただし $E_2$ で新たに使われているラベルと重複しないように、ラベルαはあらかじめ書き変えをおこなっておく。
ごちゃごちゃしていてわかりにくいけど、 $t' = t \left[ [ \alpha ]\bullet \leftarrow [ \alpha ] E_1 \{ \bullet \} \right]$ とおくと次のようになる。

$\begin{array}{c} \vdots \\ t \quad :A \qquad E_1\{\alpha\} \quad :A \\ \hline \mu \alpha . t' \quad : A \\ \vdots \\ E_2 \{ \mu \alpha . t' \} \quad : B \end{array}$ という証明図が、 $\begin{array}{c} \vdots \qquad \qquad \qquad \\ t \quad :A \qquad E_1\{\alpha\} \quad :A \\ \vdots \qquad \qquad \qquad \\ E_2 \{t \} \quad : B \qquad E_2 \{ E_1 \{ \alpha \}\} \quad : B \\ \hline \mu \alpha . E_2 \{t' \left[ [ \alpha ] \bullet \leftarrow [ \alpha ] E_2 \{ \bullet \}\right] \} \end{array}$ に書き換わる。

直観主義論理の場合と違って証明図の書き換えが下側に向かっておこなわれるので、ラムダ計算の方でも書き換える項μα.tの外側まで考慮に入れる必要がある。
ここでおこなった書き換えの最後の行は、

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

という形の書き換えになっている。これは「古典論理のカリー・ハワード対応のためのラムダ計算」に書いたブロック構文の書き換え規則そのもので、古典論理の書き変えとラムダ計算の書き換えが対応している。またこの書き換えでは、論理式を一つにまとめるのを遅らせ同じ証明を繰り返しおこなう(項の中にE{ }が複数回あらわれる)ように書き換えている。これが古典論理に対応させたラムダ計算で同じ箇所を繰り返し実行できる理由になっている。

ジャンプに関係する書き換え

古典論理の証明で、結論の論理式がいったん増えた後、ふたたび一つに融合したとする。つまり、
$\begin{array}{c} \vdots \\ A \\ \hline \{ \bot \quad A \} \\ \vdots \\ \{ B \quad B \} \\ \hline B \\ \vdots \end{array}$ という形になっていたとする。これを見ると、 $\begin{array}{c} \bot \\ \vdots \\ B \end{array}$ の部分を削って、 $\begin{array}{c} \vdots \\ A \\ \vdots \\ B \\ \vdots \end{array}$ に書き換えてよいように見える。しかしそれは一般的にはおこなえない(おこなえるとしたら直観主義論理の範囲で全て証明できることになってしまう)。問題は、Bが証明された時点で何が仮定に残っているのかということで、もし $\begin{array}{c} \bot \\ \vdots \\ B \end{array}$ の部分を除いても、Bの時点での仮定されていることが変わらない(つまり $\bot$ からBまでの証明で取り除いた仮定は、AからBまでの証明の方でも取り除いている)場合は、 $\bot$ からBまでを削っても良い。
この書き変えをラムダ計算でおこなう。

$\begin{array}{c} \vdots \\ s \quad : A \\ \hline [ \alpha ] \quad : \bot \qquad \alpha :A \\ \vdots \\ t \quad : B \qquad \qquad E \{ \alpha \} \quad : B \\ \hline \mu \alpha . t' \quad : B\end{array}$ は条件を満たす場合、 $\begin{array}{c} \vdots \quad \\ s \quad : A \\ \vdots \quad \\ E\{s\}\quad : B\end{array}$ と書き換えることができる。

この最後の行の部分の書き換えは、

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

と書ける。ただし[α]E{s}の外側をE'と書いた。これは前に与えたジャンプに対する書き換え規則とほぼ同じである。前はラベルには触らない場合だけ考えたので、

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

という形だった。ジャンプによる書き換えは、古典論理の証明を直観主義論理の証明に書き換えることになっている。
このジャンプがおこなえる条件について考える。条件は「左側の式で取り除いた仮定は右側の式でも取り除いていること」だった。
仮定は→導入か∨除去で取り除かれる。これは変数が束縛されるということである(→除去ならλx.…によって)。よって左側で取り除かれた仮定が右側でも使われているというのは、左側で束縛した変数は右側でも束縛されていることに等しい。一方、最後に出てくるt'にはE{s}が埋め込まれる。ということは、t'の中で左側の証明でおこなった変数束縛は、右側でおこなった変数束縛より外側になる。
たとえば、μα.( … λx.( λy.( … [α](λx.s) …)))だと、最初のλxとλyは左側の証明による束縛で、最後のλxは右側の証明による束縛。
したがって条件を満たす場合、左側の証明でおこなわれる束縛は右側でもおこなわれている。このことから、E{s}の自由変数がtによって束縛されていなければ書き換えがおこなえることがわかる(先にEによって束縛されるから)。書き変えをおこなうと[α]からμαまでの間にある部分を削ることになるので、削ろうとしている式によって束縛されている場合は削ることができない、ということになる。
なお通常のプログラミング言語の場合、λ式の中は(関数適用によってλが消えるまで)そもそも書き換えをおこなわない。したがってここでの条件を考慮する必要はない。

たとえば、次の排中律を表す項の場合、このままでは[α](Left x)のxがμαとのあいだにあるλの束縛内にいるのでジャンプはおこなえない。(Left x)のxが別のものならばジャンプできる。通常のプログラミング言語の場合は、ラムダの内側はさわらないので条件を考える必要もなくジャンプできない。もしも型がAのデータがあればそれと組み合わせて簡約を進めるとλが消えるかもしれない。そのときはジャンプをすることができる。
$\begin{array}{cc} [x \quad : A ]{}_{\small{1}} & \\ \hline {\rm Left} \; x : A \vee \neg A & \\ \hline {[ \alpha ] ({\rm Left}\;x) \quad : \bot \;}_{ \small{1}} & \alpha \quad :A \vee \neg A \\ \hline \lambda x . [\alpha ]({\rm Left}\;x) \quad : \neg A & \alpha \quad : A \vee \neg A \\ \hline {\rm Right}\;\lambda x . [\alpha ]({\rm Left}\;x) \quad : A \vee \neg A & \alpha \quad : A \vee \neg A \\ \hline \mu \alpha .( {\rm Right}\;\lambda x . [\alpha ]({\rm Left}\;x)) \quad : A \vee \neg A & \end{array}$

古典論理に拡張することによるラムダ計算への影響

このようにブロックについてもジャンプについても、古典論理の証明図の書き変えと項の簡約が対応している。

また、古典論理に拡張したラムダ計算では計算結果が複数ありえるようになる理由もわかる。
たとえば、
f:id:lemniscus:20190106161725g:plain

のようになっていた場合、関数適用を先におこなえばジャンプ構文[α]は消え、ジャンプを先におこなえば関数適用の部分が消える(call-by-nameなら前者、call-by-valueなら後者)。
直観主義論理では証明の書き換えの影響が出るのは必ず証明の上側だけだった。でも古典論理では書き変えの影響が下にも出るようになる。そのため、書き換えをおこなう地点が互いを消し合う場合が出てくるので、結果も複数ありうることになる。
それから、証明のある点から下側というのは、項で考えるとその項の外側つまりその項の文脈・継続にあたる。したがって証明の下側を書き換えることによる影響は、項の場合はその項の継続に対して現れることになる。ラムダ計算を古典論理に拡張したときにcall/ccのような継続に関係あるものが出てきたのも、古典論理の証明の書き換えが証明の下側にも影響することが原因だといえる。