queue). It is finite if and only if the initial tree is finite. The length of the queue must be explicitly tracked in order to ensure termination; this can safely be elided if this definition is applied only to infinite trees. Another particularly good example gives a solution to the problem of breadth-first labeling. The function label visits every node in a binary tree in a breadth first fashion, and replaces each label with an integer, each subsequent integer is bigger than the last by one. This solution employs a self-referential data structure, and the binary tree can be finite or infinite. label :: Tree a b -> Tree Int Int label t = t′ where (t′, ns) = go t (1:ns) go :: Tree a b -> [Int] -> (Tree Int Int, [Int]) go (Leaf _ ) (n:ns) = (Leaf n , n+1 : ns ) go (Branch _ l r) (n:ns) = (Branch n l′ r′ , n+1 : ns′′) where (l′, ns′ ) = go l ns (r′, ns′′) = go r ns′ An apomorphism (such as an anamorphism, such as unfold) is a form of corecursion in the same way that a paramorphism (such as a catamorphism, such as fold) is a form of recursion. The Coq proof assistant supports corecursion and coinduction using the CoFixpoint command. History Corecursion, referred to as circular programming, dates at least to , who credits John Hughes and Philip Wadler; more general forms were developed in . The original motivations included producing more efficient algorithms (allowing 1 pass over data in some cases, instead of requiring multiple passes) and implementing classical data structures, such as doubly linked lists and queues, in functional languages. See also Bisimulation Coinduction Recursion Anamorphism Notes References Theoretical computer science Self-reference Articles with example Haskell code Articles with example Python (programming language) code Functional programming Category theory Recursion