依赖类型 elaboration

表面语言允许人省略显然信息，核心语言要求机器把每个依赖关系写清。Elaborator 就像排版前的技术编辑：根据上下文补上宇宙层、隐式类型参数和强制运输，把模式子句重排成核心消去；最后由独立内核检查成稿，而不是要求用户信任编辑过程没有猜错。

依赖类型让这种补全具有反馈回路。选择一个隐式实参会改变后续参数的类型，后续显式实参又可能反过来确定先前的 metavariable。双向方向标记限制信息流，约束队列保存尚未确定的部分；二者共同把全局猜测缩小成可管理的局部求解，却不能消灭固有歧义。

设核心恒等函数为

表面项 id true 没写隐式 $A$。elaborator 先输出候选 $\mathsf{id}\{?A\}\mathsf{true}$，再由 $\mathsf{true}:\mathsf{Bool}$ 产生约束 $?A\equiv \mathsf{Bool}$，求解后得到核心项

若期望类型已经是 $\mathsf{Bool}$，checking 方向可更早传播该信息。对

调用 append xs ys 会从两个向量的类型恢复 $m,n$，再把结果类型实例化；这不是运行时读取长度，而是解 typing constraints。

边界例子是 λx. x 处在 synthesis 位置且没有注解：$x$ 的类型无来源，系统可拒绝或要求 annotation，不能凭“显然是恒等函数”选择某一个宇宙与类型。另一个边界是方程 $?Fx\equiv t$ 的高阶求解；若允许任意 metavariable 函数，可能有多个不可比较解或进入不可判定搜索。实现常采用 pattern unification、occurs check、冻结约束与用户交互，这些是有意限定的完备范围，不应包装成一般依赖类型推断。

固定一个 Π/Nat/Vec 显式核心 ​

前面的例子说明一般 elaboration 的信息流；现在单独固定核心 $\mathcal{K}$，把“最后交给内核”展开为可逐项检查的任务。宇宙层级 $i,j\in \mathbb{N}$ 是写在语法上的数，不含待求解的层级洞。规则为

此处没有宇宙累积：$A:{\mathcal{U}}_i$ 不自动成为 $A:{\mathcal{U}}_{i+1}$，更没有 ${\mathcal{U}}_i:{\mathcal{U}}_i$。层级的后继与 Π 的最大值规则可对照标准宇宙层次。[2] 以下不是任何证明助理全部表面语法的复制。

核心项只含变量、已检查常量、宇宙、Π、带参数类型的 $\lambda (x:A).t$、应用，以及下列 Nat/Vec 原语；所有参数与层级均显式，没有 metavariable、隐式实参、模式子句或一般递归。局部语境依次检查，每个声明的类型只能使用其之前的变量。应用按 Π 消去把实参同时代入余类型，全部替换均避免捕获。

自然数和向量的形成、构造规则为

$0,1,2,\dots$ 只是 zero 与有限次 succ 的缩写。下标 $i$ 防止含混地把同一个类型悄悄抬到不同宇宙。

消去子必须带齐 motive 和分支 ​

自然数消去子是全参数项构造，规则为

向量的 motive 还必须接收向量自身，而不只是长度。给定 $A:{\mathcal{U}}_i$，规则为

每行都是当前良构语境里的类型义务，不是 elaborator 可以宣称已解决的注释。尤其 $Pnv$ 是 ${\mathcal{U}}_j$ 中的类型，而 $P$ 的函数类型位于 ${\mathcal{U}}_{max(i,j+1)}$；自然数 motive 的函数类型也位于 ${\mathcal{U}}_{j+1}$，不能把这两个层次混为一谈。

消去子的四条 ι-计算为

若被消去项是变量等中立项，消去子停住，不凭长度猜出其所有元素。Nat/Vec 的这组显式接口与实现方式可对照文献。[1] 该教程用 Type:Type 简化实现；本页改用上面的分层规则，不借该简化版本声称正规化或一致性。

把向量连接编译成完整消去项 ​

先把按第一个参数递归的加法声明为已检查的透明常量：

检查 motive 得到 $\mathsf{Nat}\to {\mathcal{U}}_0$，基分支为 $n:\mathsf{Nat}$，后继分支为 $\mathsf{Nat}\to \mathsf{Nat}\to \mathsf{Nat}$。ι-规则于是给出

对每个固定层级 $i$，目标连接函数类型为

在语境 $A:{\mathcal{U}}_i$ 中，写出三个仅用于展示的缩写；内核收到的是将它们展开后的项，不把它们当作新增公理：

完整定义为

消去结果是一个仍接受 $n,ys$ 的函数，因此这一项恰有上述 Π 类型。两个分支的检查具体如下：

• 基分支要求 $M_{A}0({\mathsf{nil}}_i(A))$。展开 motive 和 add 0 n 后得到 $\mathrm{\Pi }n.{\mathsf{Vec}}_i(A,n)\to {\mathsf{Vec}}_i(A,n)$，正由 $z_A$ 居留。
• 后继分支里 $ihnys:{\mathsf{Vec}}_i(A,\mathsf{add}kn)$。cons 的显式长度参数必须是 $\mathsf{add}kn$，输出长度为其后继。期望的长度是 $\mathsf{add}(\mathsf{succ}(k))n$，由加法计算转为同一后继，所以 conversion 成功。

这也解释了为什么按第一个向量消去时，选按第一个参数计算的加法最直接。把规格机械换成 $\mathsf{add}nm$，开放的后继分支一般不会靠当前计算规则变成同一类型；加法可交换的命题证明不是本核心自动执行的 conversion。

独立核检查实际检查哪些东西 ​

核心保存有限、有顺序的透明声明表 $c:A:=t$。每项只可引用先前已检查常量；先确认 $A$ 是某宇宙中的类型，再检查 $t:A$，通过后才加入声明表。这排除前向引用和自引用；递归计算只来自上述消去子。局部语境也按同样的前缀良构原则检查。

以下是全注解核心的检查接口。Sort(A) 综合 $A$ 的类型，并要求其弱头归约结果为某个 ${\mathcal{U}}_i$，返回 $i$。Check(t,A) 先确认 $A$ 为类型（父规则已建立的良构性可复用），再综合 $t$ 的类型 $B$，调用 Conv(B,A)。综合规则逐个覆盖所有项构造：

Conv 只使用 λ 的 β、上述 ι 和已检查透明常量的 δ 展开，连同同余与 α 改名。不给函数 η、等式反映或任意数学定律开后门。一个直接实现把两侧递归归约到正规形，按绑定器的 α 等价比较。若得到同一个正规形，两条有限归约链就见证定义相等，conversion 有合法依据；层级标号也必须相同。

为了使这个教学检查器对任意输入都能返回，可给整个检查调用一个有限工作预算，每次递归处理语法节点和归约步骤都消耗预算；不足时返回 unknown，绝不返回 accept。这给出一个可能不完备的、终止的接受检查器，不需要把“所有原始语法都正规化”当成前提。更高效且完备的转换判定依赖相应类型理论的正规化、构造器可辨识性等元理论；正规化定理的输入首先是良构类型和良型项。[3]

接受可靠性按检查调用归纳即可定位每项责任：变量取已检查声明；Π 与 λ 使用良构扩张语境；应用由两个子推导和无捕获代入得到结果类型；Nat/Vec 构造与消去逐条使用上面的规则；conversion 成功时使用实际有限归约所见证的判断相等。声明表再按顺序归纳。因此每个接受结果都有核心推导，未知或拒绝都不产生可使用的声明。这是对所写算法的纸面论证；实际解析器、代入和归约实现仍在可信基中，不能称为已经机械化验证的软件。

两个向量的接受与两个错误候选 ​

取 $A=\mathsf{Nat},i=0$，完整输入为

构造器规则分别综合 $xs:{\mathsf{Vec}}_0(\mathsf{Nat},2)$ 和 $ys:{\mathsf{Vec}}_0(\mathsf{Nat},1)$。表面调用 append xs ys 可以推断出这三个隐式参数；内核实际收到

依次应用 Π 消去，结果为 ${\mathsf{Vec}}_0(\mathsf{Nat},\mathsf{add}21)$。两次后继归约再一次零归约给出

向量消去则先递归到空的左向量，返回 $ys$，再依次补回元素 $1$ 与 $0$；最终正规项为

确有类型 ${\mathsf{Vec}}_0(\mathsf{Nat},3)$。元素顺序与每个显式长度参数都可直接检查。

若 elaborator 错把第一个长度填成 $1$，内核会要求 $xs:{\mathsf{Vec}}_0(\mathsf{Nat},1)$，但综合得到长度2，正规形不同，拒绝。若错误的连接定义把后继分支写成只返回 ih n ys、省去 cons，分支实际长度为 $\mathsf{add}kn$，期望长度为其后继；对中立 $k$，前者是停住的消去表达式，后者的头为 succ，也不能转换。这一错误在泛型定义入库时就被拒绝，无须等到某个闭合测试。

独立重检意味着内核不采用 elaborator 声称的长度、motive 正确性或“约束已解”标记，而是从显式项和已检查声明重新推导。若两个阶段共用同一个有缺陷的代入器，仍可能一起出错；阶段分离缩小信任范围，却不是形式验证的替代品。

Elaboration 把丰富语法与小可信内核分离。notation、type class、coercion、record projection 和 tactic 可以在不扩张核心证明规则的情况下加入，只要最终生成的项通过检查。这种架构还改善错误定位：约束记录了哪一个隐式选择导致类型冲突，编辑器可展示尚未解决洞的局部语境与目标。

分离也明确了信任边界。Elaborator 有 bug 时可能拒绝合法程序或生成错误项，但健全内核会拦下后者；若编译器绕过重检、让未解 metavariable 成为任意常量，可靠性便失效。性能优化如缓存规范形、增量约束求解和启发式实例搜索都必须保持最终 core judgment 不变。