Classical (co)recursion: Mechanics
From MaRDI portal
Publication:6132720
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.
Cites work
- scientific article; zbMATH DE number 7037626 (Why is no real title available?)
- scientific article; zbMATH DE number 4047683 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- scientific article; zbMATH DE number 7533346 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- A call-by-name lambda-calculus machine
- A lattice-theoretical fixpoint theorem and its applications
- Abstracting models of strong normalization for classical calculi
- Automatic synthesis of typed -programs on term algebras
- Call-by-value is dual to call-by-name
- CoCaml: functional programming with regular coinductive types
- Copatterns, programming infinite structures by observations
- Data structures and program transformation
- Flexible coinductive logic programming
- Functional programming with apomorphisms (corecursion)
- Introduction to bisimulation and coinduction
- Linear logic
- On a hitherto unexploited extension of the finitary standpoint
- Paramorphisms
- Practical foundations for programming languages
- Strong categorical datatypes II: A term logic for categorical programming
- Structures for structural recursion
- The duality of classical intersection and union types
- The duality of computation
- Unifying structured recursion schemes
- Untersuchungen über das logische Schliessen. I
- Wellfounded recursion with copatterns: a unified approach to termination and productivity
This page was built for publication: Classical (co)recursion: Mechanics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6132720)
