utlc/nbe の設計

設計目標

スモールステップの正規化は、β ステップのたびに根から探索をやり直し、そのたびに項をコピーする。評価による正規化（NbE）はそうではなく、項をホスト言語の値として解釈し（そこでは β 簡約は単なる関数適用である）、その値を正規形として読み戻す。本パッケージは De Bruijn 項上の型なし計算に対する NbE を提供する：高速であるが、型なしの項は正規化するとは限らないため、燃料（fuel）によって制限される。操作的な簡約器が参照意味論であり続け、NbE はそれらに照らして検査される。

数学的背景

意味領域

値は次の文法で与えられる。ここで $\rho$ は環境（値のリストで、インデックス $0$ が先頭）、 $t$ は De Bruijn 項、 $x$ は自由な名前、 $\ell$ はレベルである：

\begin{aligned} d \in D \;&::=\; \mathsf{atom}(v) \;\mid\; \mathsf{clo}(t, \rho) \;\mid\; \mathsf{delay}(t, \rho) \;\mid\; n, \\ n \in \mathrm{Ne} \;&::=\; \mathsf{free}(x) \;\mid\; \mathsf{lvl}(\ell) \;\mid\; \mathsf{app}(d, d). \end{aligned}

$\mathsf{clo}(t, \rho)$ は $\rho$ における $\lambda.\,t$ の値であり、 $\mathsf{delay}(t, \rho)$ はまだ評価されていない引数であり、中立値 $n$ は変数で行き詰まった計算である。実装では、 $d$ が定数の場合にも $\mathsf{app}(d, e)$ が生じる。定数を引数に適用したものもやはり行き詰まるからである。

評価

$\llbracket t \rrbracket\rho$ は弱頭部形式まで評価する：

\begin{aligned} \llbracket v \rrbracket\rho &= \mathsf{atom}(v), & \llbracket x \rrbracket\rho &= \mathsf{free}(x), & \llbracket i \rrbracket\rho &= \mathrm{force}(\rho_i), \\ \llbracket \lambda.\,t \rrbracket\rho &= \mathsf{clo}(t, \rho), & \llbracket t\,u_1 \cdots u_n \rrbracket\rho &= \mathrm{app}(\cdots\mathrm{app}(\llbracket t \rrbracket\rho, \mathsf{delay}(u_1, \rho))\cdots, \mathsf{delay}(u_n, \rho)), \end{aligned}

\mathrm{app}(\mathsf{clo}(t, \rho), e) = \llbracket t \rrbracket(e \cdot \rho), \qquad \mathrm{app}(d, e) = \mathsf{app}(d, e) \ \text{otherwise}, \qquad \mathrm{force}(\mathsf{delay}(t, \rho)) = \llbracket t \rrbracket\rho .

引数は遅延されるので、評価は名前呼びである：使われない引数は決して評価されない。メモ化はなく、2 回使われる遅延引数は 2 回評価される。

読み戻し

$R_n(d)$ は $n$ 個の束縛子の下で $d$ を読み戻す：

\begin{aligned} R_n(\mathsf{atom}(v)) &= v, & R_n(\mathsf{free}(x)) &= x, & R_n(\mathsf{lvl}(\ell)) &= n - 1 - \ell, \\ R_n(\mathsf{clo}(t, \rho)) &= \lambda.\, R_{n+1}\big(\llbracket t \rrbracket(\mathsf{lvl}(n) \cdot \rho)\big), & R_n(\mathsf{app}(d, e)) &= R_n(d)\; R_n(e), & R_n(\mathsf{delay}(t,\rho)) &= R_n(\llbracket t \rrbracket\rho). \end{aligned}

クロージャは新しい変数に適用することで読み戻される。その変数はレベル $n$ で表され、値がさらに束縛子の下へ運ばれても変わらず、出現位置でインデックス $n - 1 - \ell$ に変換される（debruijn の設計のレベルを参照）。閉じた $t$ について normalize(t) は $R_0(\llbracket t \rrbracket[\,])$ である。

設計上の決定

型なし NbE には予算が必要

問題。 $\Omega = (\lambda.\,0\,0)(\lambda.\,0\,0)$ に対して、評価は $\mathrm{app}(\mathsf{clo}(0\,0, [\,]), \cdot)$ を際限なく展開する。型付きの設定では停止性は定理である（stlc の設計）が、ここでは成り立たない。

選択。 ノードの評価 1 回、force 1 回、読み戻しの 1 ステップごとに燃料を 1 単位消費し、燃料が尽きると消費量とともに FuelExhausted を返す。予算はすべての段階を通して受け渡されるので、束縛子の下での読み戻し（クロージャ本体を評価することがある）のコストも含まれる。

予算における決定性。 計算は停止のため以外に燃料を調べないので、燃料 $f$ で実行して $c \le f$ 単位を消費した後に正規形で終わる実行は、任意の燃料 $f' \ge c$ でもまったく同じ計算を行う。したがって結果は再現可能であり、consumed はその結果を得るためのちょうど最小の予算である。

問題。 正格評価（値呼び）は $(\lambda.\,7)\,\Omega$ で発散するが、この項は正規形 $7$ を持つ。

選択。 引数は遅延される。各中立項の先頭を先に評価してから引数を評価し、先頭が判明してから初めてクロージャに入る読み戻しと合わせて、これは正規順序（最左最外）簡約、すなわち eval の設計の正規化戦略を実現する。必要呼びなら遅延された結果を共有するが、可変なサンクを必要とするため採用しておらず、予算によって再計算のコストは有界かつ可視に保たれる。

不透明な意味値

Semantic[T] は非公開の列挙型を包む構造体である。呼び出し側は中立値の作成（reflect_free、reflect_level）、評価、quote はできるが、スコープの正しくない環境を持つクロージャは構築できない。これにより、すべてのクロージャの環境がその本体のスコープと一致するという不変条件が保たれる。eval が入力を一度だけ検証し、その後はすべてのインデックス参照を信頼できるのはこのためである。

正規形における単項適用

読み戻しは $R_n(\mathsf{app}(d, e)) = R_n(d)\,R_n(e)$ を単項の Apply として生成するので、スパイン $f\,a\,b$ は Apply(Apply(f, [a]), [b]) として返される。スモールステップ簡約器は入力の n 項 Apply(f, [a, b]) を保つ。どちらも同じカリー化された適用を表すので、2 つの正規化器を比較する際はまずスパインを平坦化しなければならない。

正しさ / 不変条件

定理（健全性）。 normalize(t, fuel) が NormalForm(u, _) を返すならば、 $u$ は β 正規であり、 $t =_\beta u$ である（スパインの平坦化を除いて）。

証明概要。 $n$ 個の束縛子の下での値の表示 $\lfloor d \rfloor_n$ を、それが表す項として定義する： $\lfloor \mathsf{clo}(t, \rho) \rfloor_n = \lambda.\,t[\rho]$ 、 $\lfloor \mathsf{delay}(t, \rho) \rfloor_n = t[\rho]$ 、 $\lfloor \mathsf{lvl}(\ell) \rfloor_n = n - 1 - \ell$ などであり、ここで $t[\rho]$ は $t$ の自由なインデックスに $\rho$ の表示を代入する。評価に関する帰納法により $t[\rho] \to_\beta^{*} \lfloor \llbracket t \rrbracket\rho \rfloor_n$ が成り立つ：自明でない唯一のケースは $\mathrm{app}(\mathsf{clo}(t, \rho), e)$ であり、これは β ステップ $(\lambda.\,t[\rho])\,\lfloor e \rfloor \to_\beta t[\lfloor e \rfloor \cdot \rho]$ である（debruijn の付録の代入補題）。読み戻しは束縛子の下に β ステップを挿入するだけなので、 $t \to_\beta^{*} u$ となる。正規性について： $R$ は $\lambda$ をクロージャからのみ生成し、適用を $\mathsf{app}(d, e)$ からのみ生成するが、その先頭 $d$ は中立項か定数であり、決してクロージャではない（クロージャの適用は格納されずに評価される）。よって出力は次の文法に従う

\mathit{nf} \;::=\; \lambda.\,\mathit{nf} \;\mid\; \mathit{ne}, \qquad \mathit{ne} \;::=\; x \;\mid\; i \;\mid\; v \;\mid\; \mathit{ne}\;\mathit{nf},

これは簡約基 $(\lambda.\,t)\,u$ を含まない。 $\square$

完全性（証明概要）。 $t$ が β 正規形を持つならば、十分な燃料があれば normalize はそれを返す。評価は名前呼びで弱頭部正規形を計算し、読み戻しはクロージャの本体と、中立項の先頭の後の引数を再帰的に正規化する：これは先頭と引数に分解された最左最外戦略である。正規化定理（Barendregt 13.2.2）によりこの戦略は正規形を持つすべての項で停止し、合流性により正規形は一意である。¹1 型なし NbE については K. Aehlig and F. Joachimski, “Operational aspects of untyped normalisation by evaluation”, Mathematical Structures in Computer Science 14, 2004 を、評価による強簡約については B. Grégoire and X. Leroy, “A compiled implementation of strong reduction”, ICFP 2002 を参照。

スモールステップ簡約との一致。 健全性と合流性により、同じ項に対して @nbe.normalize と @debruijn.normalize がともに正規形を返すときは常に、2 つの正規形はスパインの平坦化後に等しい。src/utlc/nbe/nbe_test.mbt のテストはこれに加え、 $(\lambda.\,7)\,\Omega$ での遅延性、 $\Omega$ での燃料切れ、quote がレベルをインデックスに戻すことを検査する。

その他の不変条件：

eval と normalize は、何の処理も行う前に、スコープの正しくない入力を ScopeFailure と consumed=0 で拒否する。
quote(value, n, _) が ScopeFailure を返すのはレベル変数が $n$ 未満でない場合のみであり、eval が生成しレベル 0 で quote した値ではこれは起こりえない。
燃料：consumed は与えられた燃料を超えることがなく、上記の決定性が成り立つ。

却下した代替案

型付きまたは η 長形式の読み戻し。 型なしの読み戻しはどこで η展開すべきかを知りえない。型付き項に対する η 長形式の正規形は stlc が提供する。
ホスト言語のクロージャ（HOAS）。 $\mathsf{clo}$ を MoonBit の関数として表せば高速になるが、燃料の計上や値の検査が不可能になり、ホスト側で新しい変数を使う工夫なしには値を quote することもできない。一階のクロージャならすべてを観察可能に保てる。
名前付き環境。 環境を De Bruijn インデックスで添字付けすることで参照は位置によるものとなり、評価中に新しい名前を必要としない。

境界

β のみ：η も定数の簡約もない。
全域的ではない：FuelExhausted は発散する項に対して予期される結果であるが、発散を証明するものではない。
遅延された引数は共有されない。
正規形は単項適用を用いる。
入力は De Bruijn 構文でなければならない。名前付き項は @debruijn.from_named で変換し、結果は @debruijn.to_named で戻すこと。

型なし NbE については K. Aehlig and F. Joachimski, “Operational aspects of untyped normalisation by evaluation”, Mathematical Structures in Computer Science 14, 2004 を、評価による強簡約については B. Grégoire and X. Leroy, “A compiled implementation of strong reduction”, ICFP 2002 を参照。 ↩