はじめに
はじめまして。記事を開いていただきありがとうございます。
この記事はプログラム意味論の古典的かつ標準的な教科書『The Formal Semantics of Programming Languages An Introduction』(Winskel, 1993)の9章(Recursion equations)の内容をもう少し一般的な形で分かりやすく書き直した内容となっております。
(cf. https://www.cin.ufpe.br/~if721/intranet/TheFormalSemanticsofProgrammingLanguages.pdf)
具体的には、RECという再帰的関数定義を持つ一階の関数型言語の操作的意味論及び表示的意味論を等式理論風のアプローチにより取り扱います。
本質的に新しい内容は含まれておりませんが、この記事がプログラム意味論初学者の方に何か新しい気づきを与えることができれば幸いに思います。
よろしくお願いします。
前提知識
プログラム意味論とは
プログラム意味論とは、単なる記号列である「プログラム」に「計算」によって不変な「値」を割り当てる様々な手法、及び各手法同士の関係を数学的に調べる分野です。
"1+1"という文字列をコンピュータに渡すだけで、"1"を自然数の1、"+"を自然数の足し算だと解釈し計算して文字列"2"を出力するのはよく考えれば驚くべきことです。
プログラム意味論はその疑問を深掘りします。
有向完備半順序集合(dcpo)
プログラム意味論において中心となる数学的構造である有向完備半順序集合(以下dcpoと呼ぶ)について駆け足で説明します。
詳しいお気持ちについては以下の記事をご参照ください。
https://zenn.dev/mineel5/articles/d6bc627587b72b
定義1: 有向集合
poset Pに対し、\emptyset\not=X\subseteq{P}が有向集合\Leftrightarrow \forall x, y\in{X}, \exists{z}\in{X}, x\leq{z}\ \&\ y\leq{z}
有向集合は列の一般化となっており、添字集合に有向性が課されている場面も目にします。
一般にposetにおいて有向集合に上限が存在するとは限りませんが、全ての有向集合が上限を持ち、かつ最小元も存在するときdcpoと呼びます。
定義2: dcpo
全ての有向集合が上限を持ち、最小元を持つposetをdcpoという
また、dcpo間の連続関数も重要な登場人物です。
定義3: 連続関数
dcpo D, Eに対し、f: D\rightarrow{E}が連続\Leftrightarrow \forall{A}\subseteq{D}: 有向, f(A)は有向でf(\sqcup{A})=\sqcup{f}(A)
連続関数は(部分関数空間等の)代数的dcpoとよばれる領域においては有限呼び出し性という性質を持つ重要な関数です。
連続関数は必ず単調関数となりますが、逆は常に成り立つとは限りません。
しかし、次のことは言えます。
命題4: 単調関数が連続となる条件
dcpo D, D'に対し、Dが狭義無限増加列を持たないとき、単調関数f:D\rightarrow{D'}は必ず連続である
(\omega-cpoの場合は明らかだが、dcpoの場合は証明に一工夫必要)
例として、平坦領域(flat cpo)について考えます。
例5: 平坦領域
集合Xに対し、dcpo X_\bot=(X_\bot, \leq)を平坦領域という
ただし、
- X_\bot=X\cup\{\bot\}\ (where\ \bot\not\in{X})
- x\leq{y}\Leftrightarrow(x=\bot)\ or\ (x=y)
そのとき、平坦領域の有限直積(各点順序)は狭義無限増加列を持たないため、平坦領域の有限直積上の単調関数は必ず連続となる
言語REC
RECの構文
まず、今回扱うプログラミング言語RECを定義していきます。
変数記号の集合をV=\{\operatorname{x}_i\}_{i\in\mathbb{N}}とします。
関数記号は、言語にはじめから備わっている\Sigma=\{\operatorname{O}^0,\operatorname{S}^1\}及び特別な関数記号\bot^0に加え、ユーザ定義関数の有限集合F=\{\operatorname{f}_i^{a_i}\}_{i\leq{m}}が与えられ、ここからその上の項を定義していきます。
関数記号の肩の自然数はアリティと呼ばれ、その関数記号の「引数」の数を表します。
以降では、アリティは適宜省略します。
集合Aの有限列全体の集合をA^*を書き、列a, bが等しいことをa\equiv{b}と書きます。
また、変数記号を表すメタ変数をx, y,...またはx_0, x_1, ...、\Sigmaの関数記号を表すメタ変数を\sigma、Fの関数記号を表すメタ変数をfと書くとします。
定義6: T
集合T\subseteq(\{\bot\}\cup{V}\cup\Sigma\cup{F})^*を次を満たす最小の集合として定義する
- \bot\in{T}
- \forall{x}\in{V},\ x\in{T}
- \forall{\sigma^a}\in\Sigma,\ \forall t_1,...,t_a\in{T},\ \sigma t_1...t_a\in{T}
- \forall{f^a}\in{F},\ \forall t_1,...,t_a\in{T},\ ft_1...t_a\in{T}
以降は適宜括弧を補ってf(t_1,...,t_a)などと書くこととします。
直感的には\operatorname{O}が自然数の0を表し、\operatorname{S}が+1をする演算に対応します。
例えば、\operatorname{S(S(O))}は直感的には0+1+1、すなわち2を表します。
また、各関数記号fはユーザが定義できる関数を表しており、例えば足し算を表す\operatorname{add}が定義できれば、\operatorname{add(S(O), S(O))}は直感的には1+1、すなわち2を表すこととなります。
続いて、自由変数の集合\operatorname{FV}(t)を帰納的に定義します。
定義7: 自由変数の集合
各t\in{T}に対し、\operatorname{FV}(t)\subseteq{V}を次で定義する
-
t\equiv\botのとき
\operatorname{FV}(t)=\emptyset
-
t\equiv{x}のとき
\operatorname{FV}(t)=\{x\}
-
t\equiv{\sigma^a}(t_1,...,t_a)のとき
\operatorname{FV}(t)=\operatorname{FV}(t_1)\cup...\cup\operatorname{FV}(t_a)
-
t\equiv{f^a}(t_1,...,t_a)のとき
\operatorname{FV}(t)=\operatorname{FV}(t_1)\cup...\cup\operatorname{FV}(t_a)
そこで、Tを変数の有限集合\Gamma\in\mathcal{P}_{fin}(V)で添字付けし、項を定義します。
定義8: 項
\Gamma\in\mathcal{P}_{fin}(V)に対し、T_\Gamma\subseteq{T}を次で定義する
T_\Gamma=\{t\in{T}\ |\ \operatorname{FV}(t)\subseteq\Gamma\}
そこで、添字\Gammaを動かして直和を取ることで項の集合T_{REC}を次で定義する
T_{REC}=\coprod_{\Gamma\in\mathcal{P}_{fin}(V)}T_\Gamma
ただし、\coprodは集合の直和を表し、
\coprod_{\Gamma\in\mathcal{P}_{fin}(V)}T_\Gamma=\{(\Gamma, t)\in\mathcal{P}_{fin}(V)\times{T}\ |\ \operatorname{FV}(t)\subseteq\Gamma\}
(\Gamma, t)\in\mathcal{P}_{fin}(V)\times{T}が項のとき\Gamma\triangleright{t}と書き、また記法を濫用して\Gamma\triangleright{t}で項(\Gamma, t)を表すこととします。
そのとき、\Gammaのことを文脈(or環境)といい、また\Gamma=\emptysetの項を閉項といいます。
項\Gamma\triangleright{t}はtが何変数の式であるかの情報も含めた式を表します。
\operatorname{add}(\operatorname{x}_0, \operatorname{x}_1)は文脈次第で2変数の式とも見れますし、出現してないだけで3変数の式ともみなせます。
前者の見方の場合は\operatorname{x}_0, \operatorname{x}_1\triangleright\operatorname{add}(\operatorname{x}_0, \operatorname{x}_1)となり、後者の見方の場合は(例えば)\operatorname{x}_0, \operatorname{x}_1, \operatorname{x}_2\triangleright\operatorname{add}(\operatorname{x}_0, \operatorname{x}_1)となるわけです。
続いて、関数定義の定義をします。
定義9: 関数定義
次で定義される集合D_{fun}\subseteq\mathcal{P}_{fin}(V)\times{F}\times{T}の元を関数定義(or関数宣言)という
D_{fun}=\{(\Gamma, f, t)\ |\ |\Gamma|=\operatorname{ar}(f), t\in{T}_\Gamma\}
(\Gamma, f, t)\in{D_{fun}}のとき\Gamma\triangleright{f}(x_1, ..., x_a)=tと書くこととし、関数定義の\Gammaは以降では適宜省きます。
(ただし、\operatorname{ar}を関数記号のアリティを与える関数として、a=\operatorname{ar}(f)、\Gamma=\{x_1, ..., x_a\}とした。)
適当な関数定義の集合E\subseteq{D}_{fun}で各関数記号がちょうど一度ずつ現れるものを与えることで関数定義が可能となります。
そこで、Eにおいてfに対応する項をt^E_fと書くこととし、肩のEは適宜省略をします。
しかし、関数定義は相互再帰的定義となっており、その定義が意味するところの関数は決して明確ではありません。
例えば、次のような関数定義を(直感的に)満たす自然数上の関数は明らかに存在しません。
\operatorname{f}_0(\operatorname{x}_0)=\operatorname{S(f}_0(\operatorname{x}_0))
そのため、関数の再帰的定義を正確に扱うための枠組みが求められます。
そこで、領域理論が登場します。
ただその前に、関数の評価方法についての説明を行います。
値呼びと名前呼び
関数fは常に無限ループを返すとし、関数gは引数に関わらず常に0を返す定数関数だとします。
その時、g(f(3))は無限ループになるのでしょうか、それとも0を返すのでしょうか。
前者の評価方法、つまり関数合成の際には内側、つまり関数gに与えられる「値」を先に評価してから全体を評価する評価方法を値呼び(call-by-value)といいます。
逆に、後者の評価方法、つまり関数合成の際には外側、つまり関数gの「名前」を先に評価して引数に関わらず0を返す評価方法を名前呼び(call-by-name)といいます。
当然これは直感的な説明であり、厳密な形式化は実際に意味論を定義する際に現れます。
例として、f(x)=x+1、g(x)=x^2+xとすれば、g(f(2))の評価は
- 値呼び: g(f(2))\rightarrow g(3)\rightarrow 3^2+3\rightarrow 12
- 名前呼び: g(f(2))\rightarrow f(2)^2+f(2)\rightarrow f(2)^2+3\rightarrow 3^2+3\rightarrow 12
となります。
ここでは比較的扱いやすい名前呼び評価による意味論を与えていきたいと思います。
表示的意味論
プログラム意味論には大きく分けて表示的意味論、操作的意味論、公理的意味論の3種類の意味論が存在し、この記事では前半2つの意味論について扱っていきます。
まずは表示的意味論から扱います。
表示的意味論とは、各プログラムを自然数等の数学的対象に対応させて、プログラムの振る舞いを数学的に調べる意味論です。
例えば、"1+1"という文字列は適切な表示的意味論の下で自然数の2に対応付けされます。
ここでは、各項をdcpo上の関数に対応させることを考えます。
(次節でdcpoを用いる理由について解説を行います。)
定義10: \Sigma-領域
関数記号の集合\Sigma及びdcpoDに対し、(D, \llbracket\rrbracket)を\Sigma-領域という
ただし、各\sigma^a\in\Sigmaに対し、\llbracket\sigma\rrbracket:D^a\rightarrow{D}は連続関数
\llbracket\sigma\rrbracketを\sigmaの表示と言います。
そこで、ユーザ定義の関数記号f^a\in{F}に対しても、与えられた関数定義の集合E\subseteq{D}_{fun}における表示\llbracket{f}\rrbracket_E:D^a\rightarrow{D}を与えることを考えたいです。
しかし、決して簡単ではないので一旦\llbracket{f}\rrbracket_Eが定義されているものとして各項の表示\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}を考えていきます。
定義11: 項の表示
\Sigma-領域D=(D, \llbracket\rrbracket)に対し、\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}:D^{\Gamma}\rightarrow{D}を次で定義する
-
t\equiv\botのとき
\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}\rho=\bot_D
-
t\equiv{x}のとき
\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}\rho=\rho(x)
-
t\equiv{\sigma^a}(t_1,...,t_a)のとき
\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}\rho=\llbracket{\sigma}\rrbracket(\llbracket\Gamma\triangleright{t_1}\rrbracket^{D, E}\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket^{D, E}\rho)
-
t\equiv{f^a}(t_1,...,t_a)のとき
\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}\rho=\llbracket{f}\rrbracket_E(\llbracket\Gamma\triangleright{t_1}\rrbracket^{D, E}\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket^{D, E}\rho)
\rho\in{D}^{\Gamma}を環境といいます。
また、\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}の肩のD, Eは適宜省略します。
\llbracket\Gamma\triangleright{t}\rrbracket^{D, E}\rho=\llbracket\Gamma\triangleright{t'}\rrbracket^{D, E}\rhoのとき、D,\rho\vDash\Gamma\triangleright{t}=t'と書き、また以下の記法を用います。
- D\vDash\Gamma\triangleright{t}=t'\Leftrightarrow\forall\rho\in{D}^{\Gamma},\ D,\rho\vDash\Gamma\triangleright{t}=t'
- \vDash\Gamma\triangleright{t}=t'\Leftrightarrow\forall{D},\ D\vDash\Gamma\triangleright{t}=t'
また、\Gamma=\emptyset、すなわち閉項のときは省略して\vDash{t}=t'などと書きます。
不動点と再帰的定義
わざわざdcpoを意味領域に用いた理由について、ユーザ定義関数の意味付けを考えながら説明をしていきます。
まず、領域理論における最も重要な定理である連続関数の不動点定理を証明無しで紹介します。
定理12: 不動点定理
dcpo D, D'及び連続関数f:D\rightarrow{D'}に対し、Dの最小元を\bot_Dとすれば次が成り立つ
f(\operatorname{fix}f) = \operatorname{fix}f
ただし、\sqcupを上限を表す記号として
\operatorname{fix}f = \sqcup_{n\in\mathbb{N}}{f^n(\bot_D)}
(つまり、 \operatorname{fix}は最小不動点を与える関数)
任意の関数が不動点を持つというのは一見ありえないように思えますが、実際はf(x)=x+1など明らかに不動点を持たない関数は不動点が存在しないことを意味する最小元\bot_Dを不動点として持つというだけの話です。
しかし、\bot_Dを導入することにより不動点を滑らかに、かつ統一的に扱うことを可能にした点こそが領域理論の最大の成果だと考えております。
ところで、不動点は再帰的定義と深い関係があります。
例えば、階乗関数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}のEにおける表示\llbracket{f}\rrbracket_E:D^a\rightarrow{D}も(最小)不動点として必ず得られることになります。
ユーザ定義関数の意味付け
\llbracket\rrbracket_Eを最小不動点としてさくっと得ちゃいましょう。
\llbracket{f^a}\rrbracket_Eは関数定義\Gamma\triangleright{f}(x_1, ..., x_a)=t_fに対し、(直感的に)次を満たしていてほしいです。
\llbracket{f}\rrbracket_E(d_1,...,d_a)=\llbracket\Gamma\triangleright{t_f}\rrbracket\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}}という略記を用います。
しかし、\llbracket\rrbracket_Eを定義しようとしているのに上で定義した項の表示は\llbracket\rrbracket_Eに依存した定義になってしまっています。
そこで、一時的に項の表示に関数環境\varphi、すなわち各関数記号{f}^a\in{F}を\varphi(f):D^a\rightarrow{D}に対応させる関数も与えて\llbracket\Gamma\triangleright{t}\rrbracket\varphi\rhoという表示を考えることにします。
それに伴い、ユーザ定義関数記号の部分だけ以下のように定義が変更されます。
\llbracket\Gamma\triangleright{t}\rrbracket\varphi\rho=\varphi(f)(\llbracket\Gamma\triangleright{t_1}\rrbracket\varphi\rho, ...,\llbracket\Gamma\triangleright{t_a}\rrbracket\varphi\rho)
(つまり、最初に与えた意味論は、ここで与えた意味論において関数環境 \llbracket\rrbracket_Eがグローバルに与えられた意味論と言える。)
すると、\llbracket\rrbracket_Eは次の関数Fの最小不動点として得ることができます。
F(\varphi)(f)(d_1, ..., d_a)=\llbracket\Gamma\triangleright{t_f}\rrbracket\varphi\rho[d_i/x_i]_{i\leq{a}}
( Fが連続であることも確認する必要があるのですが、tの構造帰納法により示されます。)
(また、Fは\rhoに依らず定義されることも示す必要があります。)
操作的意味論
操作的意味論とは、プログラムの書き換え規則により形式的に推論される標準形という特殊な項をプログラムの意味とする意味論です。
一般に、操作的意味論にはbig step semantics(自然意味論)とsmall step semantics(構造意味論)の大きく2種類があります。
前者が最終的な評価値による意味論で、後者が"1ステップ"の評価による意味論となっており、ここでは前者の意味論を取り扱います。
まず、標準形を定義します。閉項の集合をT_{cl}\subseteq{T}_{REC}とします。
以下では、閉項\emptyset\triangleright{t}は単にtと書くこととします。
定義13: 標準形
次で定義される集合C_{REC}\subseteq{T}_{cl}の元を標準形(or値)という
C_{REC}=\{\operatorname{S}^n(\operatorname{O})\}_{n\in\mathbb{N}}
ただし、\operatorname{S}^n(\operatorname{O})\equiv\operatorname{S(S(...S(O)))} (\operatorname{S}がn個、ただし\operatorname{S}^0(\operatorname{O})\equiv\operatorname{O})とする
どの閉項もある自然数を表すなら「計算」をしたら何らかの標準形にたどり着くはずです。
そこで、関数定義集合Eに対し、閉項の計算規則(評価規則という)を次のように定めます。
定義14: 評価規則
\rightarrow^E\in{T}_{cl}\times{C}_{REC}を次を満たす最小の集合とする
\frac{t_i\rightarrow^Ec_i\ (1\le i\le a)}{\sigma(t_1, ..., t_a)\rightarrow^E\sigma(c_1, ..., c_a)}
\frac{t^E_f[t_1/x_1,...,t_a/x_a]\rightarrow^Ec}{f(t_1,...,t_a)\rightarrow^Ec}
ただし、t[t_1/x_1,...,t_a/x_a]はtに現れる各変数記号x_iをt_iに同時に置き換えた項を表す
(以降ではt[t_i/x_i]_{i\leq{a}}という略記を用いる)
これらは「上の規則が成り立つとき下の規則も成り立つ」という推論のルールを表しており、上の段が空欄のときは下の段が常に成り立つことを意味します。
また、最後の規則には名前呼び評価の特徴が現れています。
f(t_1,...,t_a)の評価の際には、各t_iを評価してからtに代入するのではなく、評価前のままのt_iを先に代入してから評価しています。
t\rightarrow^Ecのとき、\vdash{t}=cと書きます。
ここで定義した操作的意味論は決定的、つまり各閉項は高々1つの標準形を持つことが言えます。
命題15: 決定性
\forall{t}\in{T}_{cl},\ \forall{c, c'}\in{C}_{REC},\ t\rightarrow^Ec\ \&\ t\rightarrow^Ec'\Rightarrow{}c\equiv{c'}
意味論の等価性
意味論の等価性とは
勝手に言語RECを2種類の方法で意味付けしましたが、出来ればこれらが等価になっていてほしいです。
すなわち、次が成り立っていてほしいです。
定理16: 意味論の等価性
\forall{t}\in{T}_{cl},\ \forall{c}\in{C}_{REC},\ \vdash{t}=c\Leftrightarrow\ \vDash{t}=c
\Rightarrowを健全性、\Leftarrowを完全性と呼びます。
定理と書いてしまいましたが、これが実際に成り立つことをこれから示していきます。
ただ、健全性の方はtの構造帰納法を用いた所謂"やるだけ"の証明で面白みがないため省略をし、次章以降で完全性を証明します。
項モデル
次の完全性を証明します。
定理17: 完全性
\forall{t}\in{T}_{cl},\ \forall{c}\in{C}_{REC},\ \vDash{t}=c\Rightarrow\ \vdash{t}=c
完全性の証明は往々にして似たような証明になるのですが、ここでは項モデルを用いた証明を与えます。
項モデルとは、項の表示として項そのものを用いるモデルのことです。
そのため項モデルによる意味論は本当の意味で表示的意味論を構築できたとはとても言えず、「構文的な意味論」だと揶揄(?)されます。
しかし、項モデルは完全性を示す際にはとても有用なモデルとなります。
今、項はそのままだと「多すぎる」ため、適切な同値関係で閉項全体T_{cl}を割ることによって適切なモデルを得ることができます。
表示的意味論は「計算」によって不変な意味を与える枠組みでした。
そのため、項モデルにおいては操作的意味論上で等しいとされる項全体をひとまとめにするような同値関係を定めればよさそうです。
定義18: 閉項上の同値関係
関係\sim\subseteq{T}_{cl}\times{T}_{cl}を次で定める
t\sim{t'}\Leftrightarrow(\exists{c}\in{C}_{REC},\ t\rightarrow{c}\ \&\ t'\rightarrow{c})\ or\ (\forall{c}\in{C}_{REC},\ t\not\rightarrow{c}\ \&\ t'\not\rightarrow{c})
つまり、「同じ標準形を持つ」か「共に標準形を持たない」ときにt\sim{t'}となります。
評価の決定性より関係\simは同値関係となり、次の項モデルが得られます。
定義19: 項モデル
\Sigma-領域TM=(T_{cl}/\mathord{\sim}, \llbracket\rrbracket)を項モデルという
ただし、\sigma^a\in\Sigmaに対し、\llbracket\sigma\rrbracket:(T_{cl}/\mathord{\sim})^a\rightarrow T_{cl}/\mathord{\sim}を次で定義する(well-defined)
\llbracket\sigma\rrbracket([t_1], ..., [t_a]) = [\sigma(t_1, ..., t_a)]
(ただし、 [t]で閉項tの同値類を表す)
また、T_{cl}/\mathord{\sim}は同値類[\bot]を最小元に持つ平坦領域とみなす
\llbracket\sigma\rrbracketの連続性を示すには命題4より単調性を言えばよいですが、素直に与えられた操作的意味論に従って示せばよいです。
そこで、項モデルTMを用いて完全性の証明を行います。
完全性の証明
今、\llbracket\rrbracket_Eの定義及び不動点定理より、\llbracket\rrbracket_E=\sqcup_{n\in\mathbb{N}}F^n(\bot)でした。
(ただし、F(\varphi)(f)(d_1, ..., d_a)=\llbracket\Gamma\triangleright{t_f}\rrbracket\varphi\rho[d_i/x_i]_{i\leq{a}})
そこで、\delta^{(r)}=F^r(\bot)、すなわち\llbracket\rrbracket_Eのr番目の近似とします。つまり、
\delta^{(r)}(f^a)(d_1, ..., d_a) =
\left\{
\begin{array}{ll}
\bot & if\ r=0 \\
\llbracket\Gamma\triangleright{t_f}\rrbracket\delta^{(r-1)}\rho[d_i/x_i]_{i\leq{a}} & otherwise
\end{array}
\right.
とします。
そこで、完全性をより強くした以下の主張を、rの帰納法により示します。
補題20:
\forall{r}\in\mathbb{N},\ \forall{\Gamma\triangleright{t}}\in{T_{REC}},\ \forall{c}\in{C}_{REC},\ \forall{s}\geq|\Gamma|,\ \forall{u_1, ..., u_s}\in{T}_{cl},\ \forall{y_1, ..., y_s}\in{V}\ (s.t.\ \Gamma\subseteq\{y_i\}_{i\leq{s}})
\llbracket\Gamma\triangleright{t}\rrbracket^{TM}\delta^{(r)}\rho[[u_i]/y_i]_{i\leq{s}}=\llbracket{c}\rrbracket^{TM}\Rightarrow t[u_i/y_i]_{i\leq{s}}\rightarrow{c}
( cには変数記号もユーザ定義関数記号も出現しないため、関数環境及び環境は省略)
Proof:
示すべき命題は以下と同値なため、次をrの帰納法により示す。
(平坦領域Dにおいて、x\leq{y}\Leftrightarrow{x}=\bot_D\ or\ x=yに注意)
\llbracket\Gamma\triangleright{t}\rrbracket^{TM}\delta^{(r)}\rho[[u_i]/y_i]_{i\leq{s}}\leq[t[u_i/y_i]_{i\leq{s}}]
以下\rho'=\rho[[u_i]/y_i]_{i\leq{s}}、t'\equiv t[u_i/y_i]_{i\leq{s}}などとし、\llbracket\Gamma\triangleright{t}\rrbracket\delta^{(r)}\rho'\leq[t']を示す。
-
r=0のとき
tの構造帰納法により示す。
\begin{array}{lll}
\llbracket\Gamma\triangleright{t}\rrbracket\bot\rho' & = & [u_i] \\
& = & [t']
\end{array}
-
t\equiv\sigma^a(t_1, ..., t_a)のとき (\sigma\in\Sigma)
\begin{array}{llll}
\llbracket\Gamma\triangleright{t}\rrbracket\bot\rho' & = & \llbracket\sigma\rrbracket(\llbracket\Gamma\triangleright{t_1}\rrbracket\bot\rho', ..., \llbracket\Gamma\triangleright{t_a}\rrbracket\bot\rho') & \\
& \leq & \llbracket\sigma\rrbracket([t_1'], ..., [t_a']) & (\because IH\ \&\ \llbracket\sigma\rrbracket:単調) \\
& = & [\sigma(t_1, ..., t_a)] & (\because \llbracket\sigma\rrbracketのdef) \\
& = & [t'] &
\end{array}
-
t\equiv f^a(t_1, ..., t_a)のとき (f\in{F})
\delta^{(0)}(f)=\botなため、\llbracket\Gamma\triangleright{t}\rrbracket\bot\rho'=[\bot]より成立
-
r > 0のとき
tの構造帰納法により示す。
t\equiv\bot, y_i, \sigma^a(t_1, ..., t_a)のときは上と変わらないためt\equiv{f^a}(t_1, ..., t_a)のときのみ示す。
\newline
まず、構造帰納法の仮定より、各i\leq sで次が成り立つ。
\begin{equation}
\llbracket\Gamma\triangleright{t_i}\rrbracket\delta^{(r)}\rho'\leq[t'_i]
\end{equation}
\phantom{h }よって、\llbracket\Gamma\triangleright{t}_f\rrbracketの単調性 ((2)とする)より、
\begin{array}{llll}
\llbracket\Gamma\triangleright{t}\rrbracket\delta^{(r)}\rho' & = & \llbracket\Gamma\triangleright t_f\rrbracket\delta^{(r-1)}\rho'[\llbracket\Gamma\triangleright{t_i}\rrbracket\delta^{(r)}\rho'/x_i]_{i\leq{a}} & (\because \delta^{(r)}のdef) \\
& \leq & \llbracket\Gamma\triangleright t_f\rrbracket\delta^{(r-1)}\rho'[[t_i']/x_i]_{i\leq{a}} & (\because (1)\ \& \ (2))\\
& \leq & [t_f[t_i'/x_i]_{i\leq{a}}] & (\because rのIH) \\
& = & [f(t_1', ..., t_a')] & (\because t_fのdef) \\
& = & [t']
\end{array}
\square
完全性は上の補題でs=0とした系として得られます。
定理17: 完全性
\forall{t}\in{T}_{cl},\ \forall{c}\in{C}_{REC},\ \vDash{t}=c\Rightarrow\ \vdash{t}=c
Proof:
TM\vDash t=cより、\llbracket\rrbracket_E=\sqcup_{r\in\mathbb{N}}\delta^{(r)}に注意しながら補題20において\Gamma=\emptyset, s=0とすれば直ちに得られる。
\square
以上により、健全性及び完全性から意味論の等価性が示せました。
おわりに
お疲れ様でした。ここまで読んでいただきありがとうございました。
プログラム意味論というタイトルでしたが、やってることは等式理論における完全性定理の証明そのものです。
自然数は0個の等式及びアリティが0, 1の2つの関数記号により生成される代数のため、ここで与えた言語RECは自然数そのものです。
しかし、RECで面白いのは、プログラミング言語らしく自分で関数を定義できる機能がついているという点にあると思います。
これは通常の等式理論には存在しない概念であり、そのため再帰的定義を扱うために領域理論を用いて\Sigma-代数を\Sigma-領域に拡張するという試みを行ってみました。
ただ、ここでは完全性定理の証明の理解を目標としていたため、議論や定義の簡潔さのためプログラミング言語としては乏しすぎるほどの表現力を持つ言語について扱っておりました。
表現力を上げる、特にRECを\mathbb{N}_\botにおいて計算可能にするためには\Sigmaに\operatorname{O}, \operatorname{S}に加え-1をする関数\operatorname{pred}、if文、射影関数あたりを導入し、適当な等式を用意することにより解決できるのではないかと考えております。
(まだ、試していないため実際どうなるかは分かっておりません)
以上でこの記事は終わりとなります。
読みにくい部分も多々あったかと思われますが、少しでも面白いと思っていただけたら幸いです。
結構雰囲気で書いているため、数学的な間違いがございましたらここにご報告いただけると助かります。
また、正直たくさんの誤魔化しも存在しているため、気になる点や分からない点がありましたらご質問をいただければできるだけ対応いたします。
改めて本当にありがとうございました。お疲れ様でした。
Discussion