执行语义与编译实现
行一：求值状态
运行环境 ρ 把局部变量映射到值，存储 σ 把可变位置映射到值。普通求值写作 ⟨e,ρ,σ⟩ ⇓ ⟨v,σ′⟩，另有异常转移、显式退出和不终止。静态类型检查不执行一般用户函数。
常量直接得到值；名字取其词法绑定或模块已初始化全局。函数形成得到“代码+词法捕获环境”，不执行函数体。普通函数参数按值传递；引用值复制位置身份，不复制其内容。
调用先求函数，再求首个运行时实参并施于函数，得到中间结果；随后求下一个实参并施于中间函数，依此进行。类型检查已保证源码参数给足，运行时仍按逐参应用执行；不可把所有实参提前求完再执行中间函数体。隐式类型参数在静态阶段完成，运行时不执行、也不占槽位。标准库 且 等普通函数是否短路取决于它的形参是否是延迟操作；普通布尔函数调用不能自动得到特殊条件求值规则。
局部绑定先求定义，再把结果加入后式环境；顺序式先求前式，保留其存储变化、丢弃前值，再求后式。元组按项次序求值、一次存储各项。条件先求爻，只求所选分支。模式分析对象只求一次；测试模式不执行任意用户函数；仅选中分支求值。字符串拼接语法糖先左后右，即使它在语法上右结合，也不可反转副作用顺序。
源文件顶层裸式会执行；类型形成、透明别名及擦除后的类型占位不应产生用户运行副作用。依赖模块先于依赖者初始化，同一程序初始化序列不重复执行同一模块。模块入口本身不是可任意重复调用的幂等函数。
行二：递归和状态
局部/顶层递归函数的通用实现：分配单槽递归单元，初值单位；把定义中的自引用改为读该槽；求定义得到闭包；写回递归单元；返回闭包。闭包捕获的是递归单元，不能在初始化前把单位拷贝为最终自身。其他捕获值按词法环境取得；捕获引用时保留引用身份。
若一般递归值在填槽前读取自身，会观察到未初始化占位或触发后续错误；不能赋予惰性无限数据结构语义。源语言没有一般递归终止检查，也不能承诺每个通过类型检查的表达式终止。
引用操作分别分配、读、写位置。写返回单位；别名观察到同一次写。GC 搬迁后引用身份保持，原始机器地址可变，所以不以裸地址作为跨安全点稳定身份。数组边界与不安全原语不由类型系统自动证明。
行三：内建函数与异常展开
以下完整名字写在 「」 中。∀a 对应 承，箭头与元组均使用类型篇定义。
| 内建函数完整名字 | 类型 |
|---|---|
《《内建函数：整数：相等》》 |
整数→整数→爻 |
《《内建函数：整数：大于》》 |
整数→整数→爻 |
《《内建函数：整数：减》》 |
整数→整数→整数 |
《《内建函数：抛出异常字符串》》 |
∀a. 字符串→a |
《《内建函数：尝试运行字符串》》 |
∀a. ((有→a) 合 (字符串→a))→a |
《《内建函数：以当前续延调用》》 |
∀a. ((∀b. a→b)→a)→a |
注意原始“尝试运行”接收一个二元组，标准库可再提供二参数包装。有 是单位类型，元 是其值；不是可容纳任意对象的顶类型。
抛出字符串的展开：读当前异常处理器闭包，再以字符串调用它。尝试运行 (操作,处理)：
- 建立当前尝试的退出续延 K，保存先前处理器 H。
- 安装新处理器
λs. 设置H；K(处理(s))。恢复 H 在处理 s 之前，因此处理器自己再抛异常由外层处理。 - 调用
操作(元)得 r；正常完成也先恢复 H，再调用 K(r)。 - K 离开本次尝试的动态范围。异常路径不能继续执行原操作之后的普通语句。
以当前续延调用把“提前返回”包装为可传函数；调用它时恢复所保存的异常处理器，并向捕获的动态返回点送值。本基线原生用编号→栈地址表，WasmGC 用异常标签和动态标识。都不提供可任意保存并多次恢复已销毁调用栈的通用多次续延契约。
模式缺支通过生成的运行时报错入口处理，不应一律等同于用户可捕获的字符串异常。C 原语的 exit/abort 也不经过上述语言异常处理器。
编一：独立实现的阶段与不变量
| 阶段 | 输入→输出 | 必须成立的不变量 |
|---|---|---|
| 词法/语法 | 字节→令牌→表达式及声明 | 定界符正确；候选解析唯一；糖和绑定范围明确 |
| 名称解析 | 声明→文件接口引用与唯一局部引用 | 模块投影可静态消除；重导出保留来源 |
| 检查 | 名称树→已检查类型与对象 | 隐参已定；不残留未解类型；错误不得延到运行时 |
| 模式展开 | 模式→单次分析、标签测试及字段投影 | 分支结果及失败轨迹不变 |
| 类型擦除 | 已检查对象→无类型对象 | 去标注、类型值、隐式参数及抽象；源显参顺序不变 |
| 局部规范化 | 无类型对象→显式参数组 | 不改变饱和组与函数值的入口协议 |
| 递归转换 | 递归→可变单槽单元 | 填槽前闭包捕获单元，允许环 |
| 闭包转换 | 局部函数→代码与捕获元组 | 除明确直接函数外，调用都传闭包自身 |
| 全局存储/提升 | 定义→全局槽和提升代码 | 公开名与定序稳定，静态根及时登记 |
| ANF | 复杂表达式→命名中间值 | 函数先于参数；实参逐个求值；控制支不提前执行 |
| 续延/帧 | 非尾调用→帧与返回块 | 存活值入栈；返回后重载；尾调用复用帧 |
| 代码生成 | 显式存储/控制→LLVM 或 WasmGC | 遵守目标 ABI；无未解析模块或自由变量 |
内部可以合并阶段。类型检查结果应能交给一个简单不优化后端；优化器不是使非法/不完整树勉强可执行的必要条件。跨模块优化可跳过，但旧模块公开直接函数已被他方引用时必须提供相同入口或桥接包装。
编二：可直接实现的 ANF
定义 正规化(e,继续)：若 e 为直接值则交给继续；否则递归正规化其子表达式，把结果绑定为新鲜临时值，再调用继续。先将表层显参脊左折为一参数应用树，再逐节点执行 正规化(函数, λf.正规化(实参, λa.令r=调用(f,a);继续(r)))。只对已经明确分组的内部 IR 才一次传其全部参数。条件将继续接至合并点，分别生成两支；不能先计算两个分支再选择值。
局部非尾调用把后续正规式变成续延块。对该块做自由变量分析：所有调用之后仍使用的值必须有豫言帧槽；新帧放在这些槽之后。恢复块从槽 3 取返回值，再从保存槽读取存活值。允许保守地保存全部有效值，但必须初始化所有被 GC 扫描的槽，且不能遗留类型 12 游标。
尾位置包括函数体末尾、条件两支末尾、令x=调用;返回x，不能因 ANF 增加临时绑定而丢失尾位置。原生用 musttail，WasmGC 用 return_call_indirect；普通 C call 后返回不一定保证恒定栈空间。
编三：闭包与直接函数桥接
对 λx1…xn.e，按固定次序枚举自由值 v1…vk，分配 [代码,v1,…,vk]。对内部多参数节点，新代码接收 self,x1,…,xn，将 vi 引用改为 self[i]（i 从 1 起）。间接调用为：求一次闭包 c；读 c[0]；以 [c,实参…] 调代码。捕获字段排列是该闭包私有协议，不能跨闭包类型推断。
普通源码的嵌套 λ 保留逐参闭包链；不能将它擅自合并后用同一全局值替换旧闭包。跨模块直接入口按明确导出的内部参数组接收实参，不含 self。需要提供可传函数值时，创建包装闭包：包装代码丢弃 self，以原实参调用直接入口。反向桥接则直接入口取保存的闭包值，插入 self 调用它。以此保持“值全局”和“公开直接函数”两种符号都可用。
优化可能移除未使用值、合并包装或直接调用已知代码。混链测试应禁用相应跨模块假设或显式保留待测试入口，不得把已经被内联的函数当作跨对象 ABI 测试成功。
编四：数值和平台指令
整数解码取低 64 位。基线直接内建减法是 LLVM sub i64（无 nsw），再 zext 至 i128 附标签；比较为 icmp eq/sgt i64，结果零扩展附爻标签。普通 C 运行时加减乘除使用有符号 int64_t 算术；溢出、除零和最小整数除负一没有统一稳定承诺。必须分清内建指令路径与 C wrapper 路径，不把两者统一为未验证的“全环绕整数”。
小数是 binary64；LLVM 常量先 bitcast double→i64 再零扩展附标签。普通打印 %lf 与中间产物精确表示 %.17g 不同。不得通过普通打印再解析生成浮点常量，否则会丢失精度。字符串常量按实际 UTF-8 字节生成，并加末尾零；源码长度、码点长度与运行时字节长度分别处理。
编五：中间产物和外部可见性
独立编译器不必复现 JSON 缓存格式才具有 ABI 兼容性。如果要消费原编译器的阶段文件，则须另遵守 ["豫言中间单元一", 阶段名, 有序定义数组]，每定义 [名,公开性,表达式]，并按对应阶段解释绑定索引、节点形状、文件身份及版本。阶段文本只是数据，不应执行其中任意函数。
对象互操作所依赖的是 .o 与符号身份。语言服务器协议、源码排版、包管理网站、缓存命中方式、调试注释及本地临时符号不在 ABI 验收内；不得以这些不相同否定已通过的对象调用兼容，也不得以它们相同代替 ABI 验证。