不動点意味論
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/30 16:28 UTC 版)
表示的意味は、システムが行うことを表現する数学的オブジェクトを探すことに関心がある。この理論は計算の数学的領域（ドメイン）を利用する。そのような領域の例として完備半順序集合などがある。 関係 x≤y は、x が y に計算的に発展する可能性があることを意味する。表示が完備半順序集合の要素ならば、例えば f≤g は f が定義されている全ての値について g と等しいことを意味する。 計算領域は次のような特徴を持つ: 下限の存在: 領域には必ず ⊥ で表される要素が含まれ、領域内の任意の要素 x について ⊥≤x が成り立つ。 上限の存在: 計算を続けると表示は洗練されるが、限界を持つべきである。そのため、 ∀ i ∈ ω {\displaystyle \forall i\in \omega } x i ≤ x i + 1 {\displaystyle x_{i}\leq x_{i+1}} としたとき、上限 ∨ i ∈ ω x i {\displaystyle \vee _{i\in \omega }x_{i}} が存在する。これを ω {\displaystyle \omega } -完全と呼ぶ。 有限要素は可算: 有向集合 A について ∨A が存在し x ≤ ∨ A {\displaystyle x\leq \vee A} であるとき、 x ≤ a {\displaystyle x\leq a} であるような a ∈ A {\displaystyle a\in A} が存在する。そのとき、要素 x は有限であるという（領域理論的に言えば、isolated）。換言すれば、x に到達あるいは x を超えるのに有限のプロセスで可能であるなら、x は有限である。 全ての要素は有限要素の順序列の上限である: 任意の要素に有限の計算手順で到達することを意味している。 領域は downward closed である システム S に関する数学的表示は、初期の空の表示 ⊥S から始めて、表示近似関数 progressionS を使って S の表示（意味）を構築していくことでよりよい近似を作っていくことで構築される。これは以下のように表される: DenoteS ≡ ∨i∈ω progressionSi(⊥S). ここで、progressionS は「単調」であるべきで、x≤y であるとき progressionS(x)≤progressionS(y) である。さらに一般化すると次のように表される。 もし ∀i∈ω xi≤xi+1 ならば progressionS(∨i∈ω xi) = ∨i∈ω progressionS(xi) このような progressionS の特徴を ω-連続と呼ぶ。 表示的意味論では、DenoteS の方程式に従って表示（意味）を作成可能かどうかを主題とする。計算領域理論の基本的定理は、progressionS が ω-連続ならば、DenoteS が存在するというものである。 そこで、progressionS が ω-連続であることから以下が成り立つ: progressionS(DenoteS) = DenoteS これはつまり、DenoteS が progressionS の「不動点; fixed point」であることを意味する。 さらに、この不動点は progressionS の不動点の中で極小である。 関数型言語の表示的意味論の実例を次節に示す。
※この「不動点意味論」の解説は、「表示的意味論」の解説の一部です。
「不動点意味論」を含む「表示的意味論」の記事については、「表示的意味論」の概要を参照ください。
- 不動点意味論のページへのリンク
