call/ccと古典論理のカリー・ハワード対応

call/ccと継続

call/ccというのは、gotoを強力にしたものだと思っておけば良い。ただしScheme以外のプログラミング言語では、あまり見かけない機能。

例えばブロック構造から抜け出すための命令がある言語を考える。どのブロックから抜け出すかはラベルで指定する。またラベルはギリシャ文字で表すことにする。とりあえず次のような感じになるだろう。jumpの部分を実行するとブロックから抜け出す。

:α{
  ...
  ...
  jump α;
  ...  // ここは実行されない
}

でも、ブロック自体が値を持っている(値を返す)ようにした方が汎用的になる。例えば、次のプログラムはflagが真ならxに1が代入され、偽なら2が代入される。

x = :α{
  ...
  ...
  if (flag) {
    jump α 1;
  }
  ...
  2;
}

値を返すにしても返さないにしても、これだけ見るとラベルというのは単なる名前に過ぎないように見える。でもこのラベル自体を変数に代入したり関数に渡したりできるようにすると、単なる名前ではなくなる。次のようなプログラムを考える。なおfunから始まる部分は関数定義とする。

fun f(label) {
  y = :β{  // とりあえずは、ここのラベルのことは無視していい
    ...
    jump label 1;
    ...
  }
}

x = :α{
  f(α);
  ...   // ここは実行されない
}

このプログラムでは、ブロック内部で関数fを呼び出していて、そこでラベルαを引数として渡している。そして関数fの内部でjump命令を実行している。そのとき使うラベルは、引数として渡されたラベルなので、一気に関数から脱出しブロックを抜けxに1が代入される。
これだけならまだラベルを名前に過ぎないと考えても問題ないように見えるかもしれない。でも例えば、関数fは再帰呼び出しでf自身を呼び出しているとする。そうすると再帰呼び出しごとにβというラベルのブロックが現れることになる。しかも、それらのラベルは名前は同じだけどそれぞれ区別しなければならない。そうしないとjumpするときに正しい位置に戻れなくなる。
さらにラベルを大域変数に代入しておけば、jumpによってブロックの外側からしかも何度もブロックから出る所に実行位置を移すことができる。
こうした動作を可能にするためには、ブロックに入った時点での制御情報(どの関数を順に呼び出している最中なのかという情報)を記録してラベルと結びつけておかないといけない。この情報のことを継続という。ラベルが単なる名前ではなく継続と結びついていることによって、正しいジャンプが可能になる。
それから、ここではjump命令というのを考えたけど、ラベルを関数のように扱いジャンプを関数呼び出しの形にするという文法にすることもできる。つまり

x = :α{
  ...
  jump α 0;
  ...
}

と書くのではなく、

x = :k {
  ...
  k(0);
  ...
}

と書く。このような書き方をすると、あまりラベルという感じがしないので、ギリシャ文字ではなくラテン文字に変えた。普通は、ラベルとは呼ばずに継続と呼ぶ。
(ただし関数呼び出しの形にするかどうかは継続と呼ぶかどうかとは関係ない。SML/NJでは、「jump k v」「k(v)」にあたる部分を「throw k v」と書くけど、kは継続と呼ばれる)
そして、Schemeではラベル付きブロック構造の代わりにcall/cc(正式名称call-with-current-continuation)という関数を使って、同等の機能を提供している。

:k {
 ...
}

と同じことを

call/cc λk.(
  ...
)

のように書く(実際にはこういう文法ではないが)。これは「λk.( ... )」という関数を引数にして、call/ccという関数を呼び出している。関数call/ccはラベル付きブロックと同じ機能を実現する。つまり、その時点での継続(≒制御情報≒ラベル)を引数にしてλk.( ... )を呼び出す。

call/ccの型

次のような場合を考えてみる。

int x;
x = call/cc λk.(
  ...
  k(1)
  ...
  2;
)

xは整数型である。関数λk.(...)が最後まで実行された場合はその値がxに代入される。したがってλk.(...)は「? → int」という型でないといけない(「?」は変数kの型)。プログラムで2を返しているのは、これに適合している。
また途中でkが呼ばれた場合、その値がxに代入される。したがってkの型は「int → ??」でないといけない(プログラムでは1をkの引数にしている)。ではkの戻り値の型は何かというと、kを呼び出すとそこからジャンプしてしまい、その位置には戻らない。実行が戻ってこない位置の型なので、これを $\bot$ 型だと考える。実行が来ないからそこの位置をどんな型にしても問題ないというのが、 $\bot$ からは何でも導けるという推論規則に対応する。
なので、λk.(...)の型は「(int → $\bot$ ) → int」になる。そしてcall/ccは、「(int → $\bot$ ) → int」型の引数を受け取りintの値を返すので「((int → $\bot$ ) → int) → int」型となる。ここではint型にしたけれど他の型でも問題ないので一般的にcall/ccの型は

call/cc : ((A→ $\bot$ ) → A) → A

となる(型Aそれぞれに対してcall/ccがあると考える)。
ここに出てきた「((A→ $\bot$ ) → A) → A」というのは、直観主義論理に追加すると古典論理になるような公理のうちのひとつである。ということは、型付きλ計算の体系にcall/ccを追加したものは、古典論理と対応が付くと考えることができる。つまりcall/cc付き型付きλ計算では、古典論理で証明できる命題の表すデータ(項)が存在することになる。

排中律について

直観主義では、A∨Bが証明できる場合は、必ずAが証明できるかBが証明できた。したがって排中律A∨¬Aが証明できるのは、Aか¬Aのどちらかが証明できる場合に限られる。
一方、古典論理では、Aも¬Aもどちらも証明できないときでもA∨¬Aが証明できる。これを型付きλ計算に移して考えると「call/ccを加えると、A型のデータも¬A型のデータも存在しない場合でもA∨¬A型のデータが存在する」という何だかおかしな結論が得られるように思える。これについて考えてみる。
例えばAが証明できる(A型の項が存在する)とする。その場合、(A→ $\bot$ )→Aも証明できるので、(A→ $\bot$ )→A型の関数fを使ってcall/ccを呼び出すことができる。call/ccを呼び出すと、call/ccはA→ $\bot$ 型の継続を引数にしてfを呼び出す。ここがポイントで、この継続は項としては存在しない。そもそもこの場合A→ $\bot$ 型の項は存在しない(Aは証明できるとしたことと、古典論理が無矛盾であることによる)。
つまりcall/ccを呼び出すと、項としては存在しないデータを使うことができる。これがA型の項も¬A型の項も存在しなくてもA∨¬A型の項が存在できる理由になる。とはいっても型の制約があるので、call/ccで¬A型の継続を得てそのまま直和型を作ってcall/ccの外に出すということはできない。
call/ccの型( (A→ $\bot$ )→A) →Aというのは、「A→ $\bot$ 型のデータを元にしてA型のデータを作ることができるなら、call/ccはA型のデータを返してくれる」と解釈することができる。これを念頭において、実際にcall/ccを使ってA∨¬A型の項を作ってみる。
欲しいのは¬A型のデータである。これはA→ $\bot$ 型と同じである。A→ $\bot$ 型のデータは、「A→?」型データと「?→ $\bot$ 」型データがあれば手に入る。「A→?」で証明できるものというと「A→A∨??」というのが考えられる。そうすると、まず「A→A∨¬A」を考えるのが良いだろう。
λx.(Left x) : A→A∨¬A
「A∨¬A→ $\bot$ 」型データはもちろんcall/ccによって得る。
call/cc : (((A∨¬A)→ $\bot$ ) → A∨¬A) → A∨¬A
「(A∨¬A)→ $\bot$ 」型の引数をkとしておく。
kとλx.(Left x)との合成関数はλy.(k (λx.(Leftx))y)になるけど、これはλx.(k(Left x))と書き直せる。
λx.(k(Left x)) : A→ $\bot$ (= ¬A)
となり、欲しかった¬A型のデータが得られた。これを使って
Right λx.(k(Left x)) : A∨¬A
となり、
λk.(Right λx.(k(Left x))) : ((A∨¬A)→ $\bot$ )→A∨¬A
が得られる。この式をcall/ccに渡せば
call/cc(λk.(Right λx.(k(Left x)))) : A∨¬A
となり排中律を表す項が得られた。
この過程を証明図の形にすれば、(A→¬A)→Aを公理としたときの排中律の証明となる。

f:id:lemniscus:20190106160912g:plain

call/cc追加による問題

例えば、次のようなプログラムを考える。

x = :k{
  f( g(k(1)), k(2))
}

このプログラムでは、k(1)とk(2)のどちらが先に実行されるかによって、xに代入される値が変わってしまう。またラムダ計算では、引数部分を実行(簡約)してから関数呼び出し(関数適用の簡約)をおこなうか、引数を簡約せずに関数を呼び出すかは決まっていない。だから

x = :k{
  (λx.1)(k 2)
}

では、xに1が代入されるかもしれないし2が代入されるかもしれない。
普通のラムダ計算ではどの順番で簡約をおこなってもあとから合流させることができるのに、call/ccを導入すると実行順序によって結果が変わる場合が出てくる。
また、call/ccを使うと次のようなことがおこる。
上で作った排中律を表す項call/cc(λk.(Right λx.(k(Left x))))を使う。ただし、型はint∨¬intとする。これを使った次のプログラムを考える。

case (call/cc (λk.(Right λx.(k(Left x))))) of
  Left  y => y
| Right z => (int)(z 10)

まずcall/ccが値を返す。これはint∨¬int型のデータでRightのタグが付いている。よってcase式でRight zとマッチする。zはint→ $\bot$ 型でλx.(k(Left x))である(ただしkは継続)である。このzに10を渡す。
関数zの中では10にタグLeftを付けてint∨¬int型にしたあと、継続kに渡している。継続kが値を受け取ったのでジャンプしてcall/ccから出るところに移動する。なので移動先は、case式になる。
ここで、一度実行した部分を再び実行することになる。これはラムダ計算で考えると、いったん簡約を済ませた部分を再びやりなおすことにあたる。
このようにcall/ccを導入すると、それまでのラムダ計算と比べて変わったことが起こるようになる。ただし、call/ccは公理として導入されているので、call/ccについての簡約規則(ここでは与えていないけど、継続のことを考える必要があるので、普通のβ簡約のようにはいかない)と、証明図の書き換えとの対応関係がない。つまり直観主義論理のときのような対応関係がない。そもそもcall/ccの型がたまたま公理と一致しているだけのようにも見える。
そこでcall/ccのような公理ではなく、推論規則の追加によってラムダ計算を古典論理に対応させる方法を考える。
(古典論理のカリー・ハワード対応のためのラムダ計算につづく)
(追記: つづきは「継続の呼び出しは、古典論理の証明を直観主義論理の証明に書き換えることだったんだよ」みたいな内容になりそうな気がしてきた。本当にそれが正しいのかは、まだはっきりしていないけど)