表示的意味論って何？
- 日本語で例を探すも見つからなかった。
- 英語だと 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.