Classical (Co)Recursion: Mechanics

TL;DR

This paper develops a computational foundation for primitive corecursion, establishing a duality with recursion, and analyzes how evaluation strategies affect their computational complexity.

Contribution

It provides a terminating calculus for primitive corecursion, syntactically derives corecursion from recursion through logical duality, and examines evaluation strategy impacts.

Findings

Call-by-name enables more efficient recursion.

Call-by-value favors more efficient corecursion.

A new foundation for primitive corecursion is established.

Abstract

Primitive recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, primitive 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.