継続 概要

ウィキペディア

継続

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/01/11 06:13 UTC 版)

概要

計算一般における継続

Schemeによる次の式を考える：

(+ 4 (+ 1 2))

この式を評価する際、まず (+ 1 2) が計算され、すなわち 1+2 が計算され、次にその結果に4を足して全体の計算結果が求められる。(+ 1 2) の評価が行われた段階での「残りの計算」を表現すると、

(lambda (v) (+ 4 v))

のようになる。この式はすなわち、値 v を引数に取り、それに4を足した値を返す関数である。実際、この後 (+ 1 2) の計算結果が v に代入されて、4を足した値が最終的に計算結果が求められるため、この関数は確かに (+ 1 2) を評価する段階での「残りの計算」の表現である。

call/cc

Schemeの call-with-current-continuation (call/cc と省略される) は、その時点での継続を引数として関数を呼び出す手続きである。Schemeの言語仕様書（R7RS）には「もっとも単純な例」として次のコードが載っている：

(define list-length
  (lambda (obj)
    (call-with-current-continuation
      (lambda (return)
        (letrec ((r
              (lambda (obj)
                (cond ((null? obj) 0)
                  ((pair? obj)
                    (+ (r (cdr obj)) 1))
                  (else (return #f))))))
          (r obj))))))

このコードは、真正な（終端が空リストである）リストが渡された際にはそのリストの要素数を数えて返し、そうでない場合はfalse値を返す。

goto文を持つ言語の意味論

継続の概念はgoto文を持つ言語に意味論を与える。goto文を持たない場合、意味論は例えば命令文 γ、変数に対する値の割り当て ρ、抽象機械の状態遷移 θ ∊ [S → S] (S は機械の状態空間を表す) を用いて

$${\mathcal {C}}[\gamma ](\rho )=\theta$$

のように与えられる。この意味論において、2つの命令の逐次実行は2つの状態遷移の合成として表すことができるが、goto文が存在する言語の場合、goto文の直後の命令は、goto文を実行した直後に実行されるわけではないため、少なくともそのように意味論を与えることはできない。

goto文を持つような言語において、意味論を与える写像 ${\textstyle {\mathcal {P}}}$ は例えば、命令文の集合 Cmd、環境の集合 Env、継続の集合 C、機械の状態の集合 S を用いて次のような型を持つ：

$${\mathcal {P}}:[{\mathit {Cmd}}\to [{\mathit {Env}}\to [C\to [S\to S]]]]$$

ここで継続は C = [S → S] すなわち状態の遷移として、また環境 Env は ${\textstyle D\supset C}$ を満たすようなラベルの集合 D と識別子の集合 Id を用いて Env = [Id → D] と表される。命令文 γ と環境 ρ に対して、${\mathcal {P}}[\gamma ]\rho$ は継続を受け取って継続を返す関数の形となる。

この設定の下でgoto文はラベルの識別子 ${\textstyle \xi \in {\mathit {Id}}}$ に対して

$${\mathcal {P}}[\mathop {\mathbf {goto} } \xi ]\rho \theta \sigma =(\rho [\xi ]|_{C})\sigma$$

のように実装される。ここで ${\textstyle \rho [\xi ]|_{C}}$ とは ${\textstyle \rho [\xi ]\in D}$ の C への射影であり、動的な型検査としての働きを持つものである。