paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Tail recursion modulo context: An equational approach (extended version)

模上下文的尾递归:一种等式推导方法(扩展版)
JFP vol.352025匹配度 1/10 · 论文属于纯编程语言与编译优化方向,研究尾递归模上下文的等式推导与实现,未涉及 LLM、Agent、静态分析或浮点/贝叶斯程序分析,与用户当前 PL×AI 交叉方向无关。引用 2 inbox
DAAN LEIJEN, ANTON FELIX LORENZEN
crossref: 2026-09-10

AI 速览

一句话:将尾递归模 cons 推广为模上下文,用等式推导出通用 TRMC 算法,并在 Koka 中实现可适应非线性控制的混合版本。

尾递归模 cons(TRMc)变换可把不完全尾递归的函数改写成高效尾递归形式。本文将其推广为尾递归模上下文(TRMC),从规范出发用等式推导出通用算法:为抽象上下文实现 application 与 composition 并满足上下文律即可得到一个实例。除已知的 CPS/求值上下文与结合运算外,还给出去函数化求值上下文、monoid、半环、指数和域等实例;用 Minamide 空洞演算证明 modulo cons 实例可靠,并用 Perceus 堆语义精确论证原地更新。此前方法在 call/cc、shift/reset、代数效应处理器等非线性控制下失效,本文把堆语义扩展为可动态适应非线性控制流的混合方法,在 Koka 中完整实现,基准显示变换后函数不慢于手工替代方案。

问题
许多函数因构造数据结构而非尾递归,无法在常量栈空间中高效执行;已有的 TRMc 变换仅适用于 cons,且遇到 call/cc、shift/reset、代数效应处理器等非线性控制时失效。
方法
把 TRMc 推广为模上下文(TRMC),从规范出发通过等式推导出通用算法,并用抽象上下文的 application/composition 实现与上下文律来实例化;针对具体实例分别用 Minamide 空洞演算和 Perceus 堆语义证明其可靠性,并将堆语义扩展为动态适应非线性控制流的混合方法。
评估
在 Koka 语言中完整实现混合 TRMc,并通过基准测试与手工替代方案对比,结果显示 TRMc 变换后的函数始终不慢于(且常常快于)手工写法。
原文摘要(Abstract)

Abstract The tail recursion modulo cons transformation can rewrite functions that are not quite tail-recursive into a tail-recursive form that can be executed efficiently. In this article, we generalize tail recursion modulo cons (TRMc) to modulo context (TRMC) and calculate a general TRMC algorithm from its specification. We can instantiate our general algorithm by providing an implementation of application and composition on abstract contexts and showing that our context laws hold. We provide some known instantiations of TRMC, namely modulo evaluation contexts (CPS), and associative operations , and further instantiations not so commonly associated with TRMC, such as defunctionalized evaluation contexts, monoids , semirings , exponents , and fields . We study the modulo cons instantiation in particular and prove that an instantiation using Minamide’s hole calculus is sound. We also calculate a second instantiation in terms of the Perceus heap semantics to precisely reason about the soundness of in-place update. While all previous approaches to TRMc fail in the presence of nonlinear control (e.g., induced by call/cc, shift/reset, or algebraic effect handlers), we can elegantly extend the heap semantics to a hybrid approach which dynamically adapts to nonlinear control flow. We have a full implementation of hybrid TRMc in the Koka language, and our benchmark shows the TRMc transformed functions are always as fast or faster than using manual alternatives.

链接与引用

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

BibTeX
@article{LeijenL25,
  title = {Tail recursion modulo context: An equational approach (extended version)},
  author = {DAAN LEIJEN and ANTON FELIX LORENZEN},
  journal = {Journal of Functional Programming},
  volume = {35},
  year = {2025},
  doi = {10.1017/s0956796825100117}
}