🙆
プログラム意味論(Winskel 9章)

2023/11/11に公開
!Mathematical Logic Advent Calendar 2023の2日目の記事です。

https://adventar.org/calendars/8737
!2025/08/20に全体的に大幅に加筆修正を行い、より一般的な再帰的定義を持つ等式理論における健全性及び完全性の証明を行う内容に変更しました。

 はじめにはじめまして。記事を開いていただきありがとうございます。
この記事はプログラム意味論の古典的かつ標準的な教科書『The Formal Semantics of Programming Languages An Introduction』(Winskel, 1993)の9章(Recursion equations)の内容をもう少し一般的な形で分かりやすく書き直した内容となっております。

(cf. https://www.cin.ufpe.br/~if721/intranet/TheFormalSemanticsofProgrammingLanguages.pdf)
具体的には、RECという再帰的関数定義を持つ一階の関数型言語の操作的意味論及び表示的意味論を等式理論風のアプローチにより取り扱います。
本質的に新しい内容は含まれておりませんが、この記事がプログラム意味論初学者の方に何か新しい気づきを与えることができれば幸いに思います。
よろしくお願いします。
!スマホで見る場合は横向きにしたほうが見やすいかもしれないです。

 準備
 ノーテーションposet Pに対して、A\subseteq_\mathrm{dir}PでAが有向集合であることを表す
一般にA\subseteq_\mathrm{fin} BでAがBの有限部分集合であることを表す

\sqcup Aで有向集合のみを定義域に取る上限（有向上限と呼ぶ）を表す
集合 A上の有限列全体の集合をA^*\coloneqq\{(a_1, \dots, a_n)\mid n\in\N, a_i\in A\text{ for }1\le i\le n\}と書く
ただし、n=0のときは(a_1, \dots, a_n)は空列を表すことに注意

本記事では見やすさ・書きやすさのため集合の内包的記法\{x\in X\mid P(x)\}において、\in Xを省いてしばしば集合を\{x\mid P(x)\}のように書く
定義の際にどの集合のsubsetを定義しているかは、「A\subseteq XをA\coloneqq\{x\mid P(x)\}と定義する」のように原則型は明記するようにしているため混乱のおそれはないはず

写像の像はf[A]のように表記する
dcpo D, Eに対し、[D\to E]でDからEへの連続関数全体の集合を表す
同時代入と環境の更新（後に本文中でも触れる）
同時代入：t[u_i/x_i]_{i\le k}でt[u_1/x_1, \dots, u_k/x_k]を表す
環境の更新：\rho[u_i/x_i]_{i\le k}で\rho[u_1/x_1, \dots, u_k/x_k]を表す
特に、\Gamma内の変数を使う場合は\rho[u_x/x]_{x\in\Gamma}, t[u_x/x]_{x\in\Gamma}のようにも書く



 プログラム意味論とはプログラム意味論とは、単なる記号列である「プログラム」に「計算」によって不変な「値」を割り当てる様々な手法、及び各手法同士の関係を数学的に調べる分野です。
"1+1"という文字列をコンピュータに渡すだけで、"1"を自然数の1、"+"を自然数の足し算だと解釈し計算して文字列"2"を出力するのはよく考えれば驚くべきことです。
プログラム意味論はその疑問を深掘りします。

 有向完備半順序集合(dcpo)プログラム意味論において中心となる数学的構造である有向完備半順序集合(以下dcpoと呼ぶ)について駆け足で説明します。
詳しいお気持ちについては以下の記事をご参照ください。

https://zenn.dev/mineel5/articles/d6bc627587b72b

 定義1: 有向集合poset Pに対し、\emptyset\not=A\subseteq{P}が有向集合\Leftrightarrow \forall a, b\in{A}, \exists{c}\in{A}, a\leq{c}\ \&\ b\leq{c}
有向集合は列の一般化となっており、添字集合に有向性が課されている場面も目にします。
一般にposetにおいて有向集合に上限が存在するとは限りませんが、全ての有向集合が上限を持ち、かつposetに最小元も存在するときそのposetをdcpoと呼びます。

 定義2: dcpoposet (D, \le)が次を満たすとき、Dを有向完備半順序集合(dcpo)という。

D上の全ての有向集合が上限を持つ

Dは最小元\bot_Dを持つ
また、dcpo間の連続関数も重要な登場人物です。

 定義3: 連続関数dcpo D, Eに対し、f: D\rightarrow{E}が連続\Leftrightarrow \forall{A}\subseteq_\mathrm{dir}D, f(A)\text{ is directed}\ \&\ f(\sqcup{A})=\sqcup{f}(A)
連続関数は(部分関数空間等の)代数的dcpoとよばれる領域においては有限呼び出し性という性質を持つ重要な関数です。
ところで、常にx\le y\implies f(x)\le f(y)なる関数を単調関数と呼びますが、連続関数は必ず単調関数となります。

（x\le yなら連続関数の定義より\{f(x), f(y)\}は有向集合となり、f(y)=f(x\sqcup y)=f(x)\sqcup f(y)が成り立つため、上限の定義よりf(x)\le f(y)となる）
もちろん単調関数は常に連続になるとは限りませんが、定義域が無限増加列を持たないとき単調関数は連続関数に一致します。

 命題4: 単調関数が連続となる条件dcpo D, Eに対し、Dが狭義無限増加列を持たないとき、単調関数 f:D\rightarrow{E}は必ず連続である。
（\omega-cpoの場合は明らかだが、dcpoの場合は証明に一工夫必要。興味のある方は横内『プログラム意味論』の命題 3.2.3をご参照ください）
例として、平坦領域(flat cpo)について考えます。
例: 平坦領域集合 Xに対し、dcpo X_\bot=(X_\bot, \leq)を平坦領域という。
ただし、
X_\bot=X\cup\{\bot\}\ (\text{where }\bot\not\in{X})
x\leq{y}\Leftrightarrow x=\bot\text{ or }x=y
そのとき、平坦領域の有限直積(各点順序)は狭義無限増加列を持たないため、平坦領域の有限直積上の単調関数は必ず連続となる。
また、平坦領域への連続写像の性質を１つ紹介します。

 命題5: 平坦領域への連続写像連続写像 f, g\colon D\to X_\bot及び有向集合 A\subseteq_\mathrm{dir}Dに対し、次が成り立つ。
f(\sqcup A)=g(\sqcup A)\implies\exists a\in A, f(a)=g(a)証明連続性より、\sqcup f[A]=\sqcup g[A](=k)が成り立つ。
k=\botのとき

f[A]=g[A]=\{\bot\}より、任意のa\in Aに対しf(a)=g(a)=\botが成り立つ。（有向集合は非空であることに注意）
k=x\in Xのとき

x\in f[A]かつx\in g[A]より、あるa_1, a_2\in Aが存在して、f(a_1)=xかつg(a_2)=xが成り立つ。

Aの有向性より、a_1, a_2\le a_3なるa_3\in Aが存在し、f, gの単調性よりf(a_3)=x=g(a_3)が成り立つ。
\square

 言語REC
 RECの構文まず、今回扱うプログラミング言語RECを定義していきます。
変数記号の集合を V=\{\operatorname{x}_i\}_{i\in\mathbb{N}}とします。

関数記号は、言語にはじめから備わっている関数記号の有限集合 \Sigma=\{\sigma_i^{a_i}\}_{i\le n}及び特別な関数記号 \bot^0に加え、ユーザ定義関数の有限集合 F=\{\operatorname{f}_i^{a_i}\}_{i\leq{m}}が与えらているとします。[1]
関数記号の肩の自然数はアリティ[2]と呼ばれ、その関数記号の「引数」の数を表します。以降では、アリティは適宜省略します。

（アリティが0の関数記号は定数であることを意味します）
\Sigmaには、自然数の0を表す\mathrm{O}や+1をする演算を表す\mathrm{S}など、言語にはじめから備わっている関数記号が含まれます。

（以降頻繁に具体例として\mathrm{S}や\mathrm{O}を用いますが、別に\mathrm{S}や\mathrm{O}が\Sigmaに含まれている必要はありません）
また、これから詳細を説明するのですが、言語RECは\mathrm{add2(x)=S(S(x))}のような関数の定義式を書くことによってユーザが関数を定義できる機能が備わっており（この例では\mathrm{add2}という+2をする関数を定義した）、Fの関数記号はユーザが定義する関数を表します。

 項の定義についてまず、言語RECの項を定義します。項とはプログラムそのものを意味する概念であり、\mathrm{S(O)}や\mathrm{add(x_0, S(O))}などが（前）項の例です。（仮に\mathrm{add}\in Fとしました。）
!言語RECは関数型の言語ですので、手続き型言語で見られるif x >= 0 then x = x + 1 else  x = x - 1のような命令形のプログラムではなく、関数そのものがプログラムの単位であることに注意してください。
また、プログラム意味論の文脈では文脈と呼ばれる関数の引数（=自由変数）のリストを含めたものを項とするのが一般的[3]です。
すなわち、x_0, x_1\triangleright\mathrm{add(x_0, S(x_1))}なる形のものこそが項であり、直感的にはf(x, y)=x+(y+1)のような関数を表すことになります。
特に、引数のない\triangleright\mathrm{S(O)}のような項は閉項と呼ばれ、直感的には常に1を返す無引数関数を表します。

（JavaScriptで言えば() => 0 + 1のような関数を表します。）
!x_0, x_1, x_2\triangleright\mathrm{add(x_0, S(x_1))}のように使わない引数\mathrm{x_2}はあっても構いませんが、x_0\triangleright\mathrm{add(x_0, S(x_1))}のように自由変数x_1が残ってしまうものは項とは呼びません。
そこで、まず文脈のない前項 (pre-term)を定義します。
!良い呼び方が思いつかなかったためpre-termと呼びましたが、これは本記事独自の用語であり一般的な呼び方ではありません。

ラムダ計算において\alpha-同値関係で割る前の項をpre-termと呼ぶことがありますが、それとは関係ありません。
変数記号を表すメタ変数をx, y,...またはx_0, x_1, ...、\Sigmaの関数記号を表すメタ変数を\sigma、Fの関数記号を表すメタ変数をfと書くとします。

 定義6: 前項 (pre-term)\Sigma-前項の集合 T^\Sigma\subseteq(\{\bot\}\cup{V}\cup\Sigma)^*を次を満たす最小の集合[4]として定義する。
\bot\in{T^\Sigma}
\forall{x}\in{V}, x\in{T^\Sigma}
\forall{\sigma^a}\in\Sigma, \forall t_1,...,t_a\in{T^\Sigma},\ \sigma^at_1...t_a\in{T^\Sigma}
さらに、Fの関数記号も含めた \Sigma, F-前項の集合 T^{\Sigma, F}\subseteq(\{\bot\}\cup{V}\cup\Sigma\cup F)^*を次を満たす最小の集合として定義する。
\bot\in{T^{\Sigma, F}}
\forall{x}\in{V}, x\in{T^{\Sigma, F}}
\forall{\sigma^a}\in\Sigma, \forall t_1,...,t_a\in{T^{\Sigma, F}},\ \sigma^at_1...t_a\in{T^{\Sigma, F}}
\forall{f^a}\in{F},\ \forall t_1,...,t_a\in{T^{\Sigma, F}},\ f^at_1...t_a\in{T^{\Sigma, F}}
（アリティが0のときは、\sigma t_1\dots t_aは単に\sigmaを表すことに注意）
以降は適宜括弧を補ってf(t_1,...,t_a)などと書くこととします。

続いて、自由変数の集合\operatorname{FV}(t)を再帰的に定義します。

 定義7: 自由変数の集合各前項 t\in{T^{\Sigma, F}}に対し、自由変数の集合 \operatorname{FV}(t)\subseteq{V}を次で定義する
\operatorname{FV}(\bot)=\emptyset
\operatorname{FV}(x)=\{x\}
\operatorname{FV}(\sigma^a(t_1,...,t_a))=\operatorname{FV}(t_1)\cup...\cup\operatorname{FV}(t_a)
\operatorname{FV}(f^a(t_1,...,t_a))=\operatorname{FV}(t_1)\cup...\cup\operatorname{FV}(t_a)
そこで、前項に対して変数の有限集合\Gamma\in\mathcal{P}_\mathrm{fin}(V)で添字付けし、項を定義します。

 定義8: 項\Sigma-項の集合 T^\Sigma_{REC}\subseteq\mathcal{P}_\mathrm{fin}(V)\times{T^\Sigma}及び \Sigma, F-項の集合 T^{\Sigma, F}_{REC}\subseteq\mathcal{P}_\mathrm{fin}(V)\times{T^{\Sigma, F}}を次で定義する。
\begin{array}{rcl}
T^\Sigma_{REC} & \coloneqq & \{(\Gamma, t)\mid\mathrm{FV}(t)\subseteq\Gamma\}\\
T^{\Sigma, F}_{REC} & \coloneqq & \{(\Gamma, t)\mid\mathrm{FV}(t)\subseteq\Gamma\}\end{array}組 (\Gamma, t)が項のとき \Gamma\triangleright{t}と書き、また記法を濫用して \Gamma\triangleright{t}で項 (\Gamma, t)を表すこととします。

（このような記法の濫用は以降でも暗黙に行います）
そのとき、\Gammaのことを文脈(or環境)といい、また \Gamma=\emptysetの項を閉項といいます。
改めてまとめると、\mathrm{S(x_1)}のような式を前項と呼び、\mathrm{x_1, x_4}\triangleright\mathrm{S(x_1)}のような文脈と呼ばれる引数のリストも一緒にしたものを項と呼びます。

 等式規則と関数定義についてまず、等式規則の定義をします。

 定義9: \Sigma-等式 (\Sigma-equation)\Sigma-等式の集合E_{REC}\subseteq\mathcal{P}_\mathrm{fin}(V)\times T^\Sigma\times T^\Sigmaを次で定義する。
E_{REC}\coloneqq\{(\Gamma, t, s)\mid \mathrm{FV}(t)\cup\mathrm{FV}(s)=\Gamma\}組(\Gamma, t, s)が \Sigma-等式であるとき、\Gamma\triangleright{t}=sと書くこととします。
!\Sigma-等式の定義には \Sigma-前項を用いていることに注意です。
\Sigma-等式は、言語にはじめから備わっている関数記号が満たすべき等式を指定します。
例： \Sigma-等式
\mathrm{x_0}\triangleright\mathrm{Pred(S(x_0))=x_0}

-1をする関数\mathrm{Pred}と+1をする関数\mathrm{S}が満たすべき等式


\mathrm{x_0}\triangleright\mathrm{e\cdot x_0=x_0}
群の公理

続いて、関数定義の定義をします。

 定義10: 関数定義\Sigma, F-関数定義の集合 D_{REC}\subseteq\mathcal{P}_\mathrm{fin}(V)\times{T^{\Sigma, F}}\times{T^{\Sigma, F}}を次で定義する。
D_{REC}=\{(\Gamma, f^a(x_1, \dots, x_a), t)\mid\mathrm{FV}(t)\subseteq\Gamma=\{x_1, \dots, x_a\}\}(\Gamma, f^a(x_1, \dots, x_a), t)\in{D_{REC}}のとき\Sigma\triangleright f^a(x_1, ..., x_a)=tと書くこととします。
!\Sigma-等式も\Sigma, F-関数定義も\Gammaが余分な変数を持つことを許さない定義となっている点には注意です。
例：足し算の再帰的定義
\mathrm{x_0, x_1}\triangleright\mathrm{add(x_0, x_1)}=\text{ if }\mathrm{x_1}\text{ then }\mathrm{x_0}\text{ else }\mathrm{S(add(x_0, Pred(x_1)))}

\mathrm{if^3, S^1, Pred^1}が\Sigmaに含まれる仮定の下で、自然数の加算を行う関数\mathrm{add}の定義

\mathrm{if^3}は条件節が0のときに\text{then}の中身を返すように等式規則が定義されているとしている

しかし、関数定義は（相互）再帰的定義となっており、その定義が意味するところの関数は決して明確ではありません。
例えば、次のような関数定義を(直感的に)満たす自然数上の関数は明らかに存在しません。
\mathrm{x_0}\triangleright\mathrm{f_0(x_0)=S(f_0(x_0))}そのため、関数の再帰的定義を正確に扱うための枠組みが求められます。

そこで、領域理論が登場します。

 表示的意味論プログラム意味論には大きく分けて表示的意味論、操作的意味論、公理的意味論の3種類の意味論が存在し、この記事では前半2つの意味論について扱っていきます。

まずは表示的意味論から扱います。
表示的意味論とは、各プログラムを自然数等の数学的対象に対応させて、プログラムの振る舞いを数学的に調べる意味論です。

例えば、"1+1"という文字列は適切な表示的意味論の下で自然数の2に対応付けされます。
ここでは、各項をdcpo上の関数に対応させることを考えます。

(次節でdcpoを用いる理由について解説を行います。)

 定義11: \Sigma-領域関数記号の集合 \Sigma及びdcpo A及び\Sigmaの各関数記号をある連続関数 \llbracket\sigma^a\rrbracket\colon A^a\to Aに対応させる関数 \llbracket\rrbracketに対し、組 (A, \llbracket\rrbracket)を\Sigma-領域という。
ただし、\llbracket\sigma^a\rrbracket\colon A^a\to Aは引数に最小元が１つでもあれば最小元を返すような関数であるとする。
\llbracket\sigma\rrbracketを\sigmaの表示と言います。
!\Sigma-代数を参考に\Sigma-領域という言葉を用いましたが、一般的な言葉ではないことにご注意ください
さらに、\llbracket\rrbracketの定義域を\Sigma-項へと拡張します。（後にさらに\Sigma, F-項へと定義域を拡張します）

 定義12: \Sigma-項の表示\Sigma-領域 A=(A, \llbracket\rrbracket)に対し、\Sigma-項 \Gamma\triangleright t\in T^\Sigma_{REC}の表示 \llbracket\Gamma\triangleright{t}\rrbracket^{A}:A^{\Gamma}\to{A}を次で定義する。
\llbracket\Gamma\triangleright\bot\rrbracket^{A}\rho=\bot_A
\llbracket\Gamma\triangleright{x}\rrbracket^{A}\rho=\rho(x)
\llbracket\Gamma\triangleright{\sigma^a(t_1,...,t_a)}\rrbracket^{A}\rho=\llbracket{\sigma^a}\rrbracket(\llbracket\Gamma\triangleright{t_1}\rrbracket^{A}\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket^{A}\rho)
このとき、\rho\in{A}^{\Gamma}を環境といいます。また、\llbracket\Gamma\triangleright{t}\rrbracket^{A}の肩のAは適宜省略します。
環境は定義通り\Gamma=\{x_1, \dots, x_n\}からAへの写像\rho\colon\{x_1, \dots, x_n\}\to{A}と見てもよいですが、どちらかというと\rho=(a_1, \dots, a_n)\in{A}^nのように値の組として見たほうが直感的に分かりやすいと思います。
そうすれば、項の表示 \llbracket\Gamma\triangleright t\rrbracketも、関数の引数の組 \rho=(a_1, \dots, a_n)\in A^nを受け取り、何らかの値 a\in Aを返す関数 \llbracket\Gamma\triangleright t\rrbracket^{A}\colon A^n\to{A}として非常に直感的に解釈できます。

（特に、\llbracket\Gamma\triangleright{x}\rrbracket^{A}をx成分を返すprojectionとみなせるのは非常に重要です）
例：\Sigma-項の表示\mathrm{add}\in\Sigmaとし、\llbracket\mathrm{add}\rrbracket^A(n, m)\coloneqq n+m\colon\N_\bot^2\to\N_\botとする。

（ただし、n=\bot\text{ or }m=\botならば\llbracket\mathrm{add}\rrbracket^A(n, m)=\botとする）

このとき、\mathrm{x_0, x_1, x_2, x_3}\triangleright\mathrm{add(x_0, add(x_1, x_2))}の表示は次のように定義される。
\llbracket\mathrm{x_0, x_1, x_2, x_4}\triangleright\mathrm{add(x_0,add( x_1, x_2))}\rrbracket^{A}(a, b, c, d)=a+b+c（ただし、a, b, c\in\N_\botの１つでも\botなら返り値も\botとなる。ただし、dは\botでも構わない）
!使わない引数は\botでも構わないという認識は非常に怪しくて、後にも軽く触れますがこれは所謂値呼びの意味論なため、\sigma\in\Sigma, f\in Fの引数では（使われなくても）１つでも\botがあれば\botを必ず返すような定義となっています。
例えば、\llbracket\mathrm{add\_first\_two}\rrbracket^A(a, b, c)\coloneqq a+bのような関数では、次のようになります。
\llbracket\mathrm{x_0, x_1, x_2\triangleright add\_first\_two(x_0, x_1, x_2)}\rrbracket^A(a, b, \bot)=\bot
環境を明示しない定義環境を明示せずに、
\llbracket\Gamma\triangleright\bot\rrbracket=\bot_{[A^\Gamma\to A]}
\llbracket\Gamma\triangleright{x}\rrbracket=\pi^\Gamma_x
\llbracket\Gamma\triangleright{\sigma^a(t_1,...,t_a)}\rrbracket^{A}=\llbracket{\sigma^a}\rrbracket\circ\langle\llbracket\Gamma\triangleright{t_1}\rrbracket^{A}, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket^{A}\rangle
のような定義を採用するか悩みましたが、一般的には環境を明示したほうが分かりやすいと思ったので、環境を明示する定義を採用しました。
ただ、このような書き方の方が圏論的な意味論へと移りやすいとは思います。

 不動点と再帰的定義ここまでで、\Sigma-領域の定義を行いました。

\Sigma-領域の定義では、各関数記号 \sigma^a\in\Sigmaに対してデフォルトで等式制約を満たす演算 \llbracket\sigma^a\rrbracket\colon A^a\to Aが与えられています。
しかし、ユーザのの定義の関数定義の表示は大きく事情が異なります。

これはユーザが後から定義を与えるものなので、モデルに表示 \llbracket{f}\rrbracket^{A, D}\colon A^a\rightarrow{A}がデフォルトで備わっているわけではありません。
むしろ、自ら定義式を満たす \llbracket{f}\rrbracket^{A, D}\colon A^a\to Aを、すなわち、関数方程式の解を探す必要があります。
もし \mathrm{f(x_0)=S(f(x_0))}のような解が明らかに存在しない場合はないことを言いたいし、もし解が存在するような関数定義ならばその解を表示として与えたいです。
そこで、ようやくわざわざdcpoを意味領域に用いた恩恵を受けることができます。
まず、領域理論における最も重要な定理である連続関数の不動点定理を証明無しで紹介します。

 定理13: 不動点定理dcpo A, B及び連続関数 f\colon A\to Bに対し、Aの最小元を \bot_Aとすれば次が成り立つ
f(\operatorname{fix}f) = \operatorname{fix}fただし、
\operatorname{fix}f\coloneqq\sqcup_{n\in\mathbb{N}}{f^n(\bot_A)}(つまり、 \operatorname{fix}は最小不動点を与える関数)
任意の関数が不動点を持つというのは一見ありえないように思えますが、実際はf(x)=x+1など明らかに不動点を持たない関数は不動点が存在しないことを意味する最小元 \bot_Aを不動点として持つというだけの話です。
しかし、\bot_Aを導入することにより不動点を滑らかに、かつ統一的に扱うことを可能にした点こそが領域理論の最大の成果だと考えております。
ところで、不動点は再帰的定義と深い関係があります。
例えば、階乗関数factの再帰的定義はOCamlでは以下のように行われます。
階乗関数 in Ocaml
let rec fact = fun x -> if x > 0 then x * fact (x - 1) else 1;;
これは見方を変えればfactが不動点になっていると見ることができ、領域理論においては上記の定理より不動点は必ず存在するので関数factが得られるわけです。
今、RECの意味領域にはdcpoを採用したため、ユーザ定義の関数記号 f^a\in{F}のD\subseteq_\mathrm{fin}D_{REC}における表示 \llbracket{f^a}\rrbracket^{A, D}\colon A^a\to{A}も（最小）不動点として必ず得られることになります。

（もし定義式を満たす関数が存在しない場合は単純に最小元 \bot_{[A^a\to A]}が得られるだけ。）

 ユーザ定義関数の意味付け関数定義の集合 D\subseteq_\mathrm{fin}D_{REC}の中でも、左辺にFの各関数記号がちょうど一度ずつ現れるものを取ります。
!以降では特に断りなく、D\subseteq_\mathrm{fin}D_{REC}は常にそのような関数定義の集合を取るとします。
その際、各f\in Fに対し、Dにおいてfに対応する項と文脈がただ１つに定まるので、それをt^D_f, \Gamma^D_fと書くこととします。（肩のDは適宜省略する）
それでは、D\subseteq_\mathrm{fin}D_{REC}におけるユーザ定義関数の表示を与える関数\llbracket\rrbracket^{A, D}を最小不動点として、すなわち、何らかの関数方程式の解としてさくっと得ちゃいましょう。
まず、各f\in Fに対し、ある連続関数 \varphi(f)を対応させる関数 \varphiで、\varphi(f^a)は引数に最小元が１つでもあれば最小元を返すような関数となる関数 \varphiを関数環境と呼びます。
そのとき、\varphiがDの各定義式を満たすためには、\varphiは関数定義 \Gamma_f\triangleright{f}(x_1, ..., x_a)=t_fに対し、(直感的に)次を満たしていてほしいです。

\varphi(f^a)(d_1,...,d_a)=\llbracket\Gamma_f\triangleright{t_f}\rrbracket\varphi\rho[d_1/x_1,...,d_a/x_a]
この式の詳細な定義環境の更新\rho[d/y]を次で定義しています。

\begin{equation*}
    \rho[d/y](x)=
    \left\{
        \begin{array}{ll}
            \rho(x) & if\  x\not=y \\
            d & if\ x=y
        \end{array}
    \right.
\end{equation*}
\rho[d_1/x_1,...,d_a/x_a]でa個の変数値の更新を表し、以降ではしばしば\rho[d_i/x_i]_{i\leq{a}}という略記を用います。

特に、今は\Gamma_f=\{x_1, ..., x_a\}なので、このような場合は\rho[d_x/x]_{x\in\Gamma_f}のようにも書き、しばしば勝手に変数と添字を同一視します。

（本当はi番目の変数 x_iに対応する値はi番目の値 d_iなのですが、これをd_{x_i}とも書くこともあるということです）
さらに、ここでの右辺の\llbracket\rrbracketは次のように関数環境と環境を受け取るように修正し、定義域を\Sigma, F-項へと拡張したものです。
\llbracket\Gamma\triangleright\bot\rrbracket\varphi\rho=\bot
\llbracket\Gamma\triangleright{x}\rrbracket\varphi\rho=\rho(x)
\llbracket\Gamma\triangleright{\sigma^a(t_1,...t_a)}\rrbracket\varphi\rho=\llbracket{\sigma^a}\rrbracket(\llbracket\Gamma\triangleright{t_1}\rrbracket\varphi\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket\varphi\rho)
\llbracket\Gamma\triangleright{f^a(t_1,...,t_a)}\rrbracket\varphi\rho=\varphi(f^a)(\llbracket\Gamma\triangleright{t_1}\rrbracket\varphi\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket\varphi\rho)
すなわち、関数環境 \varphiの関数方程式が得られました。

故に、与えられた関数定義 D\subseteq_\mathrm{fin}D_{REC}を満たす関数環境 \varphiは次の関数 Fの最小不動点として得ることができます。

F(\varphi)(f)(d_1, ..., d_a)=\llbracket\Gamma_f\triangleright{t_f}\rrbracket\varphi\rho[d_x/x]_{x\in\Gamma_f}
（Fが連続であることも確認する必要があるのですが、tの構造帰納法により示されます。また、Fは\rhoに依らず定義されることも示す必要があります）
関数環境がなすdcpo関数環境 \varphi, \psiに対して、

\varphi\le\psi\iff\forall f^a\in F, \forall d_1, ..., d_a\in A,\ \varphi(f^a)(d_1, ..., d_a)\le\psi(f^a)(d_1, ..., d_a)
とすれば、これはdcpoをなす。
そこで、関数定義の集合 D\subseteq_\mathrm{fin}D_{REC}の定義式を全て満たす関数環境 \llbracket\rrbracket^{A, D}を
\llbracket\rrbracket^{A, D}\coloneqq\operatorname{fix}Fとして定義します。
これより、\Sigma-項の表示は以下のように\Sigma, F-項の表示へと拡張することができます。

 定義14: \Sigma, F-項の表示\Sigma-領域 A=(A, \llbracket\rrbracket)を固定する。関数定義の集合 D\subseteq_\mathrm{fin}D_{REC}に対し、Dにおける\Sigma, F-項 \Gamma\triangleright{t}\in{T^{\Sigma, F}_{REC}}の表示 \llbracket\Gamma\triangleright{t}\rrbracket^{A, D}:A^{\Gamma}\to{A}を次で定義する。
\llbracket\Gamma\triangleright\bot\rrbracket^{A, D}\rho=\bot_A
\llbracket\Gamma\triangleright{x}\rrbracket^{A, D}\rho=\rho(x)
\llbracket\Gamma\triangleright{\sigma^a(t_1,...,t_a)}\rrbracket^{A, D}\rho=\llbracket{\sigma^a}\rrbracket(\llbracket\Gamma\triangleright{t_1}\rrbracket^{A, D}\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket^{A, D}\rho)
\llbracket\Gamma\triangleright{f^a(t_1,...,t_a)}\rrbracket^{A, D}\rho=\llbracket f^a\rrbracket^{A, D}(\llbracket\Gamma\triangleright{t_1}\rrbracket^{A, D}\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket^{A, D}\rho)
今、与えられた等式制約 E\subseteq_\mathrm{fin} E_{REC}を満たす\Sigma-領域を\langle\Sigma|E\rangle-領域モデルと呼ぶとします。

 定義15: \langle\Sigma|E\rangle-領域モデル\Sigma-領域 A=(A, \llbracket\rrbracket)及び等式集合 E\subseteq_\mathrm{fin} E_{REC}の組 (A, E)は次を満たすとき、\langle\Sigma|E\rangle-領域モデルという。
\forall(\Gamma, t, s)\in{E},\llbracket\Gamma\triangleright{t}\rrbracket^{A}=\llbracket\Gamma\triangleright{s}\rrbracket^{A}簡単のため、等式制約 E\subseteq_\mathrm{fin} E_{REC}が文脈から明らかなときは、Eの等式を全て満たす\Sigma-領域自体を\langle\Sigma|E\rangle-領域モデルと呼ぶことにします。
そこで、等式制約E\subseteq_\mathrm{fin} E_{REC}と関数定義D\subseteq_\mathrm{fin}D_{REC}, \langle\Sigma|E\rangle-領域モデルA, 環境 \rho\in A^\Gamma及び文脈を共有する\Sigma, F-項 \Gamma\triangleright t, \Gamma\triangleright s に対して、以下のノーテーションを定めます。
\langle\Sigma|E|F|D\rangle, A, \rho\vDash\Gamma\triangleright{t}=s\iff\ \llbracket\Gamma\triangleright{t}\rrbracket^{A, D}\rho=\llbracket\Gamma\triangleright{s}\rrbracket^{A, D}\rho
\langle\Sigma|E|F|D\rangle, A\vDash\Gamma\triangleright{t}=s\iff\forall\rho\in{A}^{\Gamma},\ \langle\Sigma|E|F|D\rangle, A, \rho\vDash\Gamma\triangleright{t}=s
\langle\Sigma|E|F|D\rangle\vDash\Gamma\triangleright{t}=s\iff\forall A:\langle\Sigma|E\rangle\text{-model},\ A\vDash\Gamma\triangleright{t}=s
\langle\Sigma|E|F|D\rangleはしばしば省略し、\Gamma\triangleright\vDash t=sのような記法を用います。

 操作的意味論操作的意味論とは、プログラムの書き換え規則により形式的に推論される標準形という特殊な項をプログラムの意味とする意味論です。
一般に、操作的意味論にはbig step semantics(自然意味論)とsmall step semantics(構造意味論)の大きく2種類があります。[5]
前者が最終的な評価値による意味論で、後者が"1ステップ"の評価による意味論となっております。
本来は操作的意味論を定義したかったのですが、今回は一般的な形での等式理論を扱っているため、代わりに\Sigma-等式の集合 E\subseteq_\mathrm{fin} E_{REC}から導かれる合同関係 \langle\Sigma|E|F|D\rangle\vdash\Gamma\triangleright t=sを扱うことにします。

 定義16: 合同関係等式制約 E\subseteq_\mathrm{fin} E_{REC}及び関数定義 D\subseteq_\mathrm{fin}D_{REC}を固定する。

そこで、文脈を共有する\Sigma, F-項 \Gamma\triangleright t, \Gamma\triangleright s\in{T^{\Sigma, F}_{REC}}に対し、E, Dから誘導される合同関係 \langle\Sigma|E|F|D\rangle\vdash\Gamma\triangleright t=sを次で定義する。

（以降では見やすさのため\vdash\Gamma\triangleright t=sと書くことにする）

\begin{equation}
\frac{\bot\in\{t_1, \dots, t_a\}}{\vdash\Gamma\triangleright g^a(t_1, \dots, t_a)=\bot}\tag{bot}
\end{equation}

\begin{equation}
\frac{\Gamma\triangleright t=s\in E\cup D\phantom{　}\Gamma\subseteq\Gamma'}{\vdash\Gamma'\triangleright t=s}\tag{axiom}
\end{equation}

\begin{equation}
\frac{}{\vdash\Gamma\triangleright t=t}\tag{refl}
\end{equation}

\begin{equation}
\frac{\vdash\Gamma\triangleright t=s}{\vdash\Gamma\triangleright s=t}\tag{sym}
\end{equation}

\begin{equation}
\frac{\vdash\Gamma\triangleright t=s\phantom{　}\vdash\Gamma\triangleright s=u}{\vdash\Gamma\triangleright t=u}\tag{trans}
\end{equation}

\begin{equation}
\frac{\vdash\Gamma\triangleright t=s\phantom{　}\vdash\Gamma\triangleright u_1=u'_1\phantom{　}\cdots\phantom{　}\vdash\Gamma\triangleright u_k=u'_k}{\vdash\Gamma\triangleright t[u_1/x_1,...,u_k/x_k]=s[u'_1/x_1,...,u'_k/x_k]}\tag{subst}
\end{equation}
（最後のsubst規則のx_1, \dots, x_kは任意の変数）

（また、bot規則のgは\SigmaかFの関数記号であるとする）
代入の定義の捕捉通常の代入は以下のように定義されます。
\bot[u/x]=\bot
x[u/x]=u

y[u/x]=y (y\neq{x})
\sigma^a(t_1,...,t_a)[u/x]=\sigma^a(t_1[u/x], ..., t_a[u/x])
f^a(t_1,...,t_a)[u/x]=f^a(t_1[u/x], ..., t_a[u/x])
t[u_1/x_1,...,u_k/x_k]は変数x_1, \dots, x_kを全て同時に置き換えた項を表します。しかし、同時代入の定義はもう少し煩雑となり、興味のある方は演習問題としてぜひ自分で定義を行ってみてください。（ラムダ計算の記事でも詳細な定義を紹介しています）
ちなみに、ラムダ計算では変数の捕捉という問題に気をつける必要があり、ラムダ計算における代入は非常に微妙な問題となります。
!この辺の定義は文献によって少し異なることがあります。特に、subst規則は\Gamma'=\{x_1, \dots, x_k\}として

\frac{\vdash\Gamma'\triangleright t=s\phantom{　}\vdash\Gamma\triangleright u_1=u'_1\phantom{　}\cdots\phantom{　}\vdash\Gamma\triangleright u_k=u'_k}{\vdash\Gamma\triangleright t[u_1/x_1,...,u_k/x_k]=s[u'_1/x_1,...,u'_k/x_k]}\text{ (subst)}
のように定義されることがあります。
しかし、本記事ではAxiom規則の弱化を許しているため、文脈は常に弱化された共通の文脈を使うこととしました。そうすると、subst規則の変数x_1, \dots, x_kは別に\Gamma内の変数である必要がなくなり、定義が少しシンプルになります。
bot規則では、引数に１つでも未定義があれば全体も未定義であることを意味し、プログラム意味論の言葉で値呼びと呼ばれる評価方法を表しています。

（特に触れていませんでしたが、よく読めば表示的意味論でも同様の評価方法を採用しています）
このとき、axiomは余分な変数を含まないという定義を採用していることから、axiomの弱化規則と合わせて、文脈から不要な変数を取り除いたり、逆に不要な変数を加えたりできることが言えます。

 命題17: 文脈の弱化など\forall E\subseteq_\mathrm{fin} E_{REC}, \forall D\subseteq_\mathrm{fin}D_{REC}, \forall{\Gamma\triangleright t, \Gamma\triangleright s}\in{T}^{\Sigma, F}_{REC}, \forall\Gamma'\supseteq\mathrm{FV}(t)\cup\mathrm{FV}(s)
\langle\Sigma|E|F|D\rangle\vdash\Gamma\triangleright t=s\implies\langle\Sigma|E|F|D\rangle\vdash\Gamma'\triangleright t=s
 意味論の等価性
 意味論の等価性とは勝手に言語RECを2種類の方法で意味付けしましたが、出来ればこれらが等価になっていてほしいです。
すなわち、次が成り立っていてほしいです。

 定理18: 意味論の等価性\forall E\subseteq_\mathrm{fin} E_{REC}, \forall D\subseteq_\mathrm{fin}D_{REC}, \forall{\Gamma\triangleright t, \Gamma\triangleright s}\in{T}^{\Sigma, F}_{REC}
\langle\Sigma|E|F|D\rangle\vdash\Gamma\triangleright t=s\iff\langle\Sigma|E|F|D\rangle\vDash\Gamma\triangleright t=s\Rightarrowを健全性、\Leftarrowを完全性と呼びます。
定理と書いてしまいましたが、これが実際に成り立つことをこれから示していきます。

 健全性まず、健全性を証明します。

 補題19: 意味と代入の可換性\llbracket\Gamma\triangleright{t[u_1/x_1,...,u_k/x_k]}\rrbracket\rho=\llbracket\Gamma\triangleright{t}\rrbracket\rho[\llbracket\Gamma\triangleright u_1\rrbracket\rho/x_1, \dots, \llbracket\Gamma\triangleright u_k\rrbracket\rho/x_k]（tの構造帰納法により証明可能）

 定理20: 健全性\forall E\subseteq_\mathrm{fin} E_{REC}, \forall D\subseteq_\mathrm{fin}D_{REC}, \forall{\Gamma\triangleright t, \Gamma\triangleright s}\in{T}^{\Sigma, F}_{REC}
\langle\Sigma|E|F|D\rangle\vdash\Gamma\triangleright t=s\implies\langle\Sigma|E|F|D\rangle\vDash\Gamma\triangleright t=s証明 (Sketch)規則帰納法で示す。
Bot規則：

\llbracket g^a\rrbracket\colon A^a\to Aは引数に１つでも最小元があれば最小元を返すような関数であったため、\llbracket\Gamma\triangleright g^a(t_1, \dots, t_a)\rrbracket\rho=\llbracket\Gamma\triangleright\bot\rrbracket\rhoが成り立つ。
Axiom規則：

\langle\Sigma|E\rangle-領域モデルの定義及び\llbracket\rrbracket^{A, D}の定義より成り立つ。
Refl, Sym, Trans規則：

明らか
Subst規則：

\vdash\Gamma\triangleright t=s, \vdash\Gamma\triangleright u_i=u'_iが成り立っていると仮定する。

帰納法の仮定より、任意の\langle\Sigma|E\rangle-領域モデル Aと環境 \rho\in A^\Gammaに対して、\llbracket\Gamma\triangleright{t}\rrbracket\rho=\llbracket\Gamma\triangleright{s}\rrbracket\rho及び \llbracket\Gamma\triangleright{u_i}\rrbracket\rho=\llbracket\Gamma\triangleright{u'_i}\rrbracket\rhoが成り立つ。



よって、補題19より

\begin{array}{rcl}\llbracket\Gamma\triangleright{t[u_i/x_i]_{i\le k}}\rrbracket\rho & = & \llbracket\Gamma\triangleright{t}\rrbracket\rho[\llbracket\Gamma\triangleright u_i\rrbracket\rho/x_i]_{i\leq{k}}\\&=&\llbracket\Gamma\triangleright{s}\rrbracket\rho[\llbracket\Gamma\triangleright u'_i\rrbracket\rho/x_i]_{i\leq{k}}\\&=&\llbracket\Gamma\triangleright{s[u'_i/x_i]_{i\le k}}\rrbracket\rho\end{array}
\square

 項モデル次に完全性を証明します。

 定理21: 完全性\forall E\subseteq_\mathrm{fin} E_{REC}, \forall D\subseteq_\mathrm{fin}D_{REC}, \forall{\Gamma\triangleright t, \Gamma\triangleright s}\in{T}^{\Sigma, F}_{REC}
\langle\Sigma|E|F|D\rangle\vDash\Gamma\triangleright t=s\implies\langle\Sigma|E|F|D\rangle\vdash\Gamma\triangleright t=s完全性の証明は往々にして似たような証明になるのですが、ここでは項モデルを用いた証明を与えます。
項モデルとは、項の意味として項そのものを用いるモデルのことです。
そのため項モデルによる意味論は本当の意味で表示的意味論を構築できたとはとても言えず、「構文的な意味論」だと揶揄(?)されます。
しかし、項モデルは完全性を示す際にはとても有用なモデルとなります。

 定義22: 項モデル等式制約 E\subseteq_\mathrm{fin} E_{REC}に対し、\langle\Sigma|E\rangle-領域モデル TM=(T^{\Sigma, F}/\mathord{\sim}, \llbracket\rrbracket)を項モデルという。
ただし、t\sim s\iff\exists\Gamma,\vdash\Gamma\triangleright t=sであり、\sigma^a\in\Sigmaに対し、\llbracket\sigma^a\rrbracket:(T^{\Sigma, F}/\mathord{\sim})^a\rightarrow T^{\Sigma, F}/\mathord{\sim}は次で定義する(well-defined)

\llbracket\sigma^a\rrbracket([t_1], ..., [t_a]) = [\sigma^a(t_1, ..., t_a)]
(ただし、 [t]で \Sigma, F-前項 tの同値類を表す)
また、T^{\Sigma, F}/\mathord{\sim}は同値類 [\bot]を最小元に持つ平坦領域とみなしている。
\llbracket\sigma\rrbracketの連続性を示すには命題4より単調性を言えばよいですが、bot規則より確かに成り立ちます。

（もちろん引数に１つでも最小元があれば最小元を返すような関数であることも確認できます）
また、項モデルが等式制約 E\subseteq_\mathrm{fin} E_{REC}を全て満たすことも、\Gamma\triangleright t=s\in Eに対し、示すべき命題 \llbracket\Gamma\triangleright{t}\rrbracket\rho=\llbracket\Gamma\triangleright{s}\rrbracket\rhoは次の補題により [t[u_x/x]_{x\in\Gamma}]=[s[u_x/x]_{x\in\Gamma}]と同値になりますが、これはsubst規則から成り立つことが分かります。

 補題23: 項モデルの性質\Sigma-項 \Gamma\triangleright t\in T^\Sigma_{REC}に対して、次が成り立つ。（\Sigma, F-項でないことに注意）
\llbracket\Gamma\triangleright t\rrbracket^{TM, D}\rho=[t[u_x/x]_{x\in\Gamma}]（ただし、項モデル上の環境 \rho\in{(T^{\Sigma, F}/\mathord{\sim})}^\Gammaに対し、\rho(x)=[u_x]とした）
証明
t\equiv\botのとき

\llbracket\Gamma\triangleright\bot\rrbracket^{TM, D}\rho=\bot_{TM}=[\bot]

t\equiv y\in\Gammaのとき

\llbracket\Gamma\triangleright{y}\rrbracket^{TM, D}\rho=\rho(y)=[u_y]=[y[u_x/x]_{x\in\Gamma}]

t\equiv z\not\in\Gammaのとき

\llbracket\Gamma\triangleright{z}\rrbracket^{TM, D}\rho=[z]

t\equiv\sigma^a(t_1, ..., t_a)のとき

帰納法の仮定より\llbracket\Gamma\triangleright t_i\rrbracket^{TM, D}\rho=[t_i[u_x/x]_{x\in\Gamma}]が成り立つので、
\begin{array}{rcl}\llbracket\Gamma\triangleright\sigma^a(t_1, ..., t_a)\rrbracket^{TM, D}\rho & = & \llbracket\sigma^a\rrbracket(\llbracket\Gamma\triangleright t_1\rrbracket^{TM, D}\rho, ..., \llbracket\Gamma\triangleright t_a\rrbracket^{TM, D}\rho)\\
& = & \llbracket\sigma^a\rrbracket([t_1[u_x/x]_{x\in\Gamma}], ..., [t_a[u_x/x]_{x\in\Gamma}])\\
& = & [\sigma^a(t_1[u_x/x]_{x\in\Gamma}, ..., t_a[u_x/x]_{x\in\Gamma})]\\
& = & [\sigma^a(t_1, ..., t_a)[u_x/x]_{x\in\Gamma}]\\
\end{array}\square
補題23の補足勝手に\rho(x_i)から代表元 u_iを取ってきましたが、[u_x]=[u'_x]なら、subst規則より[t[u_x/x]_{x\in\Gamma}]=[t[u'_x/x]_{x\in\Gamma}]が成り立つので代表元 u_x\in T^\Sigmaの取り方には依存しないことに注意してください。

subst規則適用時に\mathrm{FV}(u_x)\subseteq\Gammaなのかは気になりますが、文脈は常に弱化可能なのであまり気にしないとします。
一応より正確な説明を行うと、任意の変数全体での環境 \rho\in(T^{\Sigma, F}/\mathord\sim)^Vに対し、十分広い（=\forall x\in\Gamma, \forall u\in\rho(x), \mathrm{FV}(u)\subseteq\Gammaとなるような）文脈を持つ任意の項 \Gamma\triangleright t\in{T^{\Sigma, F}_{REC}}に取ってきた際に、\rhoの\Gammaへの制限 \rho\restriction_\Gammaに対し、\llbracket\Gamma\triangleright t\rrbracket^{TM, D}\rho\restriction_\Gamma=[t[u_x/x]_{x\in\Gamma}]が成り立つことを示していると考えるとよいかと思います。
補題24にも同様の問題が存在しますが、同じように考えて下さい。
一般の\Sigma, F-項に対してもこれが不等号で成り立つという主張が成り立つことが完全性定理の主張でもあり、本記事の最大の目的でもあります。

 完全性の証明今、ユーザ定義関数の表示を与える\llbracket\rrbracket^{A, D}は定義及び不動点定理より、\llbracket\rrbracket^{A, D}\coloneqq\sqcup_{n\in\mathbb{N}}F^n(\bot)でした。

(ただし、F(\varphi)(f)(d_1, ..., d_a)\coloneqq\llbracket\Gamma_f\triangleright{t_f}\rrbracket\varphi\rho[d_x/x]_{x\in\Gamma})
そこで、\delta^{(r)}\coloneqq F^r(\bot)、すなわち\llbracket\rrbracket^{A, D}のr番目の近似と定義します。つまり、

\delta^{(r)}(f^a)(d_1, ..., d_a) =
\left\{
  \begin{array}{ll}
      \bot & \text{if }r=0 \\
      \llbracket\Gamma_f\triangleright{t_f}\rrbracket\delta^{(r-1)}\rho[d_x/x]_{x\in\Gamma} & \text{otherwise}
  \end{array}
\right.
とします。
そこで、次をrの帰納法により示します。

 補題24: 完全性定理の補題E\subseteq_\mathrm{fin} E_{REC}, D\subseteq_\mathrm{fin}D_{REC}を固定する。そのとき、次が成り立つ。
\forall r\in\N, \forall{\Gamma\triangleright{t}, \Gamma\triangleright s}\in{T^{\Sigma, F}_{REC}}, \forall\rho\in(T^{\Sigma, F}/\mathord\sim)^\Gamma

\llbracket\Gamma\triangleright{t}\rrbracket^{TM, D}\delta^{(r)}\rho=\llbracket\Gamma\triangleright{s}\rrbracket^{TM, D}\delta^{(r)}\rho\implies[t[u_y/y]_{y\in\Gamma}]=[s[u_y/y]_{y\in\Gamma}]
（ただし、\rho(y)=[u_y]とした。補題23と同様に代表元 u_y\in T^{\Sigma, F}の取り方に依存しないことに注意）
証明示すべき命題は以下と同値なため、次を自然数 r\in\Nの数学的帰納法により示す。

(平坦領域Aにおいて、x\leq{y}\iff{x}=\bot_A\text{ or }x=yに注意)

\llbracket\Gamma\triangleright{t}\rrbracket^{TM, D}\delta^{(r)}\rho\leq[t[u_y/y]_{y\in\Gamma}]
以下簡単のため、前項 tにダッシュをつけることでt[u_y/y]_{y\in\Gamma}を表すとし、\llbracket\Gamma\triangleright{t}\rrbracket\delta^{(r)}\rho\leq[t']を示す。
r=0のとき

tの構造帰納法により示す。

t\equiv\botのとき

\llbracket\Gamma\triangleright{\bot}\rrbracket\delta^{(0)}\rho=[\bot]=[t']

t\equiv{y_i}のとき

\llbracket\Gamma\triangleright{y_i}\rrbracket\delta^{(0)}\rho=[u_i]=[t']

t\equiv\sigma^a(t_1, ..., t_a)のとき

  \begin{array}{lll}
  &\llbracket\Gamma\triangleright{t}\rrbracket\delta^{(0)}\rho\\ = & \llbracket\sigma\rrbracket(\llbracket\Gamma\triangleright{t_1}\rrbracket\delta^{(0)}\rho, ..., \llbracket\Gamma\triangleright{t_a}\rrbracket\delta^{(0)}\rho) & \\
  \leq & \llbracket\sigma\rrbracket([t_1'], ...,  [t_a']) & (\because \text{IH \& }\llbracket\sigma\rrbracket:\text{monotone}) \\
  = & [\sigma(t'_1, ..., t'_a)] & (\because \llbracket\sigma\rrbracket\text{'s def}) \\
  = & [t'] & 
  \end{array}
  
t\equiv f^a(t_1, ..., t_a)のとき

\delta^{(0)}(f)=\botなため、\llbracket\Gamma\triangleright{t}\rrbracket\delta^{(0)}\rho=[\bot]\le[t']
r > 0のとき

tの構造帰納法により示す。

t\equiv\bot, y_i, \sigma^a(t_1, ..., t_a)のときは上と変わらないためt\equiv{f^a}(t_1, ..., t_a)のときのみ示す。

\newline

まず、構造帰納法の仮定より、各x\in\Gamma_fで次が成り立つ。

\begin{equation}
\llbracket\Gamma\triangleright{t_x}\rrbracket\delta^{(r)}\rho\leq[t'_x]
\end{equation}
\phantom{h　}よって、\llbracket\Gamma\triangleright{t}_f\rrbracketの単調性[6] （(2)とする）より、

\begin{array}{lll}
& \llbracket\Gamma\triangleright{t}\rrbracket\delta^{(r)}\rho\\ = & \llbracket\Gamma_f\triangleright t_f\rrbracket\delta^{(r-1)}\rho[\llbracket\Gamma\triangleright{t_x}\rrbracket\delta^{(r)}\rho/x]_{x\in\Gamma_f} & (\because \delta^{(r)}\text{'s def}) \\
\leq & \llbracket\Gamma_f\triangleright t_f\rrbracket\delta^{(r-1)}\rho[[t_x']/x]_{x\in\Gamma_f} & (\because (1)\ \& \ (2))\\
\leq  & [t_f[t'_x/x]_{x\in\Gamma_f}] & (\because\text{ IH of }r) \\
= & [f(t_1', ..., t_a')] & (\because t_fのdef) \\
= & [t']
\end{array}
\square
完全性は上の補題から直ちに得られます。

 定理21: 完全性（再掲）\forall E\subseteq_\mathrm{fin} E_{REC}, \forall D\subseteq_\mathrm{fin}D_{REC}, \forall{\Gamma\triangleright t, \Gamma\triangleright s}\in{T}^{\Sigma, F}_{REC}
\langle\Sigma|E|F|D\rangle\vDash\Gamma\triangleright t=s\implies\langle\Sigma|E|F|D\rangle\vdash\Gamma\triangleright t=s証明仮定より、TM\vDash\Gamma\triangleright t=sが成り立つため、任意の\rhoに対して、\llbracket\Gamma\triangleright{t}\rrbracket^{TM, D}(\sqcup_{n\in\N}\delta^{(r)})\rho=\llbracket\Gamma\triangleright{s}\rrbracket^{TM, D}(\sqcup_{n\in\N}\delta^{(r)})\rhoが成り立つ。
よって、命題5より、あるr\in\Nで任意の環境 \rho\in(T^{\Sigma, F}/\mathord\sim)^\Gammaに対して \llbracket\Gamma\triangleright{t}\rrbracket^{TM, D}\delta^{(r)}\rho=\llbracket\Gamma\triangleright{s}\rrbracket^{TM, D}\delta^{(r)}\rhoが成り立つ。
ゆえに、補題24より、[t]=[s]が成り立ち（\rho(y_i)=[y_i]とすればよい）、定義よりある\Gamma'で\vdash\Gamma'\triangleright t=sが成り立つ。
したがって、命題17より、\vdash\Gamma\triangleright t=sが成り立つ。

\square
以上により、健全性及び完全性から意味論の等価性が示せました。

 おわりにお疲れ様でした。ここまで読んでいただきありがとうございました。
プログラム意味論というタイトルでしたが、やってることは等式理論における健全性及び完全性の証明そのもので、ほとんどタイトル詐欺みたいな内容になってしまいました。
しかし、RECで面白いのは、プログラミング言語らしく自分で関数を定義できる機能がついているという点にあると思います。
これは通常の等式理論には存在しない概念であり、そのため再帰的定義を扱うために領域理論を用いて\Sigma-代数を\Sigma-領域に拡張するという試みを行ってみました。
以上でこの記事は終わりとなります。
読みにくい部分も多々あったかと思われますが、少しでも面白いと思っていただけたら幸いです。
結構雰囲気で書いているため、数学的な間違いがございましたらここにご報告いただけると助かります。

また、正直たくさんの誤魔化しも存在しているため、気になる点や分からない点がありましたらご質問をいただければできるだけ対応いたします。
改めて本当にありがとうございました。お疲れ様でした。

 参考文献[1] The Formal Semantics of Programming Languages: An Introduction, Glynn Winskel, 1993.
[2] 横内寛文, プログラム意味論, 1994.

脚注
理論の一般化に焦点を当てているため、教科書とは異なる一般的な問題設定になっていることに注意してください。 ↩︎
アリティは厳密には関数記号に自然数を割り当てる関数\mathrm{ar}\colon\Sigma\cup F\to\Nと定義されます。すなわち、例えば\mathrm{S}^1というのは\mathrm{ar}(\mathrm{S})=1であることを意味します。 ↩︎
文脈の代わりにgraded setという概念を用いる場合もありますが、ほとんど同じことです。 ↩︎
このような集合の帰納的な定義方法等は再帰的定義の数学的取り扱いという記事で詳しく説明しております。 ↩︎
big step意味論は発散する計算の扱いが難しいという特徴があります。

そこで、発散する計算に関して余帰納的な定義を与えbig step意味論でも発散する計算を扱おうとする研究もあります。(cf. Coinductive big-step operational semantics) ↩︎
構造帰納法により任意の項で関数 \llbracket\Gamma\triangleright t\rrbracket\colon A^\Gamma\to Aの連続性が示せます。 ↩︎
はじめに

準備

ノーテーション

プログラム意味論とは

有向完備半順序集合(dcpo)

定義1: 有向集合

定義2: dcpo

定義3: 連続関数

命題4: 単調関数が連続となる条件

例: 平坦領域

命題5: 平坦領域への連続写像

言語REC

RECの構文

項の定義について

定義6: 前項 (pre-term)

定義7: 自由変数の集合

定義8: 項

等式規則と関数定義について

定義9: \Sigma-等式 (\Sigma-equation)

例： \Sigma-等式

定義10: 関数定義

例：足し算の再帰的定義

表示的意味論

定義11: \Sigma-領域

定義12: \Sigma-項の表示

例：\Sigma-項の表示

不動点と再帰的定義

定理13: 不動点定理

ユーザ定義関数の意味付け

定義14: \Sigma, F-項の表示

定義15: \langle\Sigma|E\rangle-領域モデル

操作的意味論

定義16: 合同関係

命題17: 文脈の弱化など

意味論の等価性

意味論の等価性とは

定理18: 意味論の等価性

健全性

補題19: 意味と代入の可換性

定理20: 健全性

項モデル

定理21: 完全性

定義22: 項モデル

補題23: 項モデルの性質

完全性の証明

補題24: 完全性定理の補題

定理21: 完全性（再掲）

おわりに

参考文献

Discussion

定義9: $\Sigma$ -等式 ( $\Sigma$ -equation)

例： $\Sigma$ -等式

定義11: $\Sigma$ -領域

定義12: $\Sigma$ -項の表示

例： $\Sigma$ -項の表示

定義14: $\Sigma, F$ -項の表示

定義15: $\langle\Sigma|E\rangle$ -領域モデル
