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