表示的意味論
関数 factorial が以下のように定義されているとする:
factorial ≡ λ(n)if (n==0)then 1 else n*factorial(n-1)
factorial の graph とは、引数と値のペアの順序集合であり、以下のようになる:
graph(factorial) = {<n, factorial(n)>|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>...}
factorial プログラムの表示(意味) Denotefactorial は、以下のように構築される:
Denotefactorial = graph(factorial) = ∪i∈ω progressionfactorial({})
ここで
progressionfactorial(g) ≡ λ(n)if (n==0)then 1 else n*g(n-1)
ただし、progressionfactorial は不動点演算子であり、極小不動点 Denotefactorial は次のようになる:
Denotefactorial = progressionfactorial(Denotefactorial)
また、progressionfactorial は、ω-連続である。
意味モデルは、直観的に構成可能な要素のみから構築可能であるべきである。形式的に表現すれば、全要素は有限要素の有向集合の上限でなければならない。