utlc/lambda の設計

設計目標

utlc/lambda は、共有レイヤーの上にできるだけ直接的に書かれた型なしλ計算である：名前付き項は syntax から、捕獲回避代入は substitution から、戦略は eval から得る。速さよりも明らかに正しいことを目指しており、より高速な正規化器（debruijn、utlc/nbe）や型付き計算 stlc をこれに照らして検査できるようにしている。

数学的背景

λ項は $t ::= v \mid x \mid t\,u \mid \lambda x.\,t$ であり、それぞれ Value、Variable、Apply(t, [u])、Bind(x, t) として符号化される。n 項の Apply(f, [a_1, …, a_n]) はカリー化されたスパイン $f\,a_1 \cdots a_n$ を表す。項は $=_\alpha$ を法として扱う。

β と η

\begin{aligned} (\beta)\quad & (\lambda x.\,b)\,a \;\to\; b[x := a], \\ (\eta)\quad & \lambda x.\,f\,x \;\to\; f \qquad \text{if } x \notin \mathrm{FV}(f). \end{aligned}

どちらも $\lambda$ の下（ $\xi$ 規則）を含むすべての文脈について閉じている。η の付帯条件は本質的である：これがないと $\lambda x.\,x\,x \to x$ によって閉じた項が開いた項になり、振る舞いの異なる関数が同一視されてしまう。η は外延性を表す： $\beta$ のもとでは、これは規則「新しい $x$ について $f\,x = g\,x$ ならば $f = g$ 」と同値である。なぜなら

f \;\leftarrow_\eta\; \lambda x.\,f\,x \;=\; \lambda x.\,g\,x \;\to_\eta\; g \qquad (x \notin \mathrm{FV}(f) \cup \mathrm{FV}(g)).

古典的な性質

合流性。 $\to_\beta$ と $\to_{\beta\eta}$ は Church–Rosser 性を持つので、項は $=_\alpha$ を除いて高々 1 つの正規形を持つ。¹1 Barendregt『The Lambda Calculus』定理 3.2.8 および 3.3.9。
正規化。 項が β 正規形を持つならば、最左最外戦略はそれに到達する（正規化定理、eval の設計を参照）。
η の後回し。 すべての $\beta\eta$ 簡約は、すべての $\beta$ ステップがすべての $\eta$ ステップより前に来るよう並べ替えられる。したがって、項が $\beta\eta$ 正規形を持つのは $\beta$ 正規形を持つときかつそのときに限る。²2 Barendregt『The Lambda Calculus』§15.1。
決定不能性。 項が正規形を持つかどうかは決定不能であり、そのため正規化器はステップ数の上限を受け取る。

設計上の決定

共有の代入による β

beta_rule は Substitution::singleton(x, a).apply(b) を呼ぶ。したがって捕獲回避はすべて 1 か所にまとまっており、substitution の設計で一度だけ証明されている。簡約基 $(\lambda x.\,\lambda y.\,x\,y)\,y$ について：

\begin{aligned} (\lambda x.\,\lambda y.\,x\,y)\,y &\to_\beta (\lambda y.\,x\,y)[x := y] \\ &= \lambda y_1.\,(x\,y_1)[x := y] && y \in \mathrm{FV}(\text{replacement}),\ \text{rename } y \\ &= \lambda y_1.\,y\,y_1 \\ &\to_\eta y . \end{aligned}

代入補題（Barendregt 2.1.16、substitution の設計で導出）により、β は α 同値類の上で well-defined となり、文脈と両立する。

スパインは引数 1 つずつ縮約される

簡約基は Apply(Bind(x, b), [a, ..rest]) である。最初の引数とだけ縮約し、残りは保つ： $(\lambda x.\,b)\,a\,\bar r \to b[x := a]\,\bar r$ 。これはスパインのカリー化された読みにおける β なので、各ステップは単一の β ステップであり、ステップ数は対応するカリー化された簡約の長さに等しい。De Bruijn 簡約器も同じ選択をしており、両者をステップごとに比較できるようにしている。

η は単項適用のみ

eta_rule は Bind(x, Apply(f, [Variable(x)])) にマッチする。カリー化された読みでは $\lambda x.\,f\,a\,x$ （Apply(f, [a, x]) と書かれる）も η 簡約基であるが、それを認識するにはスパインを分割して Apply(f, [a]) を再構築する必要がある。規則は構文的なままにしてある。n 項のスパインを作りつつ η を必要とする呼び出し側は、まずスパインを単項形式に正規化すればよい。

1 つの組み合わせ規則による正規順序

normalize は beta_eta_rule を NormalOrder 戦略で実行するので、各ステップはどちらかの種類の最左最外の簡約基を縮約する。組み合わせ規則の名前は "beta_eta" の 1 つだけであり、トレースは位置を示すが、2 つの規則のどちらが発火したかは示さない。β 簡約基と η 簡約基は根のコンストラクタが異なるため、beta_eta_rule 内部の優先順位がステップの結果を変えることはない。

正しさ / 不変条件

beta_rule(t) = Some(u) は根において $t \to_\beta u$ であることを含意する。eta_rule も $\eta$ について同様であり、付帯条件は @syntax.free_variables によって検査される。
normalize が NormalForm(u, n) を返すのは、どこにも（単項の） $\beta$ 簡約基も $\eta$ 簡約基もない $u$ に対してのみである（rewrite の正規形補題）。
合流性により、同じ項に対する本パッケージ、debruijn（β のみ）、utlc/nbe（β のみ）の停止する任意の 2 つの実行は、変換とスパインの平坦化の後に α同値となる β 正規形を与える。テスト “named and debruijn beta reduction agree modulo alpha” はリネームを必要とするステップを検査する。
β と η を組み合わせる場合、戦略として正規順序を用いる。それが正規化可能なすべての項の $\beta\eta$ 正規形に到達することは、β の正規化定理と η の後回しに基づいており、ここでは証明せずテストで検査している。

却下した代替案

独立したλ AST。 Term[T] を使うことで計算体系を共有基盤の内側に保てる：同じ解析、代入、トレースが適用でき、ドメインの値もそのまま運ばれる。
β と η の別々の正規化器。 間接的に提供されている：beta_rule または eta_rule を任意の戦略とともに @eval.evaluate に渡せばよい。
β における反復代入。 β は一度だけ代入する。計算体系が要求するとおり、引数が再び代入されることはない。

境界

型はない： $\Omega$ のような振る舞いの悪い項も受け付けられ、StepLimitReached で終わる。
共有はない：複製された引数はコピーごとに 1 回ずつ簡約される。効率的な正規化には utlc/nbe を使うこと。
η は単項適用のみを認識する。
定数（Value）にはここでは簡約規則がない。ドメイン規則は rewrite または eval で追加すること。

Barendregt『The Lambda Calculus』定理 3.2.8 および 3.3.9。 ↩
Barendregt『The Lambda Calculus』§15.1。 ↩