Induction and Co-induction
These are contrasting terms for ways of describing a system. An inductive definition begins with some kernel or primitive types of objects, and uses constructive operations on these to iteratively define a whole group of things based on those primitives. Datatypes such as lists, sets, records, and natural numbers all can be described this way (see algebra and coalgebra).By contrast, there are datatypes such as streams, graphs (including things that graphs describe, such as state machines), and the rational numbers, which elements can only be described in relation to each other, rather than to some core types. (Although there are obviously ways to implement these types in terms of other types, this is not the same as a definition.) Objects such as these without a well-founded means of deriving a definition have to be treated with a more general kind of logic, one that does not rely strictly on recursion, but may look for self-consistency instead.
Formally, the induction and principle is defined as follows. An algebra is said to be minimal when it has no proper (i.e., different from itself) subalgebra. This is the induction principle for the algebra. For instance, natural numbers with zero (0) and successors (')form a minimal algebra of the functor 1 + _: then, any subalgebra (i.e., any subset of the naturals which is closed w.r.t. zero and successor) is the whole algebra of natural numbers. This yields the familiar proof by induction for naturals, when to prove that a property holds for all the naturals you just prove that holds for zero and that, if it holds on x, then it holds on its successor x'.
The coinduction principle is defined dually. A coalgebra is said to be simple when it has no proper quotients. This is the coinduction principle for the coalgebra, but usually its practical and equivalent formulation is: when two distinct states are not bisimilar.
The induction and coinduction principle for initial and final can be also used to define functions. Initial algebras allow the exploitment of the induction principle to define functions from its carrier to the carrier of another algebra. Dually, final coalgebras allow the exploitment of the coinduction principle to define function from the carrier of another algebra to its carrier. If, for instance, we have an initial algebra O with signature F and carrier A, every function f: A→B which is also a homomorphism from the initial algebra to some F-algebra P is univocally defined. Dually for coinductive definitions of functions. An inductive definition has a typical flavour, where the effect of f on the constructors of I is defined in terms of the arguments of the constructors applied to f, where P has the role of defining the equational constraints which univocally determine f. Dually, a coinductive definition has a typical flavour, where the effect of the destructors of the final coalgebra I on an application of f is defined in terms of the arguments of this application applied in some way to fwhere P (the other coalgebra) defines the equational constraints which univocally determine f. For instance the inductive definition of the length of a list:
len(empty) = 0
len(l1 # l2) = len(l1) + len(l2)
and the coinductive definition of the "zipping" function which takes two streams and merges them by full shuffle:
head(zip(s1,s2)) = head(s1)
tail(zip(s1,s2)) = zip(s2,tail(s1))
In the first case, on the LHS we have the function on the outside, and on the RHS the function is "pushed inside", while on the outside the operators of P appear. In the second case, on the LHS we have the destructors on the outside, and on the RHS these destructors are "pushed inside", while on the outside some expression on f appears.
To edit this page see HTML special characters and symbols.
This page is linked from: Algebra and coalgebra Coinduction 101 Duality Initiality and finality Lemon Morphism