はじめに
はじめまして。記事を開いていただきありがとうございます。
我々は普段、計算したら同じ値になるものは同一視しています。
例えば、3+5と2+(3+3)は共に8に評価されるため、通常は3+5=2+(3+3)と考えられます。
このような同一視をラムダ計算の文脈では\beta-同値と呼ばれ、例えば(\lambda x.xy)z=_\beta (\lambda x.x)(zy)と考えられます。
しかし、型無しラムダ計算における「計算」、すなわち、\beta-簡約は必ずしも止まるとは限りません。
例:止まらない\beta-簡約
\Omega\equiv(\lambda x.xx)(\lambda x.xx)\to_\beta(\lambda x.xx)(\lambda x.xx)\to_\beta\dots
このような\beta-同値による同一視のもとでは、止まらない計算はすべて計算結果を持たない無意味な計算として捉えられてしまいます。
しかし、本当に止まらない計算はすべて無意味な計算としてまとめてしまってもよいのでしょうか?
例えば、適当な不動点コンビネータY, F\equiv\lambda zxy.x(zy)に対し、J\equiv YFと定義すると次のようになります。(ラムダ計算に不慣れな方は雰囲気で見てください。)
Jx_0\to_\beta\lambda x_1.x_0(Jx_1)\to_\beta\lambda x_1.x_0(\lambda x_2.x_1(Jx_2))\to_\beta\cdots
図1. 変換を無限に続けた式の木構造
このとき、どの有限ステップで止めても\lambda x_1.x_0(\lambda x_2.x_1(...(\lambda x_{n+1}.x_nx_{n+1} )...))というラムダ式になり、次の\eta-変換を繰り返し適用することでx_0に評価されます。
それならば、ラムダ式Jx_0も極限のその先で何らかの「計算」によりx_0に評価されると考えることはできないのでしょうか?
この記事では、このようなラムダ計算の構文上での極限での振る舞いを捉える手法の一つとして、Böhm木を導入して説明を試みます。
また、極限での振る舞いを見事に数学的に捉えたScottモデル D_\inftyを導入し、Böhm木による構文的近似の正当性をD_\inftyの言葉で述べる近似定理を紹介します。
(あくまでD_\inftyの紹介が中心であり、あまり型無しラムダ計算の表示的意味論の詳しい紹介は行いません。)
よろしくお願いします。
知らないまま未知のものを構成する
ひとまずラムダ計算の話は置いておいて、我々が普段どのように既知のものから未知のものを構成しているかを思い出してみましょう。
学部一回生で習う実数の構成の話をします。
今、我々は有理数しか知らないとします。さて、次の数列は収束するでしょうか?
\begin{array}{lcl}
a_0 & = & 1 \\
a_1 & = & 1.4 \\
a_2 & = & 1.41 \\
& \vdots & \\
a_n & = & \sqrt 2\text{の小数第}n\text{位まで} \\
& \vdots &
\end{array}
もちろん収束しません。しませんが、なんか収束しそうで悔しいです。
我々は有理数が全てだと思い込んでいましたが、もしかしたら我々の知らない「何か」が有理数には欠けていたのかもしれません。
しかし、その「何か」を知る手段はありません。
そこで、構成したいものを知らないまま構成する手法として列や集合そのものを数としてみるという手法が頻繁に用いられ、このように欠けた「何か」を埋めることを一般に完備化といいます。
Cauchy完備化では、「何か」に収束しそうな列のことをCauchy列と呼び、同じ「何か」に収束するものをまとめた同値類を実数と呼んでいました。
デデキント切断では、上限(極限)を取ることで「何か」収束するような集合を切断と呼び、同じ「何か」に収束するものをまとめるために(最大値を持たない)下方集合のみを考えることにより一意性を保証した切断を実数と呼んでいました。
特に、半順序集合において下方集合は順序イデアルと呼ばれることがあり、デデキント切断による実数の構成はほとんどイデアル完備化と呼ばれる手法に当たります。
すると、ラムダ計算においても、止まらない計算ももしかすると我々の知らない「何か」に収束しているだけかもしれません。
そこで、イデアル完備化により通常のラムダ式に欠けた「何か」を埋めたラムダ式がBöhm木と呼ばれるものの正体になります。
先程は(無限)列や(無限)集合により欠けた穴を埋めていましたが、ラムダ計算では(無限)木によって穴を埋めることになるわけです。
Böhm木の導入
頭正規形
\beta-基 (\lambda x.M)Nを持たない、すなわち、これ以上\beta-簡約ができないような式を\beta-正規形と呼びます。
そこで、ラムダ式Mから適当な有限回の\beta-簡約で\beta-正規形が得られるとき、Mは(弱)正規化可能であるといいます。
型無しラムダ計算において、「正規化可能なラムダ式は必ず最左戦略で\beta-正規形が得られる」という正規化定理が存在します。
つまり、何も考えずとりあえず一番左にある\beta-基を順に変換していれば\beta-正規形が得られるわけです。
その際、正規形が得られないパターンとして以下の2パターンがあります。
- 頭正規形 (head normal form; hnf)を持たない
- 頭正規形を無限回得る
定義1: 頭正規形
ラムダ式M\in\Lambdaは必ず次のいずれかの形で書ける。 (n, m\in\mathbb{N})
- \lambda x_1\dots x_n.xM_1\dots M_m
- \lambda x_1\dots x_n.(\lambda x.N)M_0\dots M_m
前者のラムダ式を頭正規形 (hnf)と呼ぶ。
例:頭正規形
- hnfな例
- x
- x(xy)
- \lambda xy.z
-
\lambda x.(\lambda y.x) (\equiv\lambda xy.x)
- hnfでない例
- (\lambda x.y)z
- \lambda x.(\lambda y.x)z
hnfでないラムダ式は、必ず頭基(\lambda x.N)M_0を持ち、頭基は常に最も左にある\beta-基になるため、最左戦略においては必ず優先的に簡約されます。
頭基を\beta-簡約することを頭変換といいます。
頭変換を繰り返すと、いずれ頭基がなくなりhnfになるか、そもそも頭変換が一生終わらず\beta-正規形にたどり着かない場合に分かれます。
もしhnf \lambda x_1\dots x_n.xM_1\dots M_mになったら、次はM_1の最左変換が始まるかもしれないため、hnfは\beta-正規形とは限りません。
M_1がもしhnfを持たない場合は最左戦略が失敗したということになるため、元のMが\beta-正規形を持たなかったということになります。
しかし、M_1のhnf \lambda x_1'\dots x_n'.xM_1'\dots M_m'にたどり着いたとしても、次はM_1'のhnfにたどり着いて、次はM_1''のhnfにたどり着いて、...を無限回繰り返す可能性があります。
このようにして、止まらない計算は改めて以下の2パターンに分かれることが分かります。
例:hnfを持たない例、無限回得る例
- hfnを持たない例
- \Omega\equiv(\lambda x.xx)(\lambda x.xx)
- hnfを無限回得る例
-
Y\equiv\lambda y.XX where X\equiv\lambda x.y(xx)
後者の例は、XX\to_\beta y(XX)に注意すると、Y\to_\beta\lambda y.y(XX)\to_\beta\lambda y.y(y(XX))\to_\beta\cdotsに注意してください。
そこで、hnfを持たないラムダ式を不定式と呼び、本当に意味を持たない計算として考えることにします。
しかし、\beta-正規形を持たない後者のパターンは、極限での振る舞いに個性がありそうで興味があります。
部分ラムダ式と近似
極限での振る舞いを近似により捉えます。そこで、ラムダ式の近似という概念を導入するために、部分ラムダ式の集合\Lambda_\botを導入します。
定義2: 部分ラムダ式
次のBNF記法で定義される集合をそれぞれV, \Lambda_\botとし、\Lambda_\botの元を部分ラムダ式と呼ぶ。
\begin{array}{ll}
x ::= & \texttt{v}\mid x' \\
e ::= & \bot\mid x\mid (\lambda x.e)\mid (ee)
\end{array}
つまり、通常のラムダ式から0個以上の部分式を\botという記号に置き換えたものを部分ラムダ式と呼びます。
今、\botを\Omegaだと思うことで、部分ラムダ式は通常のラムダ式に埋め込むことができます。
つまり、部分ラムダ式は原則は通常のラムダ式と同様に扱うことができます。
また、部分ラムダ式に対する計算規則\beta\bot-簡約を次で定めます。
定義3: \beta\bot-簡約
部分ラムダ式上の二項関係\to_{\beta\bot}を次を満たす最小の集合として定める。
(部分式の簡約規則は\beta-簡約と同じなので省略。)
\frac{}{(\lambda x.M)N\to_{\beta\bot}M[N/x]}
\frac{}{\bot M\to_{\beta\bot}\bot}
\frac{}{\lambda x.\bot\to_{\beta\bot}\bot}
(\lambda x.M)N, \bot M, \lambda x.\botの形の部分ラムダ式を\beta\bot-基と呼び、\beta\bot-基を持たない部分ラムダ式を\beta\bot-正規形と呼びます。
さらに、部分ラムダ式に半順序を導入します。
定義4: 近似関係
部分ラムダ式同士の二項関係 \mathord\le\subseteq\Lambda_\bot\times\Lambda_\botを次を満たす最小の集合として定める。
\frac{M\le M'\quad N\le N'}{MN\le M'N'}
\frac{M\le M'}{\lambda x.M\le\lambda x.M'}
すなわち、部分ラムダ式Mが部分ラムダ式M'の部分式を0個以上\botに置き換えて得られるとき、M\le M'としました。
部分ラムダ式N, M\in\Lambda_\botがN\le Mのとき、NはMを近似するといいます。
例:近似関係
- \bot\le\lambda x.x(yz)
- \lambda x.\bot\le\lambda x.x(yz)
- \lambda x.x\bot\le\lambda x.x(yz)
- \lambda x.x(y\bot)\le\lambda x.x(yz)
- \lambda x.x(yz)\le\lambda x.x(yz)
\lambda x.x(yz)という部分ラムダ式が完全な情報を持っているのに対し、\lambda x.x\botではyzという情報が欠落しています。
つまり、\lambda x.x\botは\lambda x.x(yz)の近似であると見ることができます。
上記の例では、上から順に徐々に「正確な」近似になっていっています。
すなわち、\bot\le\lambda x.\bot\le\lambda x.x\bot\le\lambda x.x(y\bot)\le\lambda x.x(yz)となっています。
近似列による部分ラムダ式の表現
では、無限に移る前に、有限の部分ラムダ式で近似での表現に慣れる練習をしましょう。
完備化の話を思い出してください。
Cauchy完備化を行ったあとの実数では、有理数2はもはや元の姿ではなく、「2に収束する数列の集合」を2と見ていたのでした。
では、同様に部分ラムダ式\lambda x.x(yz)は「\lambda x.x(yz)に収束する近似列の集合」と見なせそうです。
集合と言いましたが、実際、\lambda x.x(yz)に収束する近似列は先程の例だけではありません。
例えば、\bot\le\lambda x.\bot\le\lambda x.\bot(yz)\le\lambda x.x(yz)も同じ部分ラムダ式に収束します。
また、\botから始めるなんてルールはありませんので、\lambda x.\bot(yz)\le\lambda x.x(yz)も同じ部分ラムダ式に収束する近似列となります。
そこで、Cauchy完備化のときと同様に同じ値に収束するものをまとめた同値類を考えてもよいのですが、半順序集合においてはもっと簡単なまとめ方があります。
それは、下方集合(順序イデアル)となる近似列のみを採用するという方針です。
つまり、\lambda x.x(yz)の近似列とは、\lambda x.x(yz)以下の部分ラムダ式全体の集合\{M\in\Lambda\mid M\le\lambda x.x(yz)\}であると定義します。
そうなると、各部分ラムダ式に対応する近似列が一意に定まるため少し楽になります。デデキント切断と同じ発想です。
そこで、これからは\lambda x.x(yz)の近似列\{M\in\Lambda\mid M\le\lambda x.x(yz)\}そのものをラムダ式\lambda x.x(yz)だと思いこむようにしましょう。
さて、では無限の話に移ります。有限の場合と違い、我々の既知の世界には収束先がないような近似列を扱うことになります。
例:収束しない近似列 (Y\equiv\lambda y.XX where X\equiv\lambda x.y(xx)の例)
\bot\le\lambda y.\bot\le\lambda y.y\bot\le\lambda y.y(y\bot)\le\lambda y.y(y(y\bot))\le\cdots
しかし、すべての近似列に対して収束先を与えるわけではありません。
実際、Cauchy完備化ではCauchy列と呼ばれる「収束しそうな列」にのみ収束先を与えています。
部分ラムダ式において、「収束しそうな列・集合」とは何でしょうか?
もちろん数学においては何をどのように定義してもよいため、これは数学的な問題というよりは思想の問題になります。
その一つの回答として、領域理論における「計算」の考え方があります。
領域理論においては、有向集合こそ(矛盾のない)「計算」過程の集合であるとみなし、「計算」はすべて収束してほしいという願いを込めて有向完備 (=すべての有向集合が上限を持つ)という条件をつけた半順序集合を考えます。
この辺の考え方はぜひ私の記事をお読みください。
https://zenn.dev/mineel5/articles/d6bc627587b72b
今回はこの思想を採用して、有向集合こそ「収束しそうな列・集合」とみなすことにします。
改めてまとめると、有向集合かつ下方集合であるような集合(イデアルと呼ぶ)を「収束しそうな列・集合」とみなすことにし、イデアルそのものを(既知の世界では存在しないかもしれない)収束先と同一視します。
定義5: イデアル完備化
poset Pに対し、P上のイデアルすべてを集め、包含関係で順序付けしたposet \mathrm{Idl}(P)をPのイデアル完備化という。(poset = 半順序集合)
posetのイデアル完備化は必ず代数的cpoと呼ばれる有向完備半順序集合 (cpo)となります。
Böhm木の定義
では、有理数に対して実数を定義するように、部分ラムダ式に対してBöhm木を定義します。
特に、「意味」のある部分ラムダ式のみを考えるために、hnfな部分ラムダ式のみを考えることにします。
定義6: Böhm木
hnfな部分ラムダ式の集合を\mathcal{N}\subseteq\Lambda_\botとし、近似関係によるposetとみなす。
そのとき、\mathcal{N}のイデアル完備化\mathrm{Idl}(\mathcal{N})の元をBöhm木と呼ぶ。
つまり、hnfな部分ラムダ式上のイデアルをBöhm木と呼びます。
とはいえ、もう少し直感的に捉えることもできます。
停止しない\beta-変換の構文上での極限での振る舞いを捉えるためにBöhm木を導入しましたが、別の考え方として、「無限の長さのラムダ式が計算結果だ」と言い張ってみることもできます。
つまり、Böhm木を無限の長さの式、すなわち、無限の高さの木と見なしてみます。
例:無限木としてのBöhm木
\bot\le\lambda y.\bot\le\lambda y.y\bot\le\lambda y.y(y\bot)\le\lambda y.y(y(y\bot))\le\cdotsという近似列の収束先のBöhm木を次の木と見なす。
図2. 無限木としてのBöhm木
通常のラムダ式Mに対して、Mを計算していった際の収束先となるBöhm木 \mathrm{BT}(M)を定義します。
特に、不定式(=意味のないラムダ式)は\botという(木で言えば)深さ1のBöhm木に収束することには注意してください。
定義7: ラムダ式が収束するBöhm木
通常のラムダ式M\in\Lambdaに対し、Böhm木 \mathrm{BT}(M)\in\mathrm{Idl}(\mathcal{N})を次で定義する。
\mathrm{BT}(M)=\mathop\downarrow\{\omega(N)\mid M\to_\beta^* N\}
ただし、\to_\beta^*は\to_\betaの反射推移閉包である。
また、現在の近似 \omega\colon\Lambda\to\mathcal{N}は次で定義。
\omega(M)=
\left\{
\begin{array}{ll}
\bot & \text{ if }M\text{ is not hnf} \\
\lambda x_1\dots x_n.x\omega(M_1)\dots\omega(M_m) & \text{ if }M\equiv\lambda x_1\dots x_n.xM_1\dots M_m
\end{array}
\right.
さらに、poset Pの部分集合 X\subseteq Pに対して、\mathop\downarrow Xは次で定義。
\mathop\downarrow{X}=\{y\in P\mid \exists x\in X, y\le x\}
\omega(M)は\mathrm{BT}(M)に向かう近似列における現在の近似を表します。
このとき、M\to_\beta Nならば\omega(M)\le\omega(N)が成り立ち、CR性と合わせて\{\omega(N)\mid M\to_\beta^* N\}の有向性は保証されます。
また、定義より\beta-同値なラムダ式は同じBöhm木を持ちます。
また、通常のラムダ式M, N\in\Lambdaに対し、Böhm木同値をM=_BN\iff\mathrm{BT}(M)=\mathrm{BT}(M)で定めます。
すると、定義より\forall M, N\in\Lambda, M=_\beta N\implies M=_BNが言えます。
つまり、Böhm木同値は\beta-同値性の一般化になっており、\beta-同値性では捉えきれなかった極限での振る舞いが等しい場合にも同一視する視点を得ることができました。
おわりに
お疲れ様でした。ここまで読んでいただきありがとうございました。
ひとまずBöhm木の定義が完了し、停止しない計算を捉える足がかりができました。
しかし、あくまでBöhm木は構文的な概念であり、完全性定理における項モデルを作成しただけみたいな状況なため、Böhm木が数学的にどのような対象であるのかはもう少し調査する必要があります。
そこで、次回では型無しラムダ計算における極限での振る舞いを見事に捉えた数学的構造 D_\inftyにおいてラムダ式が解釈できることを見て、D_\inftyの構造を調査してみます。
また、最後には近似定理の紹介をし、Böhm木とD_\inftyの関係の一部について見てみることとします。
改めて、本当にありがとうございました。
Discussion