Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
In category theory, a branch of mathematics, duality is a correspondence between properties of a category C and so-called dual properties of the opposite category Cop...
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
. Corecursion and codata allow total languages to work with infinite data structures such as stream
Stream (type theory)
In type theory and functional programming, a stream is an infinite list given by the inductive definition:data Stream a = Cons a...
s. Corecursion is often used in conjunction with lazy evaluation
Lazy evaluation
In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...
. Corecursion can produce both finite and infinite data structures as result, and may employ self-referential
Self-reference
Self-reference occurs in natural or formal languages when a sentence or formula refers to itself. The reference may be expressed either directly—through some intermediate sentence or formula—or by means of some encoding...
data structures. Put simply, it is about algorithms using the data which they themselves produce, bit by bit, as they become available, and needed, to produce further bits of data.
Definition
Initial data types can be defined as being the least fixpoint (up to isomorphism) of some type equation; the isomorphism
Isomorphism
In abstract algebra, an isomorphism is a mapping between objects that shows a relationship between two properties or operations. If there exists an isomorphism between two structures, the two structures are said to be isomorphic. In a certain sense, isomorphic structures are...
In mathematics, an initial algebra is an initial object in the category of F-algebras for a given endofunctor F. The initiality provides a general framework for induction and recursion....
In mathematics, specifically in category theory, an F-algebra is a structure defined according to a functor F. F-algebras can be used to represent data structures used in programming, such as lists and trees...
. Dually, final (or terminal) data types can be defined as being the greatest fixpoint of a type equation; the isomorphism is then given by a final algebra.
In the mathematical field of category theory, the category of sets, denoted as Set, is the category whose objects are sets. The arrows or morphisms between sets A and B are all functions from A to B...
and total functions, then final data types may contain infinite, non-wellfounded
Non-well-founded set theory
Non-well-founded set theories are variants of axiomatic set theory which allow sets to contain themselves and otherwise violate the rule of well-foundedness...
values, whereas initial types do not. On the other hand, if the domain of discourse is the category of complete partial order
Complete partial order
In mathematics, directed complete partial orders and ω-complete partial orders are special classes of partially ordered sets, characterized by particular completeness properties...
In mathematics, given two partially ordered sets P and Q a function f : P \rightarrow Q between them is Scott-continuous if it preserves all directed suprema, i.e...
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
programming language, then final types coincide with initial types, and the corresponding final and initial algebras form an isomorphism.
Corecursion is then a technique for recursively defining functions whose range (codomain) is a final data type, dual to the way that ordinary recursion
Recursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
recursively defines functions whose domain is an initial data type.
The discussion below provides several examples in Haskell that distinguish corecursion. Roughly speaking, if one were to port these definitions to the category of sets, they would still be corecursive. This informal usage is consistent with existing textbooks about Haskell. Also note that the examples used in this article predate the attempts to define corecursion and explain what it is.
Discussion
The rule for primitive corecursion on codata is the dual to that for primitive recursion on data. Instead of descending on the argument by pattern-matching on its constructors (that were called up before, somewhere, so we receive a ready-made datum and get at its constituent sub-parts, i.e. "fields"), we ascend on the result by filling-in its "destructors" (or "observers", that will be called afterwards, somewhere - so we're actually calling a constructor, creating another bit of the result to be observed later on). Thus corecursion creates (potentially infinite) codata, whereas ordinary recursion analyses (necessarily finite) data. Ordinary recursion might not be applicable to the codata because it might not terminate. Conversely, corecursion is not strictly necessary if the result type is data, because data must be finite.
Here is an example in Haskell. The following definition produces the list of Fibonacci numbers in linear time:
fibs = 0 : 1 : next fibs
where
next (a: t@(b:_)) = (a+b):next t
This infinite list depends on lazy evaluation; elements are computed on an as-needed basis, and only finite prefixes are ever explicitly represented in memory. This feature allows algorithms on parts of codata to terminate; such techniques are an important part of Haskell programming.
This example employs a self-referential data structure. Ordinary recursion makes use of self-referential functions, but does not accommodate self-referential data. However, this is not essential to the Fibonacci example. It can be rewritten as follows:
This employs only self-referential function to construct the result. If it were used with strict list constructor it would be an example of runaway recursion, but with non-strict
Lazy evaluation
In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...
list constructor it (corecursively) produces an indefinitely defined list.
This shows how it can be done in Python:
from itertools import tee, chain, islice, imap
def add(x,y): return (x + y)
def fibonacci:
def deferred_output:
for i in output:
yield i
result, c1, c2 = tee(deferred_output, 3)
paired = imap(add, c1, islice(c2, 1, None))
output = chain([0, 1], paired)
return result
for i in islice(fibonacci,20):
print i
Corecursion need not produce an infinite object; a corecursive queue is a particularly good example of this phenomenon. The following definition produces a breadth-first traversal
Breadth-first search
In graph theory, breadth-first search is a graph search algorithm that begins at the root node and explores all the neighboring nodes...
of a binary tree in linear time:
data Tree a b = Leaf a | Branch b (Tree a b) (Tree a b)
bftrav :: Tree a b -> [Tree a b]
bftrav tree = queue
where
queue = tree : trav 1 queue
trav 0 q = []
trav len (Leaf _ : q) = trav (len-1) q
trav len (Branch _ l r : q) = l : r : trav (len+1) q
This definition takes an initial tree and produces list of subtrees. This list serves a dual purpose as both the queue and the result. 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. Even if the result is finite, this example depends on lazy evaluation due to the use of self-referential data structures.
Another particularly good example gives a solution to the problem of breadth-first labelling. 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) = label' t (1:ns)
label' :: Tree a b -> [Int] -> (Tree Int Int, [Int])
label' (Leaf _ ) (n:ns) = (Leaf n , n+1 : ns )
label' (Branch _ l r) (n:ns) = (Branch n l' r' , n+1 : ns)
where
(l',ns' ) = label' l ns
(r',ns) = label' r ns'
An apomorphism is the categorical dual of a paramorphism and an extension of the concept of anamorphism...
is a form of corecursion in the same way that a paramorphism
Paramorphism
A paramorphism is an extension of the concept of catamorphism to deal with a form which “eats its argument and keeps it too”, as exemplified by the factorial function. Its categorical dual is the apomorphism...
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
proof assistant supports corecursion and coinduction
Coinduction
In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects.Coinduction is the mathematical dual to structural induction...
using the CoFixpoint command.
The source of this article is wikipedia, the free encyclopedia. The text of this article is licensed under the GFDL.
