“行政正规形（ANF）也显式安排左到右求值，但目标函数仍普通返回，中间结果由 let 命名，并未把续延作为目标程序参数。其编译算法用一个高阶函数组织输出，不构成输出已经是 CPS 的证明；两种…”
形式陈述
行政正规形（ANF）使复合运算的输入已经是值或名字，把求值次序显式写成 let 链。它不是把程序算到β-正规形。以下固定左到右传值语言，输入已经通过唯一身份解析，绑定不可变，状态仅由显式引用单元读写；整数无溢出，单线程，无异常处理器和一等控制。
给出一个受限但完整的目标文法。原子 fun b -> N。简单计算 add(a,a)、ref(a)、load(a)、store(a,a)、call(a,a)、pair(a,a)、fst(a)、snd(a)。正规表达式 return a 或 let b=c in N。函数体仍是 N；创建函数值不执行函数体。该文法没有 if，条件分支扩展在边界处另述。
转换维护新鲜临时 ID，并有两个互递归接口：norm(e) 返回一个正规表达式；atom(e,k) 把 e 规范化，最后将得到的原子交给生成剩余目标语法的编译期函数 k。k 不是生成代码里的运行时续延参数。
text
atom(number_or_unit_or_var, k) = k(number_or_unit_or_var)
atom(fun b -> e, k) = k(fun b -> norm(e))
atom(let b=e1 in e2, k) =
atom(e1, a1 => let b=a1 in atom(e2,k))
atom(e1 ; e2, k) =
atom(e1, ignored => atom(e2,k))
atom(op(e1,...,em), k) =
atom(e1, a1 => ... atom(em, am =>
let fresh_t=op(a1,...,am) in k(fresh_t)) ...)
norm(e) = atom(e, a => return a)op 包括上列 ref/load/store/call/pair 等，参数一律依原 AST 顺序原子化。store 返回 unit；序列丢弃第一个结果，仍保留产生结果的 let 链，所以副作用没有被删掉。let 的右侧可以是原子别名，故目标文法允许 let b=a in N；以后删除此类绑定是独立的代换优化。
临时量必须与所有源声明 ID 及先前临时 ID 不同。输入已唯一化也保证提取嵌套 let 时，不会把外部同名变量意外捕获。实现 k 只应用一次，不反复复制其产生的后缀；用节点构造而不是不断拼接字符串，可在输入 n 个节点和输出 m 个节点上用
直觉
表达式 f(g(1)) 隐含“先得到 f，再算 g(1)，最后调用”。ANF 把这些暂时停留在求值器中的中间结果变成显式名字。效果类似把一长句拆成几句按次序执行的指令，却仍保留词法函数的结构。
CPS把“接下来做什么”变成目标程序的显式续延参数；本页只是用编译期 k 组织输出 let 链，生成函数仍普通返回。两者可有紧密语义关系，但“转换实现用了函数 k”不等于“输出已经是 CPS”。
例子与边界
两次调用不能交换，也不能重复
设 cell 初值为 4，f(d) 执行 cell := !cell+d; !cell。源表达式为 f((f(1); 2))。函数位置 f 先作为值确定，随后参数中的 f(1) 把 cell 改成 5，序列再产生 2，最外层调用把 cell 改成 7，最终结果 7。
以 f 的唯一身份为 f#7，转换得到：
text
let t1 = call(f#7, 1) in
let t2 = call(f#7, 2) in
return t2t1 未被读取不意味着其绑定可删除：call 可能写共享状态。删除第一行会得到 6；交换两行会先写 6、再写 7，却返回第一行原本对应的 6，输出和事件次序都错。若把 call(f#7,1) 同时展开到多个使用处，更会重复副作用。
函数体自己的转换为：
text
fun d#4 ->
let t3 = load(x#1) in
let t4 = add(t3,d#4) in
let t5 = store(x#1,t4) in
let t6 = load(x#1) in
return t6x#1 是指向同一单元的位置。load(x#1) 不是原子：若把它视为永远可重复的纯名字，就会在 store 前后读到不同数值。也不能把 t3 等绑定提升到 fun 外面；函数创建时不应立即读写 cell，而每次调用必须重新执行自己的读写。
let 结合依赖绑定身份
输入 let a=(let b=ref(0) in b) in !a 可规范成 let b=ref(0) in let a=b in let t=load(a) in return t。位置仍只有一个，a、b 是同一引用值的别名。若源中另有外部文本名 b，唯一声明 ID 使两个 b 不混淆；只按字符串把 let 外提会产生捕获。
若扩展条件语句，可允许简单计算 if a then N1 else N2，把整个选择结果命名一次。分支体必须留在分支内：if true then 1 else store(x,99) 不能变成先执行 store 再选择。另一种办法是让 N 含尾部 if，并引入显式 join；不能把相同的大后缀复制进每个嵌套分支后仍宣称输出线性。本页 checker 的源子集没有 if，不把该扩展标成已实现。
推论与应用
保持什么，为什么保持
观察包括终止返回值、引用别名关系及 ref/load/store 的有序事件；新 let、名字查找和临时量绑定不是源可见事件。源位置与目标位置一一对应，引用创建扩展这份对应，普通算术与 pair 不改变存储。函数值按对应环境及转换后的函数体配对。
对 atom 的接口建立归纳性质：在对应环境与存储下，转换只先执行源 e 会执行的效果，产生与源结果对应的原子值，然后才执行 k 给出的后续代码。原子规则无新增效果；函数规则只构造值，其体在未来调用时使用归纳性质；let 先完成 e1 再进入绑定后的 e2；op 连续应用归纳假设，得到与源相同的从左到右参数次序，再恰执行一次操作；序列保留第一段效果后丢弃值。因此 norm 保持每次终止执行的值、状态和事件。
这份大步归纳不直接构成所有发散行为的完备证明。对于当前语法导向转换，每个源求值步骤只插入有限的管理步骤，且没有新递归调用边，可进一步建立小步模拟处理发散；含异常、捕获续延或资源失败的扩展必须重写观察与证明。ANF 也可能改变临时值存活范围，结果保持不自动证明最大堆空间相同。
运行时每个新 let 增加一次绑定动作，复合操作次数保持。最多同时活着多少临时量需另做活跃性分析；checker 用 Python 字典环境执行 AST，复制环境与打印事件的成本不等于寄存器 IR 的机器成本。记录 e 个事件至少需要
迁移任务：将外层表达式改成 (f(1),f(2))。答案是 (5,7)，最终 cell=7，先后两个 pair 字段必须保存各自当时的返回值；不能最后读取 cell 两次而输出 (7,7)。再将函数体改为 fun d -> (ref(d),ref(d))：每次调用必须分配两个不同位置，ANF 可以给两次 ref 命名，不能将它们公共子表达式合并。
完整前端终点将 token、声明身份、ANF 和运行事件连起来，随后把 ANF 函数交回已有闭包转换。SSA的控制流汇合与 φ 节点继续由原路线负责；ANF 的唯一临时名字并不自动等于那份 CFG 契约。
参考资料
[1] Cormac Flanagan、Amr Sabry、Bruce F. Duba、Matthias Felleisen，The Essence of Compiling with Continuations，PLDI 1993，237–247；作者公开稿 §4 “A-Normal Form Compilers”、附录 A 的线性 A-normalization 算法。原文提供 ANF 与 CPS 编译的研究背景；本页目标文法、有状态教学变换与证明义务单独明示，不把所有原文定理搬到本扩展。
[2] Andrew W. Appel，Compiling with Continuations，Cambridge University Press，1992，Chapters 1–3。CPS 基础公式和保持目标沿用本站CPS 变换页，本页不把管理结构消除误称为 β-正规化执行。