\(\def\rewrite{\color{blue}{\iff}}\)
Scheme には call/cc (call-with-current-continuaion; 現在継続) というプリミティブな手続きがある. Lisp は計算モデルを最小で構成する理論から生まれ Scheme はその流れを汲んだ由緒正しいプログラミング言語だが, call/cc に関しては理論ありきではなく, その真逆で, 実装できたから実装したという言語機能だという.
call/cc は関数に対しての return だと言える. return という文はすごくて, 大域脱出をしつつ値を返すというすごい機能をサポートしている.
何ともつかない擬似言語で書くと return というのは次のようなものだろう.
function f() {
do1();
return 42;
do2();
}これは関数 f を定義している. f を呼び出すとこれはおそらく do1 という手続きを実行し, そして 42 を返して即座に終了する. すなわち, 後続する do2 という手続きは実行 されない. すなわち return はその一行でだけの効果ではなくて, それに続く後ろをスキップするという信じられない効果を持っている. これを 大域脱出 という. for 文に対する break も同じような効果を持っている. return は関数の中ならどこでも呼ぶことが出来て, for 文の中からでも脱出することが出来る.
function f() {
do1();
for (var i = 0; i < 10; ++i) {
return i;
}
do2();
}この return はたぶん i=0 の時点で return 0 を実行するから, i=1 以降は実行すらされない. すごい.
また break との違いとして, 値を返す効果も持っている. return x とすると, f の値が x になる.
call/cc はこの return という手続き自体を値としてプリミティブに扱うことのできる機能である. Scheme には return というキーワード自体が無いわけだが, 次のようなことができる.
(define (f)
(call/cc (lambda (return)
(print 'do1)
(return 42)
(print 'do2)
)))この手続き f を呼び出すと do1 を表示したら 42 を f の値として返して即座に終了する. ここでこの return というのはいわゆる return 的な操作をする手続きが入った変数であり, 親しみのために return という名前をつけているだけで何でもいい.
ここで return はユーザーが定義した手続きと同様に使えるので, その値をそのまま他の式に渡せる. 例えば次は 2 * (return 42) みたいなことをしている.
(define (f)
(call/cc (lambda (return)
(print 'do1)
(*
2
(return 42))
(print 'do2)
)))この f を呼ぶと何が返ってくるのかというと 2 * 42 ではなく, 42 そのものが返ってくる. return は式の中の部分であっても間違いなく大域脱出をしてくれる.
実際には Scheme は動的型付けなので何でもいいんだけど, （静的に）型を与えることを考える.
仮に x の型を T とする. return は T を受け取る. 返り値は無いし return の値自体が使われるこはない. これは先程 (* 2 (return 42)) と書いたときに (* 2 ...) 部分が実行されなかったことから分かる通り.
仮に何も無いことを表す型を Nothing と書く. 型理論だと \(\bot\) と書いたほうが馴染みがあるかもしれない. 一応 Scala だと Nothing という型がある.
Nothing は多くの言語にある Null とは全く別物なので注意. 本当に値を返さなくて参照しようとすら出来ない.
return : T -> Nothing次に call/cc の第一引数 (lambda (return) ...) の型だが ... が分からないので仮にここを ? にすると
(lambda (return) ...) : (T -> Nothing) -> ?となる. 最後にこれらを組み合わせて call/cc の型が付く. call/cc の最後の値は (return x) していれば x なので,
call/cc : ((T -> Nothing) -> ?) -> Tさて ? だが, これは ... の中で return を使わない場合を考えると自然に決まる.
(call/cc (lambda (return)
42))このような場合は call/cc 全体の値は 42 になるのが自然でそのためには (lambda (return) 42) の値が 42 である必要がある. 従って, ? には x の型が入るべきで
call/cc : ((T -> Nothing) -> T) -> Tとなる.
ご存知のように（純粋関数言語の）プログラムの型は論理式に対応する. 特に Nothing という型は矛盾を表す命題 \(\bot\) に対応して
論理式 call/cc: \[((T \implies \bot) \implies T) \implies T\] を得る.
また NOT 演算 \(\lnot T \iff (T \implies \bot)\) を使うと call/cc は \[(\lnot T \implies T) \implies T\] とすっきり書ける.
白状すればこの議論は直観論理もしくは古典論理で行っている. このどちらでも次の2つは成立する.
命題の中における \(\iff\) と区別してよりメタな意味での書き換えを表すのに \(\rewrite\) を使ってみる. 単に読みやすさのために.
これらを使うと,
\[\begin{align*} \mathrm{call/cc} & ~~ \colon ~ (\lnot T \implies T) \implies T \\ & \rewrite \lnot (\lnot T \implies T) \lor T \\ & \rewrite \lnot (\lnot \lnot T \lor T) \lor T \\ & \rewrite (\lnot \lnot \lnot T \land \lnot T) \lor T \\ \end{align*}\]
古典論理なら二重否定除去 \(\lnot \lnot T \rewrite T\) を使って即座に \(\mathrm{call/cc} \rewrite \lnot T \lor T\) を得る. 直観論理では二重否定除去は使えないが, \(\lnot \lnot \lnot T \land \lnot T \iff \lnot T\) が, というかもっと一般に, \(\lnot \lnot X \land X \iff X\) が言えるので, やはり \(\lnot T \lor T\) を得る.
以上から call/cc の型はカリーハワード対応によって排中律に対応していることが分かった.
直観論理の体系でこれを確認する.
\(\implies\) は自明で \(\land\) の右を取ればよい. \(\impliedby\) を確認する.
\(X \implies X\) と \(X \implies \lnot \lnot X\) が同時に成り立てば, これらを組み合わせて \(X \implies \lnot \lnot X \land X\) を得る. 1つ目は自明なので \(X \implies \lnot \lnot X\) を証明すればよい.
\(\lnot\) の糖衣構文を展開すると, \[\begin{align*} & X \implies \lnot \lnot X \\ \rewrite & X \implies \lnot X \implies \bot \\ \rewrite & X \implies (X \implies \bot) \implies \bot & \text{ 三段論法}\\ \rewrite & X \land (X \implies \bot) \implies \bot \\ \rewrite & \bot \implies \bot \\ \rewrite & \top \\ \end{align*}\] と確認できた.
以上より \(\lnot \lnot X \land X \iff X\) である.
涼宮ハルヒの直観楽しみ～2020