paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Low-Level Look at A-Normal Form

A-Normal Form 的低层视角
OOPSLA 8(OOPSLA2)2024匹配度 2/10 · 论文属于编译器中间表示与形式语义,讨论 ANF 与 monadic form 的低层性质,与用户关注的 LLM/Agent、面向 ML/Agentic 程序的静态分析、浮点程序分析或贝叶斯程序分析没有直接交叉。虽然其理论形式化与工程实现风格可能符合部分偏好,但研究主题不在核心方向上。引用 5 inbox
William J. Bowman
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:重新审视 ANF 的底层内涵性质,论证应优先采用 monadic form,只在低层命令式中间表示中做 A-规范化。

ANF 是被广泛研究的中间表示:它在语法中显式化局部控制流与数据流,并让控制流图等价的程序具有唯一范式。但 ANF 难以高效实现,也难以扩展新的词法作用域构造(如带作用域的区域分配),根源在于 commuting conversion 的规范化十分困难。本文指出这一源于高层演算与形式模型的传统看法是错误的:通过研究 ANF 的底层内涵(intensional)性质,作者导出一个 commuting conversion 规范化很简单的范式,无需 join point、无需代码复制、内联后也无需重新规范化,且易于扩展新的词法作用域效应。文章形式化了 ANF 与 monadic form 的联系及其内涵性质,推导出命令式 ANF,并设计了一条从含 scoped region 的未类型化 λ-演算,经 monadic form,到低层命令式 monadic form 的编译流水线;在该低层形式中 A-规范化是平凡且对区域安全的。作者证明该编译器相对 ANF 保持或优化栈与内存行为,其形式化还重建并系统化了实践(包括生产级编译器)中的务实选择。

问题
ANF 虽被广泛使用,却难以高效实现,也难以扩展新的词法作用域构造(如带作用域的基于区域的分配),其根本困难在于 commuting conversion 的规范化。
方法
通过研究 ANF 的低层内涵性质,形式化 ANF 与 monadic form 的关系,导出命令式 ANF,并设计一条从含 scoped region 的未类型化 λ-演算经 monadic form 到低层命令式 monadic form 的编译流水线。
评估
以形式化证明为主要评估手段,证明该编译流水线相对 ANF 保持或优化栈与内存行为,并将形式化结果与实践(包括生产级编译器)中的既有选择相对应。
原文摘要(Abstract)

A-normal form (ANF) is a widely studied intermediate form in which local control and data flow is made explicit in syntax, and a normal form in which many programs with equivalent control-flow graphs have a single normal syntactic representation. However, ANF is difficult to implement effectively and, as we formalize, difficult to extend with new lexically scoped constructs such as scoped region-based allocation. The problem, as has often been observed, is that normalization of commuting conversions is hard. This traditional view of ANF that normalizing commuting conversions is hard, found in formal models and informed by high-level calculi, is wrong. By studying the low-level intensional aspects of ANF, we can derive a normal form in which normalizing commuting conversion is easy, does not require join points, or code duplication, or renormalization after inlining, and is easily extended with new lexically scoped effects. We formalize the connection between ANF and monadic form and their intensional properties, derive an imperative ANF, and design a compiler pipeline from an untyped λ-calculus with scoped regions, to monadic form, to a low-level imperative monadic form in which A-normalization is trivial and safe for regions. We prove that any such compiler preserves, or optimizes, stack and memory behaviour compared to ANF. Our formalization reconstructs and systematizes pragmatic choices found in practice, including current production-ready compilers. The main take-away from this work is that, in general, monadic form should be preferred over ANF, and A-normalization should only be done in a low-level imperative intermediate form. This maximizes the advantages of each form, and avoids all the standard problems with ANF.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{Bowman24,
  title = {A Low-Level Look at A-Normal Form},
  author = {William J. Bowman},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA2},
  year = {2024},
  doi = {10.1145/3689717}
}