"Lectures on Semantics: The initial algebra and final coalgebra perspectives"

読む

1.2 Examples of Syntax and Semantics p.4 のメモ

メモ

syntaxの定義として、expressionのset E
それに対して、structure \cal{A}=(A,...)
と、meaning function []:E -> A
を用意してsemanticsとする。

structureの最初の要素Aは、structure のunderlying set.
数学的なstructureは、形式言語の「実装」となる。
ふたつめ、みっつめの例では、fixed set Kが与えられている。
よっつめの例では、function symbols の set Σにより構成されるsignatureが与えられる。
σ∈Σのそれぞれは、そのarityとして、自然数n_\sigmaを持つ。

arityは、関数の引数の数ということでいいのかな。
functionのsetではなくて、function symbolsのset？
function symbolsっていうのはどういうことだろう。
functionのsymbolだけあって、実装はべつってことだろうか。。。

Peano Structures p.5

structure \cal{A} = (A,a,f)
a∈A
f:A→A
e::=□｜e^+.（e∈E）
定義はここまで。
Eは再帰的な定義により実際には、
E={\boxe , \boxe^{ + } , \boxe^{ + + } , . . . }
のようになる。
でこのPeano structure \cal{A} = (A, a, f)
に対するmeaning function \llbracket \rrbracket : E \rightarrow Aは、

\{ \llbracket \boxe \rrbracket = a \\ \llbracket e ^ + \rrbracket = f (\llbracket e \rrbracket)
となる。具体的に適用してみると、
E= \{ \boxe , \boxe^{ + } , \boxe^{ + + } , \boxe^{ + + +} , . . . \}
A= \{ a, f(a), f(f(a)), f(f(f(a))), ...\}
こんなかんじ。
とくに fについて、単射であるとかないとか、そういうことは書いてない。
数学的な、集合や関数からのみ定義されたstructureを用意して、
expressionsからstructrueにマップするmeaning functionを決めることで、
semanticsを決定したことにすると、そんなかんじなのかな。

List Structures p.5

こんどは、まずset Kが与えられる。で、 K上のList Structureとして、
\cal{A} = (A, a, f)
f :K \times A \rightarrow A
a \in A
を定義する。
syntaxは、 e ::= [ ] | k : e (k \in K)
まるでHaskellのリスト。 Kを仮に自然数の集合とすると、
たとえば、 2 : 1 : 3 : [ ] こんな感じの式が作れる。
meaning functionは、
\{ \llbracket [ ] \rrbracket = a \\ \llbracket k : e \rrbracket = f ( k , \llbracket e \rrbracket) (k \in K , e \in E)
となる。 \llbracket 2 : 1 : 3 : [ ] \rrbracket = f( 2, f( 1, f(3, a) ) )
まるでLispのconsみたいだが、Lisp Structuresは、次。
Kと \cal{A}の関係がはっきりわからないのがすこし気持ち悪い。

Lisp Structures p.5

最初、List Structuresのところででてきたやつは、リストで、Lisp構造といえばやっぱりリストだろ？Lisp Structuresって、いったいなんだ？と思ったが、どうやらリストの要素にリストがきたり、整数がきたりする、Lispの動的型付けなリストのことのようだ。上ででたList Structureは、Haskellのリストのように、k \in Kのみがリストの要素になれる。k \in Kのリストを要素に含むリストは構成できない。

まず、List Structuresの時と同じように、set Kが与えられる。で、 K上のLisp Structureの定義は、
\cal{A} = (A, a, f)
f :A \times A \rightarrow A
a :K \rightarrow A
になる。List Structures に比べると、 aが、KからAへの関数になっている点と
fのソースが、 K \times Aでなくて、 A \times Aになっているところが違う。
nilは特に明示されていないな。
syntaxは、 e ::= k | e \cdot e (k \in K)
なので、さっきのようにKを整数の集合にしておくと、
[tex: *1]とか。
とにかく、空リストに相当するものが与えられていないので、Kを整数ってことにしてしまうと、
純リストは構成できなくい。が、まぁいいのか。

今思ったけど、syntaxには、結合の優先順序みたいなものは考慮されていない。というか、本当にテキストファイルにかかれたプログラムというより、パースして木にした後だけのことを考えてるってことか。実際にsyntaxにそってちゃんと書こうとすると、明示的に()をたくさん使うしかないな。
で、meaning functionは、
\{ \llbracket k \rrbracket = a(k) \\ \llbracket e_1 \cdot e_2 \rrbracket = f ( \llbracket e_1 \rrbracket , \llbracket e_2 \rrbracket) (k \in K , e \in E)
になる。
ということで例としては、
[tex: \llbracket*2, a(3))]
\llbracket ( (1 \cdot 2) \cdot (1 \cdot 2)) \rrbracket = f(f(a(1), a(2)),f(a(1), a(2)))こんなかんじか。

*1:1 \cdot 2) \cdot 3)]とか [tex: ( (1 \cdot 2) \cdot (1 \cdot 2

*2:1 \cdot 2) \cdot 3) \rrbracket = f(f(a(1), a(2