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

## 表示的意味論って何？

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

https://www.eecs.umich.edu/courses/eecs498.old/498/lecture3.pdf

- 眺めてみよう。

----

## 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.
```