読者です 読者をやめる 読者になる 読者になる

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

プログラミング 哲学 数学

mandel59.hateblo.jp

ここでは自然数の集合  {\bf N} は0を含むこととする。また、記法  \bullet_{k=m}^{n} の類は  k m 以上  n 未満の区間の整数を動くことを表す。 m = n の時は空の区間を表す。

形式言語

形式言語  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 L の関手,  t_1, \cdots, t_n L の式であるとき,  f(t_1, \cdots, t_n) L の式である。

構成的意味論

構成的意味論  \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 を構成できる。