Classical (co)recursion: Mechanics

DOI10.1017/S0956796822000168arXiv2103.08521OpenAlexW3152464979MaRDI QIDQ6132720FDOQ6132720

Authors: Paul Downen, Zena M. Ariola 

Publication date: 14 July 2023

Published in: Journal of Functional Programming (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2103.08521

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• CoCaml: functional programming with regular coinductive types
• Untersuchungen über das logische Schliessen. I
• Title not available (Why is that?)
• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• Practical foundations for programming languages
• Introduction to bisimulation and coinduction
• The duality of computation
• A call-by-name lambda-calculus machine
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• Paramorphisms
• Data structures and program transformation
• Call-by-value is dual to call-by-name
• Strong categorical datatypes II: A term logic for categorical programming
• Title not available (Why is that?)
• Abstracting models of strong normalization for classical calculi
• On a hitherto unexploited extension of the finitary standpoint
• The duality of classical intersection and union types
• Functional programming with apomorphisms (corecursion)
• Copatterns, programming infinite structures by observations
• Flexible coinductive logic programming
• Structures for structural recursion
• Wellfounded recursion with copatterns: a unified approach to termination and productivity
• Title not available (Why is that?)
• Unifying structured recursion schemes
• Title not available (Why is that?)

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)