语义与类型规则速查

输入	规则	输出	边界
源码字符	scan	token流	非法字符带源位置
token流	parse	AST	歧义与恢复策略明确
Γ与表达式e	Γ ⊢ e : τ	类型τ	失败给约束来源
环境ρ与e	ρ ⊢ e ⇓ v	值v	明确求值策略
机器状态C	C → C'	下一状态	无规则时为值或停滞
根集与堆σ	reach(roots,σ)	活对象	弱引用另行处理

常用规则

变量查找使用最近词法绑定；闭包=(参数,函数体,定义环境)。按值调用先求实参，按名每次替换求值，按需首次求值后共享。类型保持要求一步求值不改变类型，进展要求良类型闭项为值或可继续。模式匹配按构造器与子模式递归，必须验证穷尽性。

使用顺序

先写语法类别与状态分量，再选规则；列出全部前提后才能得到结论。遇到类型错误追踪约束来源，遇到运行错误寻找第一步分叉，遇到并发错误比较允许交错与线性化点。速查不能替代推导树和测试。

反查清单

每次推导都检查变量是否在环境中、闭包是否保留定义环境、位置和值是否混淆、求值顺序是否写明、类型变量是否通过 occurs check、模式是否穷尽、GC根集是否完整、并发结论是否覆盖全部允许交错。公式给出结论之前，横线上每个前提都必须能由程序结构或上一条推导得到。

失败定位与交付

扫描失败检查字符类别和源区间，解析失败检查期待集合与恢复点，绑定失败检查环境父链，类型失败检查第一条冲突约束，运行失败检查第一步状态分叉，GC失败检查根集与可达边，并发失败检查导致不同观察值的最小交错。解释器交付时同时冻结语言规格、AST版本、语义规则、错误码、四类边界测试和可复现运行命令；任何优化都必须与未优化解释器做观察等价对照。