goto文を持つ言語の意味論
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/06/01 02:22 UTC 版)
「継続」の記事における「goto文を持つ言語の意味論」の解説
継続の概念はgoto文を持つ言語に意味論を与える。goto文を持たない場合、意味論は例えば命令文 γ、変数に対する値の割り当て ρ、抽象機械の状態遷移 θ ∊ [S → S] (S は機械の状態空間を表す) を用いて C [ γ ] ( ρ ) = θ {\displaystyle {\mathcal {C}}[\gamma ](\rho )=\theta } のように与えられる。この意味論において、2つの命令の逐次実行は2つの状態遷移の合成として表すことができるが、goto文が存在する言語の場合、goto文の直後の命令は、goto文を実行した直後に実行されるわけではないため、少なくともそのように意味論を与えることはできない。 goto文を持つような言語において、意味論を与える写像 P {\textstyle {\mathcal {P}}} は例えば、命令文の集合 Cmd、環境の集合 Env、継続の集合 C、機械の状態の集合 S を用いて次のような型を持つ： P : [ C m d → [ E n v → [ C → [ S → S ] ] ] ] {\displaystyle {\mathcal {P}}:[{\mathit {Cmd}}\to [{\mathit {Env}}\to [C\to [S\to S]]]]} ここで継続は C = [S → S] すなわち状態の遷移として、また環境 Env は D ⊃ C {\textstyle D\supset C} を満たすようなラベルの集合 D と識別子の集合 Id を用いて Env = [Id → D] と表される。命令文 γ と環境 ρ に対して、 P [ γ ] ρ {\displaystyle {\mathcal {P}}[\gamma ]\rho } は継続を受け取って継続を返す関数の形となる。 この設定の下でgoto文はラベルの識別子 ξ ∈ I d {\textstyle \xi \in {\mathit {Id}}} に対して P [ g o t o ξ ] ρ θ σ = ( ρ [ ξ ] | C ) σ {\displaystyle {\mathcal {P}}[\mathop {\mathbf {goto} } \xi ]\rho \theta \sigma =(\rho [\xi ]|_{C})\sigma } のように実装される。ここで ρ [ ξ ] | C {\textstyle \rho [\xi ]|_{C}} とは ρ [ ξ ] ∈ D {\textstyle \rho [\xi ]\in D} の C への射影であり、動的な型検査としての働きを持つものである。
※この「goto文を持つ言語の意味論」の解説は、「継続」の解説の一部です。
「goto文を持つ言語の意味論」を含む「継続」の記事については、「継続」の概要を参照ください。
- goto文を持つ言語の意味論のページへのリンク
