一句话:为原始余递归建立与递归对等的计算基础,借抽象机与逻辑对偶揭示求值策略对(余)递归组合子复杂度的影响。
论文针对余递归相较递归长期被忽视、缺乏同等计算基础的问题,为原始余递归给出以计算为中心的基础,并构造一个与递归原始计算模型类似的终止演算。作者通过抽象机的实现细节加强递归与余递归的联系,并利用逻辑对偶从递归语法地推导出余递归。文章还考察求值策略对原始(余)递归组合子计算复杂度的影响,指出 call-by-name 更有利于高效递归,而 call-by-value 更有利于高效余递归。
Abstract Recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, corecursion is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a foundation for primitive corecursion based on computation, giving a terminating calculus analogous to the original computational foundation of recursion. We show how the implementation details in an abstract machine strengthens their connection, syntactically deriving corecursion from recursion via logical duality. We also observe the impact of evaluation strategy on the computational complexity of primitive (co)recursive combinators: call-by-name allows for more efficient recursion, but call-by-value allows for more efficient corecursion.