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.
[citation needed] Coinductively defined data types are known as codata and are typically infinite data structures, such as streams.
As a definition or specification, coinduction describes how an object may be "observed", "broken down" or "destructed" into simpler objects.
As a proof technique, it may be used to show that an equation is satisfied by all possible implementations of such a specification.
To generate and manipulate codata, one typically uses corecursive functions, in conjunction with lazy evaluation.
Informally, rather than defining a function by pattern-matching on each of the inductive constructors, one defines each of the "destructors" or "observers" over the function result.
Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation, concurrent logic programming, model checking, bisimilarity proofs, etc.
"[1] Experimental implementations of co-LP are available from the University of Texas at Dallas[2] and in the language Logtalk (for examples see [3]) and SWI-Prolog.
While this article is not primarily concerned with induction, it is useful to consider their somewhat generalized forms at once.
In order to state the principles, a few preliminaries are required.
is F-closed when you cannot conclude anymore than you've already asserted, while
) is given by the intersection of all F-closed sets, while the greatest fixed-point (denoted
We can now state the principles of induction and coinduction.
The principles, as stated, are somewhat opaque, but can be usefully thought of in the following way.
By the principle of induction, it suffices to exhibit an F-closed set
Then it suffices to exhibit an F-consistent set that
These types can be identified with strings over the alphabet
denote all (possibly infinite) strings over
We should now define our set of datatypes as a fixpoint of
Using the principle of induction, we can prove the following claim: To arrive at this conclusion, consider the set of all finite strings over
cannot produce an infinite string, so it turns out this set is F-closed and the conclusion follows.
We would like to use the principle of coinduction to prove the following claim: Here
denotes the infinite list consisting of all
This depends on the suspicious statement that The formal justification of this is technical and depends on interpreting strings as sequences, i.e. functions from
in the category of sets: The final F-coalgebra
is final, there is a unique morphism such that The composition
We will show that is the final coalgebra of the functor
Consider the following implementations: These are easily seen to be mutually inverse, witnessing the isomorphism.
In detail, we require: That is, This is precisely mathematical induction as stated.