elab 設計

elab パッケージは stella のカーネルです。ユニット型、 $\Pi$ 、 $\Sigma$ 、同一性型、W 型、宇宙の累積的階層を持つ Martin-Löf 流の依存型理論を実装し、評価による正規化（NbE）で定義的等価性を計算する双方向検査器によって型付けを判定します。このページでは、コードが実装する規則を述べ、それらが機能するための性質を導き、実装が不完全な箇所を記録します。

設計目標

構造が理論を反映した、小さく読みやすいカーネル。判断ごとに 1 つの関数、規則ごとに 1 つの match アーム。
少ない注釈で決定可能な検査。ユーザーは検査器が推論できない箇所にだけ注釈を付けます。
計算による型の等価性。2 つの型は、構文を書き換えるのではなく、評価して正規形を比較することで比較されます。
プロジェクトが参照する文献に近い実装。Löh、McBride、Swierstra によるチュートリアル実装 $\lambda\Pi$ と、Agda に関する Norell の博士論文です。¹1 A. Löh, C. McBride, W. Swierstra, “A tutorial implementation of a dependently typed lambda calculus”, Fundamenta Informaticae 102 (2010). U. Norell, Towards a practical programming language based on dependent type theory, PhD thesis, Chalmers (2007).

数学的背景

構文

項は、それを扱う判断によって分けられます。推論可能な項（TermInf）を $e$ 、検査可能な項（TermChk）を $t$ と書くと、次のようになります。

\begin{aligned} e \;::=\;& \#i \mid x \mid \mathbf 1 \mid \mathcal U_i \mid (t : t) \mid \Pi(t, t) \mid e\;t \mid \Sigma(t, t) \mid \pi_1 e \mid \pi_2 e \\ \mid\;& \mathrm{Id}(t, t, t) \mid J(t, t, t, t, t, e) \mid W(t, t) \mid \mathrm{wrec}(t, t, t, t, e) \\ t \;::=\;& e \mid \star \mid \lambda.\,t \mid (t, t) \mid \mathrm{refl}\;t \mid \sup(t, t) \end{aligned}

束縛変数は de Bruijn インデックス $\#i$ （Bound(i)）です。 $\#0$ は最も近い外側の束縛子を指します。束縛子は $\lambda$ と、 $\Pi$ 、 $\Sigma$ 、 $W$ の第 2 引数です。束縛変数には名前がないため、2 つの項が $\alpha$ 同値であるのは木として等しいときに限ります。したがって TermInf と TermChk の導出された Eq は $\alpha$ 同値そのものです。

値と中立項

評価は項を意味領域 $D$ （Value）に写します。

\begin{aligned} v, A \;::=\;& \underline{n} \mid \mathbf 1 \mid \star \mid \mathcal U_i \mid \lambda f \mid \Pi(A, F) \mid \Sigma(A, F) \mid (v, v) \mid \mathrm{Id}(A, v, v) \mid \mathrm{refl}\;v \mid W(A, F) \mid \sup(v, F) \\ n \;::=\;& x \mid n\;v \mid \pi_1 n \mid \pi_2 n \mid J(A, v, v, v, v, n) \mid \mathrm{wrec}(A, F, v, v, n) \end{aligned}

ここで $f, F : D \to D$ は MoonBit の関数です。束縛子の本体は値上の関数になります。 $\Pi(A, F)$ は型 $\Pi_{x : A} F(x)$ です。中立項 $n$ （Neutral）は自由変数 $x$ で行き詰まった除去です。

すべての値は弱頭部正規形にあります。評価器はそのような簡約基を構築した時点で簡約するため、導入形式に除去が適用されたものは存在しません。

評価

評価 $\llbracket t \rrbracket_\rho$ （eval_inf、eval_chk）は、 $i$ 番目のエントリが $\#i$ の値である環境 $\rho$ を受け取ります。

\begin{aligned} \llbracket \#i \rrbracket_\rho &= \rho(i) & \llbracket (t : T) \rrbracket_\rho &= \llbracket t \rrbracket_\rho \\ \llbracket \lambda.\,t \rrbracket_\rho &= \lambda\bigl(v \mapsto \llbracket t \rrbracket_{v :: \rho}\bigr) & \llbracket \Pi(A, B) \rrbracket_\rho &= \Pi\bigl(\llbracket A \rrbracket_\rho,\; v \mapsto \llbracket B \rrbracket_{v :: \rho}\bigr) \\ \llbracket e\;t \rrbracket_\rho &= \llbracket e \rrbracket_\rho \cdot \llbracket t \rrbracket_\rho & \llbracket \pi_k e \rrbracket_\rho &= \pi_k \cdot \llbracket e \rrbracket_\rho \end{aligned}

他のコンストラクタも同様です。意味論的除去（val_app、val_fst、val_snd、val_j_elim、val_w_rec）が計算規則を担います。

\begin{aligned} (\lambda f) \cdot v &= f(v) && (\beta) \\ \pi_1 \cdot (v, w) = v, \qquad \pi_2 \cdot (v, w) &= w && (\Sigma\beta) \\ J(A, x, P, d, y, \mathrm{refl}\;z) &= d && (J\beta) \\ \mathrm{wrec}(A, B, P, s, \sup(a, f)) &= s \cdot a \cdot \lambda f \cdot \lambda\bigl(z \mapsto \mathrm{wrec}(A, B, P, s, f(z))\bigr) && (W\beta) \end{aligned}

中立な引数に対してはスパインを延長します。たとえば $\underline{n} \cdot v = \underline{n\;v}$ です。注釈は消去されます。

読み戻しと正規形

読み戻し $q_l$ （quote、neutral_quote）は、 $l$ 個の束縛子の下にある値を項に変換します。関数は新しい変数に適用することで読み戻されます。

q_l(\lambda f) = \lambda.\; q_{l+1}\bigl(f(\underline{\mathsf{Quote}(l)})\bigr), \qquad q_l\bigl(\Pi(A, F)\bigr) = \Pi\bigl(q_l(A),\; q_{l+1}(F(\underline{\mathsf{Quote}(l)}))\bigr),

そして、新しい変数はインデックスに戻されます。

q_l\bigl(\underline{\mathsf{Quote}(k)}\bigr) = \#(l - k - 1).

なぜ $l - k - 1$ なのか。 読み戻しは束縛子を外側からレベルで番号付けします。深さ $k$ で開かれた束縛子は $\mathsf{Quote}(k)$ を導入します。深さ $l$ では、それより後に開かれた束縛子のレベルは $k + 1, \dots, l - 1$ なので、出現箇所とその束縛子の間には $l - 1 - k$ 個の束縛子があり、これがその de Bruijn インデックスです。深さ $l$ でスコープにあるのは $\mathsf{Quote}(0), \dots, \mathsf{Quote}(l-1)$ だけなので、この変数は新しいものです。レベルにより新しさの保証は自明になり（名前の付け替えもシフトも不要）、インデックスにより出力は標準的になります。

閉じた項の正規形は $\mathrm{nf}(t) = q_0(\llbracket t \rrbracket_\varepsilon)$ です。

評価が $\beta$ を尊重する理由

NbE の中心的な補題は、 $\beta$ 等価な項は同じ値を持つ、というものです。簡約基については、

\begin{aligned} \llbracket (\lambda.\,t : T)\;u \rrbracket_\rho &= \llbracket \lambda.\,t \rrbracket_\rho \cdot \llbracket u \rrbracket_\rho \\ &= \bigl(v \mapsto \llbracket t \rrbracket_{v :: \rho}\bigr)\bigl(\llbracket u \rrbracket_\rho\bigr) \\ &= \llbracket t \rrbracket_{\llbracket u \rrbracket_\rho :: \rho} \\ &= \llbracket t[u / \#0] \rrbracket_\rho , \end{aligned}

ここで最後のステップは代入補題で、 $t$ に関する帰納法で証明されます。 $\#0$ に $u$ を代入して $\rho$ のもとで評価することは、 $\rho$ を $u$ の値で拡張したもとで評価することと同じ値を与えます。他の簡約基についても、上記の $\Sigma\beta$ 、 $J\beta$ 、 $W\beta$ を用いて同じ計算ができます。項の値はその $\beta$ 同値類だけに依存するので、正規形も同様です： $t =_\beta u \Rightarrow \mathrm{nf}(t) = \mathrm{nf}(u)$ 。逆に、 $\mathrm{nf}(t)$ は $t$ から $\beta$ ステップで到達されるので、正規形が等しければ $\beta$ 等価です。これらを合わせると、「正規形を比較する」ことは、評価が停止する項における $\beta$ 等価性の決定手続きになります。²2 U. Berger と H. Schwichtenberg の「An inverse of the evaluation functional for typed λ-calculus」（LICS 1991）が NbE を導入しました。A. Abel の Normalization by Evaluation: Dependent Types and Impredicativity（教授資格論文、LMU Munich、2013）は、 $\eta$ を持つ Martin-Löf 型理論に対する NbE の健全性と完全性を証明しています。これらは理論に関する結果であり、この実装については証明ではなくテストで確認されています。

双方向の判断

検査器には 2 つの判断があり、それぞれが 1 つの関数です。

$\Gamma; \rho \vdash_l e \Rightarrow A$ （推論、type_inf）： $e$ は型 $A$ を持ち、検査器がそれを計算します。
$\Gamma; \rho \vdash_l t \Leftarrow A$ （検査、type_chk）： $t$ は与えられた型 $A$ を持ちます。

文脈 $\Gamma$ は名前を型（値）に写し、 $\rho$ は現在の位置の環境、 $l$ は入った束縛子の数です。束縛子の下では、検査器はこの 3 つすべてを新しい変数 $x_l = \underline{\mathsf{Local}(l)}$ で拡張し、 $\Gamma, x_l : A;\ \rho, x_l \vdash_{l+1}$ と書きます。したがって $\rho$ は常に $\#i$ を変数 $x_{l-1-i}$ に写し、 $\Gamma$ がその型を与えます。以下では $\llbracket t \rrbracket$ は $\llbracket t \rrbracket_\rho$ の略記です。

変数、定数、注釈。

\dfrac{\rho(i) = \underline{x} \qquad (x : A) \in \Gamma}{\Gamma; \rho \vdash \#i \Rightarrow A}\;(\textsf{Var}) \qquad \dfrac{(x : A) \in \Gamma}{\Gamma; \rho \vdash x \Rightarrow A}\;(\textsf{Free}) \qquad \dfrac{\Gamma; \rho \vdash T \Rightarrow \mathcal U_j \qquad \Gamma; \rho \vdash t \Leftarrow \llbracket T \rrbracket}{\Gamma; \rho \vdash (t : T) \Rightarrow \llbracket T \rrbracket}\;(\textsf{Ann})

宇宙と型形成子。 ここ以降、前提 $T \Rightarrow \mathcal U_i$ は、 $T$ が推論可能な項であり、その推論された型が宇宙そのものであることを要求します。これらの前提に包摂（subsumption）はありません。

\dfrac{}{\Gamma; \rho \vdash \mathbf 1 \Rightarrow \mathcal U_0}\;(\mathbf 1\textsf{-F}) \qquad \dfrac{}{\Gamma; \rho \vdash \mathcal U_i \Rightarrow \mathcal U_{i+1}}\;(\mathcal U\textsf{-F}) \qquad \dfrac{\Gamma; \rho \vdash_l A \Rightarrow \mathcal U_i \qquad \Gamma, x_l : \llbracket A \rrbracket;\ \rho, x_l \vdash_{l+1} B \Rightarrow \mathcal U_j}{\Gamma; \rho \vdash_l \Pi(A, B) \Rightarrow \mathcal U_{\max(i, j)}}\;(\Pi\textsf{-F})

規則 $(\Sigma\textsf{-F})$ と $(W\textsf{-F})$ は、 $\Pi$ を $\Sigma$ と $W$ に置き換えた同じものです。同一性型はその台の宇宙に属します。

\dfrac{\Gamma; \rho \vdash A \Rightarrow \mathcal U_i \qquad \Gamma; \rho \vdash x \Leftarrow \llbracket A \rrbracket \qquad \Gamma; \rho \vdash y \Leftarrow \llbracket A \rrbracket}{\Gamma; \rho \vdash \mathrm{Id}(A, x, y) \Rightarrow \mathcal U_i}\;(\mathrm{Id}\textsf{-F})

導入は検査される。 期待される型が、項が省略したもの、たとえば $\lambda$ の定義域を補います。

\dfrac{\Gamma, x_l : A;\ \rho, x_l \vdash_{l+1} t \Leftarrow F(x_l)}{\Gamma; \rho \vdash_l \lambda.\,t \Leftarrow \Pi(A, F)}\;(\Pi\textsf{-I}) \qquad \dfrac{\Gamma; \rho \vdash t \Leftarrow A \qquad \Gamma; \rho \vdash u \Leftarrow F(\llbracket t \rrbracket)}{\Gamma; \rho \vdash (t, u) \Leftarrow \Sigma(A, F)}\;(\Sigma\textsf{-I}) \qquad \dfrac{}{\Gamma; \rho \vdash \star \Leftarrow \mathbf 1}\;(\mathbf 1\textsf{-I})

\dfrac{\Gamma; \rho \vdash_l t \Leftarrow A \qquad \llbracket t \rrbracket \equiv_A v \qquad \llbracket t \rrbracket \equiv_A w}{\Gamma; \rho \vdash_l \mathrm{refl}\;t \Leftarrow \mathrm{Id}(A, v, w)}\;(\mathrm{Id}\textsf{-I}) \qquad \dfrac{\Gamma; \rho \vdash a \Leftarrow A \qquad \Gamma; \rho \vdash f \Leftarrow \Pi\bigl(F(\llbracket a \rrbracket),\ \_ \mapsto W(A, F)\bigr)}{\Gamma; \rho \vdash \sup(a, f) \Leftarrow W(A, F)}\;(W\textsf{-I})

除去は推論される。 除去される項の型を推論し、それを分解します。

\dfrac{\Gamma; \rho \vdash f \Rightarrow \Pi(A, F) \qquad \Gamma; \rho \vdash t \Leftarrow A}{\Gamma; \rho \vdash f\;t \Rightarrow F(\llbracket t \rrbracket)}\;(\Pi\textsf{-E}) \qquad \dfrac{\Gamma; \rho \vdash e \Rightarrow \Sigma(A, F)}{\Gamma; \rho \vdash \pi_1 e \Rightarrow A}\;(\Sigma\textsf{-E}_1) \qquad \dfrac{\Gamma; \rho \vdash e \Rightarrow \Sigma(A, F)}{\Gamma; \rho \vdash \pi_2 e \Rightarrow F(\pi_1 \cdot \llbracket e \rrbracket)}\;(\Sigma\textsf{-E}_2)

パス帰納法。モチーフ $P$ は推論され、 $\bar A = \llbracket A \rrbracket$ 、 $\bar x = \llbracket x \rrbracket$ 、 $\bar y = \llbracket y \rrbracket$ 、 $\bar P = \llbracket P \rrbracket$ とします。

\dfrac{ \begin{gathered} \Gamma; \rho \vdash A \Rightarrow \mathcal U_i \qquad \Gamma; \rho \vdash x \Leftarrow \bar A \qquad \Gamma; \rho \vdash y \Leftarrow \bar A \qquad \Gamma; \rho \vdash p \Leftarrow \mathrm{Id}(\bar A, \bar x, \bar y) \\ \Gamma; \rho \vdash P \Rightarrow \Pi(D_1, F_1) \qquad \Gamma \vdash_l \bar A \le D_1 \\ F_1(z) = \Pi(D_2, F_2) \qquad \Gamma, z : \bar A \vdash_{l+1} \mathrm{Id}(\bar A, \bar x, z) \le D_2 \qquad F_2(w) = \mathcal U_k \qquad \Gamma; \rho \vdash d \Leftarrow \bar P \cdot \bar x \cdot \mathrm{refl}\;\bar x \end{gathered} }{\Gamma; \rho \vdash J(A, x, P, d, y, p) \Rightarrow \bar P \cdot \bar y \cdot \llbracket p \rrbracket}\;(J)

motive の宇宙レベル $k$ は固定せずに推論する。これは累積的宇宙に必要な性質である。ただし二つの定義域は引き続き検査する。 $P$ が適用されるのは $\bar A$ の点と $\bar x$ から出るパスだけなので、その定義域はこれらの引数を受け付けなければならず、 $\Pi$ は定義域について反変である。形 $\Pi(D_1, \Pi(D_2, \mathcal U_k))$ だけを検査すると、検査中に $P$ が誤った型の引数に適用されうる。

W 再帰。 $B$ は推論可能な関数 $A \to \mathcal U_k$ で、 $\bar B(v) = \llbracket B \rrbracket \cdot v$ 、 $\bar W = W(\bar A, \bar B)$ とします。

\dfrac{ \begin{gathered} \Gamma; \rho \vdash A \Rightarrow \mathcal U_i \qquad \Gamma; \rho \vdash B \Rightarrow \Pi(D, G),\ \bar A \le D,\ G(z) = \mathcal U_k \qquad \Gamma; \rho \vdash w \Leftarrow \bar W \\ \Gamma; \rho \vdash P \Rightarrow \Pi(D', G'),\ \bar W \le D',\ G'(z) = \mathcal U_m \qquad \Gamma; \rho \vdash s \Leftarrow \Pi_{a : \bar A}\, \Pi_{f : \bar B(a) \to \bar W}\, \Pi_{h : \Pi_{b : \bar B(a)} \bar P \cdot f(b)}\; \bar P \cdot \sup(a, f) \end{gathered} }{\Gamma; \rho \vdash \mathrm{wrec}(A, B, P, s, w) \Rightarrow \bar P \cdot \llbracket w \rrbracket}\;(W\textsf{-E})

方向の切り替え。 推論可能な項は、その型が期待される型の部分型であれば検査モードで受理されます。

\dfrac{\Gamma; \rho \vdash_l e \Rightarrow A' \qquad \Gamma \vdash_l A' \le A}{\Gamma; \rho \vdash_l e \Leftarrow A}\;(\textsf{Sub})

逆方向は $(\textsf{Ann})$ です。検査可能な項は、その型を書き下せば推論可能になります。

部分型付けと変換

関係 $A \le A'$ （subtype_nf。空の文脈向けには def_eq として公開）は累積性です。

\dfrac{i \le j}{\mathcal U_i \le \mathcal U_j} \qquad \dfrac{A' \le A \qquad \Gamma, x_l : A' \vdash_{l+1} F(x_l) \le F'(x_l)}{\Gamma \vdash_l \Pi(A, F) \le \Pi(A', F')} \qquad \dfrac{A \equiv A' \qquad \Gamma, x_l : A \vdash_{l+1} F(x_l) \le F'(x_l)}{\Gamma \vdash_l \Sigma(A, F) \le \Sigma(A', F')} \qquad \dfrac{A \equiv A'}{A \le A'}

$\Pi$ 規則は定義域について反変です。 $A$ のすべての要素を受け付ける関数は部分型 $A' \le A$ のすべての要素を受け付け、その $F(x)$ における結果は上位型 $F'(x)$ における結果でもあります。 $\Sigma$ 規則は第 1 成分を不変に保ちます。共変にしても健全ですが、実装とそのテストはそこで変換を要求します。

変換 $A \equiv A'$ （conv_type）は型を構造的に比較し、新しい変数で束縛子に入り、同一性型の端点を $\eta$ を加えた型主導の $\equiv_A$ （conv_nf）で比較します。

f \equiv_{\Pi(A, F)} g \iff f \cdot x_l \equiv_{F(x_l)} g \cdot x_l, \qquad p \equiv_{\Sigma(A, F)} r \iff \pi_1 p \equiv_A \pi_1 r \;\wedge\; \pi_2 p \equiv_{F(\pi_1 p)} \pi_2 r, \qquad u \equiv_{\mathbf 1} u'.

中立項はスパインごとに比較する（conv_neu）。適用の引数を正しい型で比較するために、先頭変数の型を $\Gamma$ から調べる。先頭の型が $\Gamma$ にない場合、たとえばコンテキストを持たない def_eq では、二つのスパインを読み戻しの結果で比較する。読み戻しが等しい値は定義的に等しいので、これは健全だが、引数に $\eta$ は使わない。それ以外はすべて読み戻しの比較 $q_l(v) = q_l(v')$ に帰着する。

宇宙

宇宙は可述的かつ Russell 流です。型それ自体が項であり、 $\mathcal U_i : \mathcal U_{i+1}$ です。自分自身を含む宇宙は理論を矛盾させる（Girard のパラドックス）ため、規則 $\mathcal U_i : \mathcal U_i$ はありません。³3 J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, thèse d’État (1972)。短い証明として A. J. C. Hurkens, “A simplification of Girard’s paradox”, TLCA 1995 があります。型形成子は構成要素の大きい方の宇宙 $\max(i, j)$ に属し、これが可述性の要求するところです。 $\Pi_{A : \mathcal U_0} A \to A$ は $\mathcal U_0$ 上で量化するので $\mathcal U_1$ に属します。累積性 $\mathcal U_i \le \mathcal U_{i+1}$ は型付け規則ではなく部分型付けの一部で、 $(\textsf{Sub})$ で使われます。

設計上の決定

双方向検査

問題。 依存型理論で注釈のない $\lambda$ の型を推論するには定義域を推測する必要があり、これは一般に高階単一化を意味し、高階単一化は決定不能です。

選択肢。 (a) すべての束縛子に注釈を付ける、 $\lambda (x : A).\,t$ 。(b) 単一化変数で推論する。(c) 項を検査されるものと推論されるものに分ける。

選択。 (c)。導入形式（ $\lambda$ 、ペア、 $\star$ 、 $\mathrm{refl}$ 、 $\sup$ ）は、型が欠けている情報を決定するので検査されます。除去と型形成子は、先頭の型が全体の型を決定するので推論されます。注釈が必要なのは導入が除去と出会う箇所、すなわち $(\lambda.\,t : T)\;u$ のような $\beta$ 簡約基か、モチーフが関数でなければならない箇所だけです。正規形の項は、モチーフを除けば注釈をまったく必要としません。この区別を型 TermInf と TermChk に符号化することで、注釈のない簡約基は実行時エラーではなく表現不可能になります。

クロージャを持つ値

問題。 型を比較するには、束縛子の下も含めて型を評価する必要があります。

選択肢。 (a) 代入によって構文を書き換える。これには各ステップで捕獲回避代入とインデックスのシフトが必要です。(b) 束縛子がホスト言語の関数である意味領域へ評価する。

選択。 (b)。本体は MoonBit の関数 (Value) -> Value で表現されるため、 $\beta$ 簡約はホスト関数の呼び出しであり、構文上の代入は決して起こりません。読み戻しは必要なときだけ構文を復元します。表示のため、 $q_l$ による比較のため、そして正規形を比較する検査の中でです。

項ではインデックス、値ではレベル

項はインデックスを使うので、 $\alpha$ 同値は構造的等価性となり、閉じた部分項はその位置に依存しません。値の中の新しい変数はレベル（検査器では Local(l)、読み戻しでは Quote(l)）を使うので、新しい変数の作成はカウンタのインクリメントであり、値がシフトを必要とすることはありません。2 種類の新しい変数は別々の Name コンストラクタなので、検査器が導入した変数が読み戻し中に導入された変数と取り違えられることはありません。

明示的な持ち上げの代わりに部分型付け

累積性は、明示的な持ち上げ演算子 $\uparrow : \mathcal U_i \to \mathcal U_{i+1}$ で表現することもできます。代わりにそれを方向の切り替え $(\textsf{Sub})$ に組み込むことで、 $\mathcal U_0$ で書かれた型を項レベルの型強制なしに $\mathcal U_1$ で使えます。type_chk(..., Inf(UnitType), VUniverse(1)) のようにです。

正しさと不変条件

環境の不変条件。 レベル $l$ では、env はちょうど $l$ 個のエントリを持ち、エントリ $i$ は $x_{l-1-i}$ であり、ctx はすべての $x_k$ を宣言しています。束縛子の下に入る規則だけが状態を拡張し、その際 3 つすべてを同時に拡張します。 $(\textsf{Var})$ はこの不変条件に依存しています。これを破る type_inf の呼び出し側は Internal error: Bound variable not in environment を受け取ります。
検査済みのものだけを評価する。 どの規則でも、部分項はそれを検査する前提の後で評価されます。たとえば $(\Pi\textsf{-E})$ の引数や $(\textsf{Ann})$ の型です。評価器は型の誤った簡約基で panic するので、この順序こそが型の誤った入力に対して検査器を全域的に保つものです。検査器は評価する前に TypeError を送出します。
型の安定性。 検査器が返す型はすべて値なので、呼び出し側が再び正規化する必要はなく、型の比較はすべて値の上で行われます。
停止性。 型の正しい項の評価は、W 型と可述的宇宙を持つ Martin-Löf 型理論の正規化定理により停止します。検査器は検査済みの項だけを評価する（不変条件 2）ので、規則が健全であるすべての入力で停止します。以下に挙げる欠落が例外です。

既知の欠落

実装は開発途中であり、いくつかの規則は上記の理論より弱かったり強かったりします。ユーザーが避けられるようにここに記録しますが、コードは変更していません。

部分型付けは $\Pi$ 、 $\Sigma$ 、宇宙だけ。 $W$ と同一性型は、成分に累積性を持たない変換によって比較されます。

採用しなかった代替案

名前付きの型付き項。 名前付き変数は捕獲回避代入を必要とし、 $\alpha$ 同値を別の検査にしてしまいます。de Bruijn インデックスはその両方を避けます。
代入に基づく正規化。 構文的代入の繰り返しは、クロージャへの評価より遅く、正しく実装するのも難しく、しかも別途変換の検査が必要です。
非可述的な宇宙や自分自身を含む宇宙。 $\mathcal U : \mathcal U$ は矛盾しており、非可述的な $\mathrm{Prop}$ は stella が従う理論には含まれません。
帰納族。 W 型は単一の除去子で整礎木を提供し、カーネルを小さく保ちます。一般の帰納的定義には正値性検査器が必要になります。

境界

このパッケージは意図的に次のことを行いません。

表層構文の解析、暗黙引数のエラボレーション、単一化問題の求解。項はコア構文の MoonBit 値として構築します。
定義、let、本体を持つグローバル定義のサポート。文脈には公理（型を持つ名前）だけが入ります。
宇宙多相、帰納族、空型、直和型の提供。
一価性、高次帰納型、その他ホモトピー型理論の機能の実装。論考ではそれらをプロジェクトの目標として述べていますが、実装はされていません。
評価器への型の誤った入力に対する保証。eval_inf、eval_chk、val_ 関数は panic することがあります。

A. Löh, C. McBride, W. Swierstra, “A tutorial implementation of a dependently typed lambda calculus”, Fundamenta Informaticae 102 (2010). U. Norell, Towards a practical programming language based on dependent type theory, PhD thesis, Chalmers (2007). ↩
U. Berger と H. Schwichtenberg の「An inverse of the evaluation functional for typed λ-calculus」（LICS 1991）が NbE を導入しました。A. Abel の Normalization by Evaluation: Dependent Types and Impredicativity（教授資格論文、LMU Munich、2013）は、 $\eta$ を持つ Martin-Löf 型理論に対する NbE の健全性と完全性を証明しています。これらは理論に関する結果であり、この実装については証明ではなくテストで確認されています。 ↩
J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, thèse d’État (1972)。短い証明として A. J. C. Hurkens, “A simplification of Girard’s paradox”, TLCA 1995 があります。 ↩