意味論のアーキテクチャ

このガイドでは type_theory のパッケージがどのように組み合わさるかを説明する：どのパッケージが何を定義するか、λ計算の 3 つの正規化器がどう関係するか、失敗がどう報告されるかである。定義と証明は個々の設計ページにある。

層

ライブラリは層状に構築されており、各層はその下の層によって定義される。

名前（core）。名前は等価性で比較される文字列であり、新しさは常に明示的な使用済み名前の集合に対して相対的に決まるので、すべての結果は決定的である。
束縛構文（syntax）。Term[T] は不透明な定数、n 項適用、1 変数の束縛子を持つ名前付き構文である。自由変数、α同値、捕獲回避リネーミングはここで定義される。トレイト BindingSyntax は 1 層のビューを通じて任意の下流 AST に同じ構造を公開する。
代入（substitution）。同時・1 パス・捕獲回避の代入であり、合成と代入補題を備え、Term[T] とすべての BindingSyntax AST に対して使える。
書き換え（rewrite、eval）。規則は項をその根で書き換え、走査はそれを 1 つの位置で適用して規則とパスを報告し、正規化器とトレースはステップ数の上限内で単一ステップを繰り返す。eval は標準的な戦略に名前を与える。
計算体系（utlc/lambda、debruijn、utlc/nbe、stlc）。名前付き形式と名前なし形式の型なしλ計算、型なしの評価による正規化、単純型付きλ計算である。

下流の AST は BindingSyntax を実装することで第 2 層に入り（adapter の設計を参照）、その後は第 3 層と第 4 層を直接使う。ドメイン規則、標準形、不動点の方針は下流のパッケージにとどまり、基盤はそのいずれも固定しない。

1 つの意味論、3 つの正規化器

型なしλ計算には参照意味論が 1 つある：名前付き項上の正規順序 β(-η) 簡約、すなわち書き換え層が生成する単一ステップの列である。より高速な 2 つの実装はこれに照らして検査される。

正規化器	表現	戦略	上限	出力
`@lambda.normalize`	名前付き `Term[T]`	正規順序、β と η	ステップ数上限	β-η 正規形、n 項スパインを保持
`@debruijn.normalize`	`DbTerm[T]`	正規順序、β	ステップ数上限	β 正規形、n 項スパインを保持
`@nbe.normalize`	`DbTerm[T]`	評価 + 読み戻し、名前呼び	燃料	β 正規形、単項適用

これらは次の意味で一致する。De Bruijn 形式への変換は α同値を除いて β ステップと可換であり（debruijn の設計）、したがって名前付きと名前なしの簡約器は対応するステップを踏む。NbE は β に関して健全であり、同じ正規化戦略を実現する（utlc/nbe の設計）。β 簡約は合流的なので、そのうち 2 つが同じ項に対して β 正規形を返すときは常に、変換と適用スパインの平坦化の後に結果は一致する。η は名前付き簡約器にのみ含まれる。

型付き項については、stlc が 4 つ目の正規化器を加える：型主導の NbE であり、上限を必要とせず、β 正規かつ η 長形式の結果を返すので、型の付いた項の β-η 等価性を決定する（η は関数型について）。

失敗の報告

公開境界における想定内の失敗は値であり、決して中断ではない：

無効な入力データは Result 型で報告される。例えば RuleName::new("") は Err(RuleNameError::Empty) を返し、型エラーは TypeError の値である；
De Bruijn 項におけるインデックスエラーは ScopeError の値であり、DbStepResult、DbNormalizationResult、および NbE の結果によって運ばれる；
ステップや燃料が尽きることは通常の結果（StepLimitReached、FuelExhausted）であり、行った作業量を報告する。

処理を中断しうる関数には unsafe_ が付けられ（RuleName::unsafe_new）、リテラルのように妥当性が明らかな値のためのものである。代入における新しい名前の検査のような内部アサーションは、対応する設計ページの補題により到達不能である。

既知の限界

Term[T] は T を閉じたものとして扱う。定数の中で変数が探されることはない。
汎用の代入は一度だけ適用される。挿入された置換項が再び訪問されることはない。
型なしの正規化は全域的ではない。発散する項に対しては StepLimitReached や FuelExhausted が想定される結果である。
単純型付き計算体系には基本型、Unit、矢印型しかなく、Unit に対する η 則もない。

正しさのチェックリストには、監査済みの不変条件、その根拠、既知の問題が列挙されている。