表示的意味論

denotational semanctics

意味関数を定義して、プログラムの「意味」を定義する

対象とする言語の語句それぞれを、「表示」に変換する

変換方法(つまりプログラムの実行方法)については問わない

プログラムの挙動や、評価戦略などについては定義されない

意味領域の集まりの性質を用いて、プログラムの振る舞いに関して推論するための強力な法則を導くことができる

例えば以下のような法則

2つのプログラムが厳密に同じ振る舞いをすることを証明するための法則

プログラムの振る舞いが何らかの仕様を満たすことを証明するための法則

「表示」とは

表示的意味論は、プログラムを、プログラムの意味を表す数学的対象へ写す

表示的意味論: プログラム -> 数学的対象

この「数学的対象」が「表示(denotation)」である

プログラムの10や1+9やsum [1..4]は、整数10を表示(denote)する

表記

プログラムのはOxford Bracketsで囲う

e.g.

$ \llbracket 1+9 \rrbracket = 10

$ \llbracket \mathrm{Integer} \rrbracket = \mathbb{Z}

$ \llbracket a+b \rrbracket = \llbracket a \rrbracket + \llbracket b \rrbracket

BNF記法とかは、表示的意味論になるのか？

評価戦略は何も言わないけど、記号の優先順位云々はある

手続き型言語でのための表示的意味論は難しい？

書籍

ここのamazonレビューに難易度を書いてくださっている人がいる

易しいもの順に並べると

という感じらしい

参考

Haskellでの表示的意味論の解説

詳しい