文脈付き構成的意味論を構成的意味論に変換する

mandel59.hateblo.jp

ここでは, 自然数の集合 ${\bf N}$ に0を含めることとする。

記法 $\left ( a_k \right )_{k=m}^{n}$ は $\left (a_m, a_{m+1}, \cdots, a_{n-2}, a_{n-1} \right )$ を表す。 $m = n$ の時は $\left ( \right )$ を表す。
記法 $\bigwedge_{k = m}^{n} p_k$ は $p_m \wedge p_{m+1} \wedge \cdots \wedge p_{n-2} \wedge p_{n-1}$ を表す。 $m = n$ の時は $\top$ （真理値の真）を表す。

形式言語

形式言語 $L = \langle F, | \bullet | \rangle$ は関手集合 $F$ , 関手の項数 $| \bullet | : F \rightarrow {\bf N}$ からなる組である。

式

形式言語 $L = \langle F, | \bullet | \rangle$ の式集合 $E(L)$ を, つぎの帰納的定義によって定める:

$f \in F \land \left ( \bigwedge_{k = 0}^{|f|} t_k \in E(L) \right ) \Rightarrow f(t_k)_{k=0}^{|f|} \in E(L)$ .

これは, 次のようなことを含意している:

が項数の関手であり, が式であるとき, は式である。
- 特に, $f$ が項数 $0$ の関手であるとき, $f()$ は式である。
$t$ が式であるとき, ある自然数 $n$ , ある項数 $n$ の関手 $f$ , ある式 $t_0, \cdots, t_{n-1}$ が存在し, $t = f(t_0, \cdots, t_{n-1})$ .

構成的意味論

構成的意味論 $\Sigma = \langle L, M, I \rangle$ は形式言語 $L = \langle F, | \bullet | \rangle$ , 意味集合 $M$ , 解釈 $I : f \in F \mapsto g \in [ M^{|f|} \rightarrow M ]$ からなる組である。

このとき $\Sigma$ のもとの式の意味 $\Sigma \unicode{x27e6} \bullet \unicode{x27e7} : E(L) \rightarrow M$ を, つぎの帰納的定義によって定める。

$\Sigma \unicode{x27e6} f(t_k)_{k=0}^{|f|} \unicode{x27e7} = I(f) \left ( \langle \Sigma \unicode{x27e6} t_k \unicode{x27e7} \rangle_{k=0}^{|f|} \right )$

文脈付き構成的意味論

文脈付き構成的意味論 $\Sigma_\star = \langle L, C, V, I_\star \rangle$ は形式言語 $L = \langle F, | \bullet | \rangle$ , 文脈集合 $C$ , 値集合 $V$ , 解釈 $I_\star : f \in F \mapsto g \in [ [ C \rightarrow V ]^{|f|} \rightarrow [ C \rightarrow V ] ]$ からなる組である。

このとき $\Sigma_\star$ のもとの式の意味 $\Sigma_\star \unicode{x27e6} \bullet \unicode{x27e7} : E(L) \rightarrow [ C \rightarrow V ] \$ を, つぎの帰納的定義によって定める。

$\Sigma_\star \unicode{x27e6} f(t_k)_{k=0}^{|f|} \unicode{x27e7} = I_\star(f) \left ( \langle \Sigma_\star \unicode{x27e6} t_k \unicode{x27e7} \rangle_{k=0}^{|f|} \right )$