継続 - herp-technote

継続

#ラムダ計算

力なり

残りの計算を指す｡

基本

継続は動的に現れ､あらゆる位置に存在する｡

次のコードを見てみる｡

code:ocaml

let x = e1 in

let y = e2 in

x + y

このコードの流れは(call-by-valueを想定)

1. まず e1 を計算し

2. それを x に束縛し

3. e2 を計算し

4. それを y に束縛し

5. (+) をx に(部分)適用し

6. 返ってきた関数を y に適用する｡

1. から見た残りの計算､つまり継続とは 2.~ 6. のことである｡ e1 の継続は次のように表され､

code:ocaml

let x = in

let y = e2 in

x + y

e1 の部分はholeと呼ばれる｡

e1 を値に評価し､それをholeに放り込むことで継続が実行され､計算が再開される｡

記法

多くの教科書的記法では､

code:ocaml

E = let x = in

let y = e2 in

x + y

のように E ( *E* valuation context) と記され､holeに値を放り込むときは

code:ocaml

のように書き表される｡

また､継続を関数として用いる場合は､

code:ocaml

k = fun x -> Ex

のように k (kappa もしくは *k* eizoku)もしくは単に cont などの変数名が使われる｡

継続演算子 - call/cc

最もメジャーな継続演算子といえば Schemeなどがプリミティブに持つ call/cc だろう｡

code:racket

(begin

(display "hello")

(let (x (call/cc (λ (k)

(k "world")

(display "!"))))

(display x)))

OCamlに親しんだ人間なら､

code:ocaml

(* ややウソ｡beginを翻訳してないがunitなんでまあ *)

let () = print_string "hello" in

let x = callcc @@ fun k ->

let () = k "world" in

print_string "!"

print_string x

と読める｡

まず､ call/cc は(概念的に)プログラムの実行を一時停止し､継続として切り出し､渡された関数のボディを評価する｡

code:ocaml

let E = let () = () in (* 評価済み *)

let x = in (* ここでcall/ccが呼ばれた *)

print_string x

let k = fun x -> Ex in

(fun k ->

let () = k "world" in

print_string "!"

) k

そして継続のholeに world が放り込まれることでプログラムの実行が再開される｡このとき､ call/cc 内の残りの部分(これも(異なる)継続)は破棄される｡

確かな事情は分かっておらずサーベイ不足で申し訳ないが､おそらくはプログラムの終了までの継続を全て取ってくるので継続を呼んだらプログラムが終了するようになってほしい､ということだろうか｡したがって継続が呼ばれる位置以降の (display "!") は実行されない｡

したがって､出力は helloworld となる｡

コラム call/ccの型

ところで､call/cc の型はどうなるだろうか?

まずholeの型を 'a と置くと､ call/cc に渡される関数は " 'a を受け取って何かを返す"型を受け取る｡ "何か" は 'b 型としよう｡つまり継続の型は 'a -> 'b となる｡

call/cc が返す型はholeの型なので､ 'a を返すはずである｡だがちょっと待てよ､ call/cc 内で継続を呼ぶとそれ以降が破棄されるから… call/cc に渡される関数は継続 'a -> 'b を受け取って､継続を実行して終了するから 'b を返せばよい｡つまり call/cc に渡される関数の型は ('a -> 'b) -> 'b)だ｡

なので call/cc の型は (('a -> 'b) -> 'b) -> 'a となる｡

限定継続

詳細は別紙にて