语义架构

本指南说明 type_theory 的各个包如何组合在一起：哪个包定义什么、λ 演算的三个范式化器之间的关系，以及失败如何报告。各设计页面给出定义与证明。

层次

本库分层构建，每一层都以其下方的层来定义。

名字（core）。名字是按相等性比较的字符串；新鲜性总是相对于一个显式的已用名字集合，因此每个结果都是确定的。
绑定语法（syntax）。Term[T] 是带不透明常量、n 元应用和单变量绑定子的具名语法。自由变量、α-等价和避免捕获的重命名在此定义。trait BindingSyntax 通过单层视图为任意下游 AST 暴露相同的结构。
代换（substitution）。同时、一趟、避免捕获的代换，带有复合与代换引理，适用于 Term[T] 及每个 BindingSyntax AST。
重写（rewrite、eval）。规则在项的根处重写它；遍历在某一个位置应用规则并报告规则与路径；范式化器与轨迹在步数上限内重复单步。eval 为标准策略命名。
演算（utlc/lambda、debruijn、utlc/nbe、stlc）。具名与无名形式的无类型 λ 演算、无类型的基于求值的范式化，以及简单类型 λ 演算。

下游 AST 通过实现 BindingSyntax 进入第 2 层（见 adapter 设计），然后直接使用第 3 层和第 4 层。领域规则、规范形式和不动点策略都留在下游包中；基底不固定其中任何一项。

一种语义，三个范式化器

无类型 λ 演算只有一个参考语义：具名项上的正规序 β(-η) 归约，即由重写层产生的单步序列。另外两个更快的实现以它为基准进行检验。

范式化器	表示	策略	界限	输出
`@lambda.normalize`	具名 `Term[T]`	正规序，β 与 η	步数上限	β-η 范式，保留 n 元脊
`@debruijn.normalize`	`DbTerm[T]`	正规序，β	步数上限	β 范式，保留 n 元脊
`@nbe.normalize`	`DbTerm[T]`	求值 + 读回，传名调用	燃料	β 范式，一元应用

它们在如下意义上一致。转换为 De Bruijn 形式与 β 步在 α-等价意义下交换（debruijn 设计），因此具名与无名归约器执行对应的步骤。NbE 对 β 是可靠的，并实现了相同的范式化策略（utlc/nbe 设计）。由于 β 归约是合流的，只要其中两者对同一个项都返回 β 范式，结果在转换并展平应用脊之后就是一致的。η 只属于具名归约器。

对于有类型项，stlc 增加了第四个范式化器：类型导向的 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 没有 η 律。

正确性检查清单列出了经过审查的不变式、其依据以及已知问题。