日記 (2020 年 7 月 5 日)

プログラミング言語の Scheme には call/cc という関数が用意されていて、 これを用いると 「継続」 と呼ばれる情報を好きなタイミングで取り出して、 別の関数の引数として渡すなどプログラム中で自由に扱うことができる。 この機構は大域脱出やコルーチンを実装するのに利用できるなど、 応用の幅が広い。 さらに、 call/cc を含む体系は Curry–Howard 対応 (プログラムと証明の間の対応) のもとで古典論理に対応することが知られており、 これにより、 直観主義論理の範囲では証明できない二重否定除去則や Peirce の法則について、 その計算論的な意味付けがなされたことになる。

これから続く日記シリーズで、 継続と call/cc について理解しようとして私が勉強した内容をまとめていくつもりである。 なお、 議論の基盤としては、 Scheme などの実用プログラミング言語ではなく、 それを数学的に形式化したラムダ計算の体系を用いることにする。 私はこれらのトピックについて本格的に触れるのが初めてなので、 完璧な説明をすることは不可能だが、 継続と call/cc を理解したいという人にとっての助けになれば幸いである。

1 日目である今日は、 継続とは何かについて触れようと思う。 これを書くにあたっては Griffin†2 を大いに参考にした。

まず、 通常のラムダ計算の体系を思い出そう。 しばらくの間、 議論を簡単にするために型なしの体系を考えることにし、 さらに項の構築子としては関数のみを許すことにする。 以降、 これを単に λ と呼ぶことにする。

ラムダ計算の体系を定義するためにあとしなければならないことは、 項の簡約規則 (もしくは計算規則) を定めることである。 ここで問題となるのが評価順序であるが、 差し当たり値呼び (先に引数を値まで簡約してから関数適用を簡約する) を採用することにする。 簡約の厳密な定式化には、 評価環境の概念を用いる。

定義から見て分かるように、 評価環境 E の中には 1 箇所だけ [] という記号が含まれている。 この [] を何らかの項 M で置き換えて得られる項を E[M] で表す。

定義から、 ある評価環境の中に (λx.M)V という関数適用の形が現れていれば、 それは M[x:=V] という実際に引数を関数内部に代入した形に評価される。 したがって、 評価環境は関数適用の評価をする際の (評価自体とは無関係な) 外側を表していて、 その意味で 「環境」 なのである。 しかし、 この評価環境は別の見方もすることができる。

何らかの項 P,Q と値 V0 をとり、 F ≡ λx.P G ≡ λy.Q M0 ≡ G(FV0) とおく。 すなわち、 F,G はともに関数で、 M0 はその 2 つの関数を順番に V0 に適用した項である。 このとき M0 は、 M0 ≡ E0[FV0] E0 ≡ G[] と分解できるから、 簡約の定義により、 M0 の中にある FV0 すなわち (λx.P)V0 の部分が簡約され、 P[x:=V0] に置き換わる。 つまり、 M1 ≡ GV1 V1 ≡ P[x:=V0] とおけば、 M0 は M1 に簡約される。 ここで簡単のため、 V1 はすでに値になっているとする (そうでなければ値まで簡約した項を改めて V1 とすれば良い)。 このとき M1 は、 M1 ≡ E1[GV1] E1 ≡ [] と分解されるから、 M2≡Q[y:=V1] に簡約される。 以上をまとめると、 G(FV0)⇝GV1⇝M2 という簡約列が存在するということである。 言葉で言えば、 V0 から始めて、 最初に F を適用してその結果 V1 を計算し、 次にそれに G を適用してその結果を計算したということになる。

ここで、 最初の E0 の形を思い出そう。 これは G[] であった。 この形は、 [] という記号に対して G を適用した項と読むことができる。 M0 の簡約列を思い出すと、 この 「G を適用する (そしてその結果を計算する)」 という操作は、 最初の簡約である FV0 を V1 に置き換える操作の後に行われる操作であった。 すなわち E0 は、 M0 を 1 回簡約した後にさらに何を行うべきかを表現していると見なすことができる。

以上に見たように、 評価環境は、 そのとき行おうとしている簡約の後に行われるべき計算全体を表している。 これが 「継続」 の正体である。 すなわち、 今回の形式化では、 継続とは評価環境そのものである。

Scheme では、 call/cc という関数のおかげで、 この継続を好きなタイミングで取得し、 変数に束縛したり関数の引数として渡したりすることができる。 このように、 Scheme の継続は他の普通の値と同じようにプログラム内で利用することができるので、 「一級継続」 と呼ばれている。

通常のラムダ計算では、 継続 (つまり評価環境) は評価をするときにメタな視点から使われるにすぎず、 言語の中から操作することはできない。 したがって、 言語の中で継続を操作できるようにするためには、 何らかの方法で通常のラムダ計算を拡張する必要がある。 その拡張の 1 つに Parigot†3 の λμ-計算があり、 ここでは継続を変数に束縛する構文を追加することで一級継続を実現している。 しかし、 これにいきなり触れると定義を直観的に理解するのが少し難しいので、 まずはよりシンプルな Felleisen et al†1 の λc-計算を扱おうと思う。

λc-計算は、 通常のラムダ計算に abort と cont という 2 つの演算子を加えたものである。 形式的には以下の通りである。

追加された 2 つの演算子に関する簡約規則は以下のように定義される。 どちらの簡約規則も、 変化する部分は評価環境の内部に留まらず、 項全体が変化する。

以降、 ⇝ の反射推移閉包を ⇝∗ で表すことにする。 すなわち、 ⇝ が 1 ステップの簡約を表すのに対し、 ⇝∗ は 0 ステップ以上の任意回数の簡約を表す。

新しい演算子の直観的な説明は次の通りである。 abort の役割は、 その時点での評価環境を破棄することである。 定義によって、 E[abortM] という形の項は M に簡約される。 この簡約後の項には E は現れていない。 したがって、 計算の途中で abortM という形に遭遇した場合、 これの簡約によりその時点の評価環境が破棄されることになるわけである。

cont の役割は、 その時点での継続 (つまり評価環境) を関数の引数に渡して利用できるようにすることである。 定義を見ると、 E[contM] という形の項は M(λx.abortE[x]) に簡約される。 ここに出てくる λx.abortE[x] という部分項は、 引数を E で包んだものを返す関数であるから、 これを何らかの項に適用することで、 その項を contM に遭遇したときの評価環境のもとで評価することができるようになる。 つまり、 この λx.abortE[x] は、 contM を簡約した際の継続を関数の形で言語内で利用できるようにしたものなので、 以降では継続関数と呼ぶことにする。

これらの演算子の応用の 1 つに大域脱出がある。 大域脱出は、 多くの実用プログラミング言語に例外捕捉や関数の return 文などの形で実装されている他、 C 言語には setjmp と longjmp というそのままの関数が用意されている。

何らかの評価環境 E と項 P をとって、 M≡E[cont(λk.kP)] という項を考えよう。 ここで、 Q≡λx.abortE[x] とおけば、 M ⇝ (λk.kP)Q ⇝ QP[k:=Q]♡ と簡約される。 Q は値だから、 この後は P[k:=Q] の部分が簡約されていくことになる。

仮に P の中に k が自由に全く現れなかったとしよう。 このとき、 P[k:=Q] は P そのものである。 そこで、 P が最終的に値 V に簡約されたとする。 すると、 簡約列 ♡ の続きは、 ⋯ ⇝∗ QV ⇝ abortE[V] ⇝ E[V] となる。

P の中に k が自由に現れ、 P の簡約の仮定でそのような k がいずれ簡約される場合を考える。 P の中には k が複数個現れるかもしれないが、 一番最初に簡約される k に注目することにする。 これから簡約しようとしている項は P[k:=Q] であるが、 ここでは P の中にあった k は Q に置き換わっていることに注意しよう。 Q は継続関数であるから、 Q が何らかの項に適用される形で使われることが想定されている。 そこで、 Q は P[k:=Q] の中に QW という形で現れると仮定し、 簡単のため W は値であるとする。 以上の仮定を置くと、 P[k:=Q] を簡約していくと、 ある評価環境 E󰎘 によって E󰎘[QW] と表される項にいずれは簡約されるはずである。 したがって、 簡約列 ♡ の続きは、 ⋯ ⇝∗ QE󰎘[QW] ⇝ QE󰎘[abortE[W]] ⇝ E[W] となる。

以上をまとめれば、 E[cont(λk.kP)]⇝∗{ E[V] (k は P に自由に現れない,P⇝∗V) E[W] (k は P に自由に現れる,P⇝∗E󰎘[kW]) となる。 これを見ると、 次のことが観察できる。 まず、 この簡約によって、 cont(λk.kP) の外側である評価環境 E は変化せず、 cont(λk.kP) のみが値に置き換わる。 置き換わった結果得られる値は、 P の中に k が自由に現れるかどうかで変化する。 k が自由に現れないのなら、 通常通り P が簡約されて得られる値 V になる。 一方、 k が自由に現れる場合は、 P がどのような形なのかに関わらず、 P の中で (最初に簡約される) k に渡された引数 W になってしまう。

この現象は、 cont(λk.kP) が例外の catch 文に相当し、 P の中に現れる k がそれに対応する throw 文だと考えると、 イメージが湧きやすいだろう。 throw 文が一切現れなければ通常通り評価が進むが、 throw 文に引数が渡されてそれが評価されると、 他に処理がどんなに残っていようとそこに渡された引数が全体の返り値になる。

さて、 最初に Scheme の call/cc について少し触れたが、 この演算子は、 E[call/ccM]⇝E[M(λx.abortE[x])] という振る舞いをするものとして定式化できる。 cont との違いは、 簡約するときにその時点での評価環境を破棄しない点である。 この演算子を用いると、 上の説明で出てきた項 M は、 M=E[call/cc(λk.P)] とよりシンプルに書くことができる。

なお、 X≡λm.cont(λk.k(mk)) とおくと、 任意の項 M について XM と call/ccM は同値になる。 したがって、 λc-計算において call/cc の演算を行いたいときに、 プリミティブな演算子を新しく言語に追加する必要はなく、 上記の X を使えば良い。 逆に、 プリミティブな演算子として call/cc が入っている体系において、 Y≡λm.call/cc(λk.abortmk) とおくと、 任意の項 M について YM と contM は同値になる。

追記 (2020 年 7 月 6 日)

大域脱出の説明をしている箇所の記述が少しミスリーディングな気がしたので、 内容はそのままに記述を少し書き換えた。 また、 最後の call/cc に関する箇所により詳しい内容を追加した。

参考文献

1. M. Felleisen et al (1987) 「A syntactic theory of sequential control」 『Theoretical Computer Science』 52(3):205–237
2. T. G. Griffin (1989) 「A formulae-as-types notion of control」 『Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on principles of programming languages』 47–58
3. M. Parigot (1992) 「λμ-calculus: an algorithmic interpretation of classical natural deduction」 『Lecture Notes in Artificial Intelligence』 624:190–201