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

読む

Exercise 1.1 p.6

Σ-structuresの具体例を、先のstructuresの４つのうちのΣ-structuresをのぞく最初の3つに対応づける問題。

1. \Sigma = \{ \boxe ,+ \} , with n_{\boxe}=0, n_+ = 1.

一番目の例、Peano Structuresに相当する。

syntaxは、先のΣ-structuresの定義では、
e::=\sigma \overbrace{e \cdots e}^{n_ \sigma}(\sigma \in \Sigma)
\Sigma = \{ \boxe ,+ \} しかないので、
e::=\boxe | + e。
具体的には、 E = \{ \boxe , + \boxe, + + \boxe ... \}

meaning functionは、Σ-structuresの一般的な定義では、
\llbracket \sigma e_1 \cdots e _ {n_ \sigma} \rrbracket = \sigma ^{\cal {A}}(\llbracket \e_1 \rrbracket , . . . , \llbracket \e_{n_\sigma} \rrbracket) ( \sigma \in \Sigma , e_1,...,e_{n_\sigma} \in E)
なので、
\{ \llbracket + e \rrbracket = + ^{\cal {A}}( \llbracket e \rrbracket) \\ \llbracket \boxe \rrbracket = \boxe ^{\cal {A}}()
ということで、具体的には、
\llbracket + + \boxe \rrbracket = + ^{\cal {A}}( + ^{\cal {A}}( \boxe ^{\cal {A}} ) )
ということか。

例ででてきたPeano Structuresの定義と比較。

structure \cal{A} = (A,a,f)
a∈A
f:A→A
e::=□｜e^+.（e∈E）
（具体的には、E={\boxe , \boxe^{ + } , \boxe^{ + + } , . . . }）
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))), ...\}
）

syntaxは、ちょっと順序が逆になっているが、それをのぞけばきれいに対応している。