【ラムダ計算】停止しない計算は無意味なのか？（Böhm木、 D∞）【part1】

本記事ではラムダ計算と領域理論の基礎の知識を仮定しています。
私の方でも紹介記事を書いておりますので、もし興味があればぜひお読み下さい！

• ラムダ計算：https://zenn.dev/mineel5/articles/lambdalambdalambda
• 領域理論：https://zenn.dev/mineel5/articles/d6bc627587b72b

はじめに

はじめまして。記事を開いていただきありがとうございます。

我々は普段、計算したら同じ値になるものは同一視しています。
例えば、$3+53+5$と$2+(3+3)2+(3+3)$は共に$88$に評価されるため、通常は$3+5=2+(3+3)3+5=2+(3+3)$と考えられます。

このような同一視をラムダ計算の文脈では$β\beta$-同値と呼ばれ、例えば$(λx.xy)z=β(λx.x)(zy)(\lambda x.xy)z=_\beta (\lambda x.x)(zy)$と考えられます。

しかし、型無しラムダ計算における「計算」、すなわち、$β\beta$-簡約は必ずしも止まるとは限りません。

例：止まらない$β\beta$-簡約

$$Ω≡(λx.xx)(λx.xx)→β(λx.xx)(λx.xx)→β… \Omega\equiv(\lambda x.xx)(\lambda x.xx)\to_\beta(\lambda x.xx)(\lambda x.xx)\to_\beta\dots$$

このような$β\beta$-同値による同一視のもとでは、止まらない計算はすべて計算結果を持たない無意味な計算として捉えられてしまいます。

しかし、本当に止まらない計算はすべて無意味な計算としてまとめてしまってもよいのでしょうか？

例えば、適当な不動点コンビネータ$YY$, $F≡λzxy.x(zy)F\equiv\lambda zxy.x(zy)$に対し、$J≡YFJ\equiv YF$と定義すると次のようになります。（ラムダ計算に不慣れな方は雰囲気で見てください。）

$$Jx0→βλx1.x0(Jx1)→βλx1.x0(λx2.x1(Jx2))→β⋯ 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. 変換を無限に続けた式の木構造

このとき、どの有限ステップで止めても$λx1.x0(λx2.x1(...(λxn+1.xnxn+1)...))\lambda x_1.x_0(\lambda x_2.x_1(...(\lambda x_{n+1}.x_nx_{n+1} )...))$というラムダ式になり、次の$η\eta$-変換を繰り返し適用することで$x0x_0$に評価されます。

$$λx.yx→ηy \lambda x.yx\to_\eta y$$

それならば、ラムダ式$Jx0Jx_0$も極限のその先で何らかの「計算」により$x0x_0$に評価されると考えることはできないのでしょうか？

この記事では、このようなラムダ計算の構文上での極限での振る舞いを捉える手法の一つとして、Böhm木を導入して説明を試みます。
また、極限での振る舞いを見事に数学的に捉えたScottモデル $D∞D_\infty$を導入し、Böhm木による構文的近似の正当性を$D∞D_\infty$の言葉で述べる近似定理を紹介します。
（あくまで$D∞D_\infty$の紹介が中心であり、あまり型無しラムダ計算の表示的意味論の詳しい紹介は行いません。）

よろしくお願いします。

知らないまま未知のものを構成する

ひとまずラムダ計算の話は置いておいて、我々が普段どのように既知のものから未知のものを構成しているかを思い出してみましょう。

学部一回生で習う実数の構成の話をします。

今、我々は有理数しか知らないとします。さて、次の数列は収束するでしょうか？

$$a0=1a1=1.4a2=1.41⋮an=2の小数第n位まで⋮ \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$-基 $(λx.M)N(\lambda x.M)N$を持たない、すなわち、これ以上$β\beta$-簡約ができないような式を$β\beta$-正規形と呼びます。
そこで、ラムダ式$MM$から適当な有限回の$β\beta$-簡約で$β\beta$-正規形が得られるとき、$MM$は（弱）正規化可能であるといいます。

型無しラムダ計算において、「正規化可能なラムダ式は必ず最左戦略で$β\beta$-正規形が得られる」という正規化定理が存在します。
つまり、何も考えずとりあえず一番左にある$β\beta$-基を順に変換していれば$β\beta$-正規形が得られるわけです。

その際、正規形が得られないパターンとして以下の2パターンがあります。

• 頭正規形 (head normal form; hnf)を持たない
• 頭正規形を無限回得る

---

定義1: 頭正規形

ラムダ式$M∈ΛM\in\Lambda$は必ず次のいずれかの形で書ける。 $(n,m∈N)(n, m\in\mathbb{N})$

• $λx1…xn.xM1…Mm\lambda x_1\dots x_n.xM_1\dots M_m$
• $λx1…xn.(λx.N)M0…Mm\lambda x_1\dots x_n.(\lambda x.N)M_0\dots M_m$

前者のラムダ式を頭正規形 (hnf)と呼ぶ。

---

例：頭正規形

• hnfな例
  • $xx$
  • $x(xy)x(xy)$
  • $λxy.z\lambda xy.z$
  • $λx.(λy.x)\lambda x.(\lambda y.x)$ $(≡λxy.x)(\equiv\lambda xy.x)$
• hnfでない例
  • $(λx.y)z(\lambda x.y)z$
  • $λx.(λy.x)z\lambda x.(\lambda y.x)z$

hnfでないラムダ式は、必ず頭基$(λx.N)M0(\lambda x.N)M_0$を持ち、頭基は常に最も左にある$β\beta$-基になるため、最左戦略においては必ず優先的に簡約されます。
頭基を$β\beta$-簡約することを頭変換といいます。

頭変換を繰り返すと、いずれ頭基がなくなりhnfになるか、そもそも頭変換が一生終わらず$β\beta$-正規形にたどり着かない場合に分かれます。

もしhnf $λx1…xn.xM1…Mm\lambda x_1\dots x_n.xM_1\dots M_m$になったら、次は$M1M_1$の最左変換が始まるかもしれないため、hnfは$β\beta$-正規形とは限りません。
$M1M_1$がもしhnfを持たない場合は最左戦略が失敗したということになるため、元の$MM$が$β\beta$-正規形を持たなかったということになります。

しかし、$M1M_1$のhnf $λx1′…xn′.xM1′…Mm′\lambda x_1'\dots x_n'.xM_1'\dots M_m'$にたどり着いたとしても、次は$M1′M_1'$のhnfにたどり着いて、次は$M1′′M_1''$のhnfにたどり着いて、...を無限回繰り返す可能性があります。

このようにして、止まらない計算は改めて以下の2パターンに分かれることが分かります。

• hnfを持たない
• hnfを無限回得る

例：hnfを持たない例、無限回得る例

• hfnを持たない例
  • $Ω≡(λx.xx)(λx.xx)\Omega\equiv(\lambda x.xx)(\lambda x.xx)$
• hnfを無限回得る例
  • $Y≡λy.XXY\equiv\lambda y.XX$ where $X≡λx.y(xx)X\equiv\lambda x.y(xx)$

後者の例は、$XX→βy(XX)XX\to_\beta y(XX)$に注意すると、$Y→βλy.y(XX)→βλy.y(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}$を次を満たす最小の集合として定める。^[1]
（部分式の簡約規則は$\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{}{\bot\le M}$$

$$\frac{}{x\le x}$$

$$\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

今回はこの思想を採用して、有向集合こそ「収束しそうな列・集合」とみなすことにします。

改めてまとめると、有向集合かつ下方集合であるような集合（イデアル^[2]と呼ぶ）を「収束しそうな列・集合」とみなすことにし、イデアルそのものを（既知の世界では存在しないかもしれない）収束先と同一視します。

---

定義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$の関係の一部について見てみることとします。

改めて、本当にありがとうございました。

脚注

1. 下二つの規則は、$\bot$が$\Omega$に置き換えたラムダ式を最左戦略により簡約している状況を想定した規則です。そのため名前呼びになっています。

2. 束論ではイデアルの定義に有向性の代わりに$\forall a, b\in L, a\vee b\in L$という条件が課されることが多いですが、束においては有向性と同値な条件です。有向性の方が上限を用いない一般的な定義ですので、有向性を用いるようにしましょう。