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

mandel59.hateblo.jp

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

記法  \left ( a \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 が項数  n の関手であり,  t_0, \cdots, t_{n-1} が式であるとき,  f(t_0, \cdots, t_{n-1}) は式である。
    • 特に,  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 )

文脈  c \in C のもとの式  e の値は  \Sigma_\star \unicode{x27e6} e \unicode{x27e7} (c) \ になる。

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

文脈付き構成的意味論  \Sigma_\star = \langle L, C, V, I_\star\rangle から自明な構成的意味論  \Sigma ' _\star = \langle L, [ C \rightarrow V ], I_\star \rangle を構成できる。