表示的意味論がわからないので簡単な例を翻訳してみた。 #Prolog

表示的意味論って何？

日本語で例を探すも見つからなかった。
英語だと Denotational Semantics というらしい。
Denotational Semantics example でググってみた。
見つかった。

眺めてみよう。

Denotational Semantics

Establish the meaning of a program by specifying a meaning for each phrase of the Abstract Syntax Tree (AST).

declarations
commands
expressions

The mean of a phrase is defined by the meaning of each subphrase.

The meaning is its denotation.
Established by providing semantic functions that map phrases to their denotations.

Example: Binary Numbers

Numerals are syntactic entity; numbers are semantic.

Numeral -> 0
        -> 1
        -> Numeral 0
        -> Numeral 1

Each (binary) numeral denotes a single member of the domain:

Natural = { 0, 1, 2, ... }

to formalize this, we define the semantic function:

valuation: Numeral -> Natural

with the definition:

valuation [[0]] = 0
valuation [[1]] = 1
valuation [[N 0]] = 2*valuation N
valuation [[N 1]] = 2*valuation N + 1

The valuation function’s 4 equations correspond to the phrases of the (abstract) syntax for our binary language.
Look at evaluation sequence for “110”:

valuation[[110]]
= 2*valuation[[11]]
= 2*(2*valuation[[1]]+1)
= 2*(2*1+1)
= 6

翻訳すると良さそう。

翻訳してみた。

表示的意味論

抽象構文木（AST）の各フレーズの意味を指定して、プログラムの意味を確立します。

宣言 (declarations)
コマンド (commands)
式 (expressions)

フレーズの意味は、各サブフレーズの意味によって定義されます。

Established by providing semantic functions that map phrases to their denotations.
意味はその表示 (denotation) です。
フレーズをその表示にマップする意味論的関数 (semantic functions) を提供することによって確立されます。

例: 2進数

数字(Numerals)は構文上の実体 (syntactic entity) です; 数字は意味論的です。

数字 -> 0
    -> 1
    -> 数字 0
    -> 数字 1

各（2進）数は、ドメインの単一のメンバーを示します:

自然数 = {0, 1, 2, ...}

これを形式化するために、セマンティック関数を定義します:

評価: 数値 -> 自然数

定義は:

評価[[0]] = 0
評価[[1]] = 1
評価[[N0]] = 2 * 評価 N
評価[[N1]] = 2 * 評価 N + 1

評価関数の4つの方程式は、2進数言語の(抽象)構文のフレーズに対応しています。
"110" の評価シーケンスを見てください。

評価[[110]]
= 2 * 評価[[11]]
= 2 *（2 * 評価[[1]] + 1）
= 2 *（2 * 1 + 1）
= 6

なるほどなるほど

なんとなくわかった気がする。
Haskell で書いてみよう。

構文

numeral [0]   = True
numeral [1]   = True
numeral (0:n) = numeral n
numeral (1:n) = numeral n
numeral _     = False
main = do
  print $ numeral [0,0,0]
  print $ numeral [1,3,0]

変換関数

valuation n = rvaluation (reverse n)
rvaluation [0] = 0
rvaluation [1] = 1
rvaluation (0:n) = (2 * rvaluation n)
rvaluation (1:n) = (2 * rvaluation n) + 1
main = do
  print $ valuation [1,1,1]
  print $ valuation [1,0,0,0,0]

なんかちがう

Haskell っぽいけど微妙に違う。
リストだと逆順だ。
Prolog で書いてみる。

構文

numeral(0).
numeral(1).
numeral((N-0)) :- numeral(N).
numeral((N-1)) :- numeral(N).
:- numeral((0)).
:- numeral((1-1-0)).
:- \+numeral((1-3-0)).
:- numeral((1-1-1)).
:- halt.

を区切り文字として使って定義通りの順番にした。
なんか違う？

変換関数

valuation(0,0).
valuation(1,1).
valuation((N-0), R):- valuation(N, N1), R is 2 * N1.
valuation((N-1), R):- valuation(N, N1), R is 2 * N1 + 1.
:- valuation((1-1-1),7).
:- valuation((1-0-0-0-0),16).
:- halt.

これじゃ関数じゃなくて述語だ

操作的意味論じゃね？

Prolog は一階述語論理であり操作の定義をした感じになるので、操作的意味論に近くなってしまった。
表示的意味論の操作的意味を考えてみれば良いのかな？

表示的意味の構文の操作的意味

m(V,V).
m(S,V):- syntax(S->_),s(S,V).
m(S1-S2,V1-V2):- m(S1,V1),m(S2,V2).
ss(S->_,V):-m(S,V).
ss(_->SS,V):- !,ss(SS,V).
ss(S,V):-m(S,V).
s(S,V):- syntax(S->SS),ss(SS,V),!.

m/2 が構文のマッチングを行い、 ss/2 が構文規則を全て検査し、s/2 が構文名に当てはまるか検査する規則になる。m/2 は - な式だけ特別扱いしていることに注意。

表示的意味の構文

syntax(
  numeral -> 0
          -> 1
          -> numeral-0
          -> numeral-1
).
:- s(numeral,0),s(numeral,1),s(numeral,1-0),\+s(numeral,0-2).
:- s(numeral,1-0-1-0),halt.

うまくいくようです。

表示的意味論の関数の操作的意味

e(I1+I2,R):- integer(I1),integer(I2),!,R is I1+I2.
e(I+E,I+R):- integer(I),!,e(E,R).
e(E1+E2,R+E2):- e(E1,R).
e(I1*I2,R):- integer(I1),integer(I2),!,R is I1*I2.
e(I*E,I*R):- integer(I),!,e(E,R).
e(E1*E2,R*E2):- e(E1,R).
e(E,R):- fn(E=R),!.
en(E,R):- e(E,E2),!,en(E2,R).
en(E,E).

e/2 が１回分の代入をする評価規則で、en/2 が変換終わるまで変換する評価規則です。小ステップな操作的意味になリマス。

表示的意味論の変換関数

ty(valuation = numeral -> integer).
fn(valuation(0) = 0).
fn(valuation(1) = 1).
fn(valuation((N-0)) = 2*valuation(N)).
fn(valuation((N-1)) = 2*valuation(N)+1).
:- en(valuation(1-0-0-1),9),en(valuation(1-1-1-1),15).
:- en(valuation(1-0-0-0-0),16).
:- halt.

パターンマッチングのある関数型言語が定義できてしまった。
ちゃんと動くぞー。

まとめ

表示的意味論の簡単な例を見つけた
翻訳してみた
HaskellとPrologで実装してみたがなんか違う
Prolog で表示的意味論の操作的意味を考えてみた
完全に理解した！

付録

算術式の構文

:- op(700,xf,[=]).
m(V,V).
m(integer,V):- integer(V).
m(S,V):- syntax(S->_),s(S,V).
m(S,V):- S =.. [O|SS] , V =.. [O|VS], maplist(m,SS,VS).
ss(S->_,V):-m(S,V).
ss(_->SS,V):- !,ss(SS,V).
ss(S,V):-m(S,V).
s(S,V):- syntax(S->SS),ss(SS,V),!.
syntax(command -> expression =).
syntax(
  expression -> integer
             -> expression+expression
             -> expression-expression
             -> expression*expression).

意味論の操作的意味

e(I1+I2,R):- integer(I1),integer(I2),!,R is I1+I2.
e(I+E,I+R):- integer(I),!,e(E,R).
e(E1+E2,R+E2):- e(E1,R).
e(I1-I2,R):- integer(I1),integer(I2),!,R is I1-I2.
e(I-E,I-R):- integer(I),!,e(E,R).
e(E1-E2,R-E2):- e(E1,R).
e(I1*I2,R):- integer(I1),integer(I2),!,R is I1*I2.
e(I*E,I*R):- integer(I),!,e(E,R).
e(E1*E2,R*E2):- e(E1,R).
e(E,R):- fn(E=R),!.
en(E,R):- e(E,E2),!,en(E2,R).
en(E,E).

算術式の関数

fn(sum(E1,E2) = E1+E2).
fn(difference(E1,E2) = E1-E2).
fn(product(E1,E2) = E1*E2).
fn(exec(E=) = eval(E)).
fn(eval(E1+E2) = sum(eval(E1),eval(E2))).
fn(eval(E1-E2) = difference(eval(E1),eval(E2))).
fn(eval(E1*E2) = product(eval(E1),eval(E2))).
fn(eval(N) = N).
:- s(command,(40-3)*9=).
:- en(exec((40-3)*9=),R),!,R=333.
:- halt.