nLab recursion scheme

Redirected from "recursion schemes".
Contents

Contents

 Idea

It is a well-known fact in computability that it is not possible to write a decision procedure that tells whether another program is terminating or not. This fact is known as the halting theorem.

For this reason most functional programming languages are endowed with an unrestricted fixed-point operator at all types, which simplifies the implementation of the language, but allows the user to write functions that are not-well defined mathematically.

Inspired by category theory, a recursion scheme is a structured recursion operator that ensures that the definitions of recursive functions are well-defined.

For example,

  1. A catamorphism (a.k.a. a fold) is the unique FF-algebra homomorphism from an initial algebra for the functor FF.

  2. An anamorphism? (a.k.a. unfold) is the unique GG-coalgebra homomorphism into the final coalgebra for the functor GG.

  3. An hylomorphism? corresponds to the idea of a recursive coalgebra or well-founded coalgebra. In words, a recursive FF-coalgebra (c,X)(c, X) has a unique mapping f:XYf : X \to Y into any other FF-algebra (Y,a)(Y, a) such that f=aF(f)cf = a \circ F(f) \circ c.

A hylomorphism gives a simple example of an opportunity for optimization: an anamorphism builds up a tree structure and a catamorphism consumes it, so if this hylomorphism structure is recognized in the program, then an implementation need not build the intermediate tree, and so the space usage of the program can be reduced.

Recursion Schemes via Adjunctions

Catamorphisms and their variants are basic and rather restricted forms of recursion, i.e. where the recursive call is called on smaller input.

Many other patterns of recursion exist that are equally well-defined, but they cannot be expressed directly in terms of catamorphisms. However, most recursion schemes are adjoint folds (Hinze, Wu and Gibbons, 2013), i.e. every complex recursion scheme can be reduced to a basic one via an adjunction. Moreover, every recursion scheme is an instance of a conjugate hylomorphism (Hinze, Wu and Gibbons, 2015) .

A comprehensive list of recursion schemes can be found in Yang and Wu, 2022

References

  • Erik Meijer, Maarten M. Fokkinga, Ross Paterson, Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, FPCA 1991, (doi)

  • Ralf Hinze, Nicolas Wu and Jeremy Gibbons, Unifying structured recursion schemes, ACM SIGPLAN International Conference on Functional Programming, ICFP’13, doi

  • Ralf Hinze, Nicolas Wu, _ Unifying structured recursion schemes - An Extended Study, J. Funct. Program., 2016, doi

  • Ralf Hinze, Nicolas Wu and Jeremy Gibbons, Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes, Symposium on Principles of Programming Languages, POPL 2015, doi

  • Zhixuan Yang and Nicolas Wu, Fantastic Morphisms and Where to Find Them - A Guide to Recursion Schemes, Mathematics of Program Construction, MPC 2022, doi

Last revised on August 22, 2024 at 16:44:34. See the history of this page for a list of all contributions to it.