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

読む

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

Σ-structures p.5

まず、signatureとしてΣが与えられる。
このとき、Σ-structures
\cal{A} = ( A, \sigma^{\cal{A} })_{\sigma \in \Sigma}
が、set Aと、
\sigma \in \Sigmaそれぞれにつき与えられる
\sigma^{\cal{A} }:A^{n_ \sigma} \rightarrow A
により構成される。
{n_ \sigma}ってのは、 g: \Sigma \rightarrow \mathbb{N}のような関数が用意されていて、\sigmaにつき、それぞれarity {n_ \sigma}が割り当てられている、ということだろう。
\sigmaと \sigma^{\cal{A} }の関係が分かりづらいな。
p.4の最後のところに、 \Sigmaは、function symbolsのsetであると書いてあるので、
\sigma \in \Sigmaはfunctionそのものではないと。で、
\sigma ^{\cal{A} } は、Aとともに\cal{A}が与えられたときに、structureとsignatureを組合せてはじめて関数そのもの \sigma^{\cal{A} }:A^{n_ \sigma} \rightarrow Aがえられるってことかな。としても、やっぱり
\cal{A} = ( A, \sigma^{\cal{A} })_{\sigma \in \Sigma}
が分かりづらいな。Aと、 {\sigma \in \Sigma}のそれぞれにつき \sigma^{\cal{A}}が与えられているとすると、 {\sigma^{\cal{A}} \in \Sigma^{\cal{A}}}のような {\sigma^{\cal{A}}を要素とする集合が暗に考えられているのか。そうだったら、
\cal{A} = ( A, \{ \sigma^{\cal{A} } : {\sigma \in \Sigma}\})ってことなのか。
それとも、 \cal{A}自体がタプルの集合ということで、
\cal{A} = \{ ( A, \sigma^{\cal{A} }) : {\sigma \in \Sigma} \}
ということなのだろうか？わからない。。。
ま、とにかくsymbolである \sigmaとそれに対応するfunction \sigma ^{\cal{A}}
が存在することだけわかればいいか。
syntax は、
e::=\sigma \overbrace{e \cdots e}^{n_ \sigma}(\sigma \in \Sigma)

meaning functionは、
\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)

Exercise 1.1 p.6

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