In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
, coinduction is a technique for defining and proving properties of systems of concurrent interacting
objects.
Coinduction is the
mathematic
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
al
dual to
structural induction Structural induction is a proof method that is used in mathematical logic (e.g., in the proof of Łoś' theorem), computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction over natural n ...
. Coinductively defined types are known as codata and are typically
infinite
Infinite may refer to:
Mathematics
*Infinite set, a set that is not a finite set
*Infinity, an abstract concept describing something without any limit
Music
*Infinite (group)
Infinite ( ko, 인피니트; stylized as INFINITE) is a South Ko ...
data structures
In computer science, a data structure is a data organization, management, and storage format that is usually chosen for efficient access to data. More precisely, a data structure is a collection of data values, the relationships among them, a ...
, such as
streams
A stream is a continuous body of surface water flowing within the bed and banks of a channel. Depending on its location or certain characteristics, a stream may be referred to by a variety of local or regional names. Long large streams ...
.
As a definition or
specification
A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard.
There are different types of technical or engineering specificat ...
, 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
implementation
Implementation is the realization of an application, or execution of a plan, idea, model, design, specification, standard, algorithm, or policy.
Industry-specific definitions
Computer science
In computer science, an implementation is a real ...
s of such a specification.
To generate and manipulate codata, one typically uses
corecursive functions, in conjunction with
lazy evaluation
In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an expression until its value is needed ( non-strict evaluation) and which also avoids repeated evaluations ( sharing).
T ...
. 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.
In programming, co-logic programming (co-LP for brevity) "is a natural generalization of logic programming and coinductive logic programming, which in turn generalizes other extensions of logic programming, such as infinite trees, lazy predicates, and concurrent communicating predicates. Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation, concurrent logic programming, model checking,
bisimilarity proofs, etc." Experimental implementations of co-LP are available from
The University of Texas at Dallas and in
Logtalk (for examples see ) and
SWI-Prolog.
Description
In a concise statement is given of both the ''principle of induction'' and the ''principle of coinduction''. 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.
Preliminaries
Let
be a set and
be a
monotone function
In mathematics, a monotonic function (or monotone function) is a function between ordered sets that preserves or reverses the given order. This concept first arose in calculus, and was later generalized to the more abstract setting of ord ...
, that is:
:
Unless otherwise stated,
will be assumed to be monotone.
: X is ''F-closed'' if
: X is ''F-consistent'' if
: X is a
fixed point if
These terms can be intuitively understood in the following way. Suppose that
is a set of assertions, and
is the operation which takes the implications of
. Then
is ''F-closed'' when you cannot conclude anymore than you've already asserted, while
is ''F-consistent'' when all of your assertions are supported by other assertions (i.e. there are no "non-F-logical assumptions").
The
Knaster–Tarski theorem tells us that the ''least fixed-point'' of
(denoted
) is given by the intersection of all ''F-closed'' sets, while the ''greatest fixed-point'' (denoted
) is given by the union of all ''F-consistent'' sets. We can now state the principles of induction and coinduction.
Definition
: ''Principle of induction'': If
is ''F-closed'', then
: ''Principle of coinduction'': If
is ''F-consistent'', then
Discussion
The principles, as stated, are somewhat opaque, but can be usefully thought of in the following way. Suppose you wish to prove a property of
. By the ''principle of induction'', it suffices to exhibit an ''F-closed'' set
for which the property holds. Dually, suppose you wish to show that
. Then it suffices to exhibit an ''F-consistent'' set which
is known to be a member of.
Examples
Defining a set of datatypes
Consider the following grammar of datatypes:
:
That is, the set of types includes the "bottom type"
, the "top type"
, and (non-homogenous) lists. These types can be identified with strings over the alphabet
. Let
denote all strings over
. Consider the function
:
:
In this context,
means "the concatenation of string
, the symbol
, and string
." We should now define our set of datatypes as a fixpoint of
, but it matters whether we take the ''least'' or ''greatest'' fixpoint.
Suppose we take
as our set of datatypes. Using the ''principle of induction'', we can prove the following claim:
: All datatypes in
are ''finite''
To arrive at this conclusion, consider the set of all finite strings over
. Clearly
cannot produce an infinite string, so it turns out this set is ''F-closed'' and the conclusion follows.
Now suppose that we take
as our set of datatypes. We would like to use the ''principle of coinduction'' to prove the following claim:
: The type
Here
denotes the infinite list consisting of all
. To use the ''principle of coinduction'', consider the set:
:
This set turns out to be ''F-consistent'', and therefore
. This depends on the suspicious statement that
:
The formal justification of this is technical and depends on interpreting strings as
sequences
In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is called ...
, i.e. functions from
. Intuitively, the argument is similar to the argument that
(see
Repeating decimal
A repeating decimal or recurring decimal is decimal representation of a number whose digits are periodic (repeating its values at regular intervals) and the infinitely repeated portion is not zero. It can be shown that a number is rational i ...
).
Coinductive datatypes in programming languages
Consider the following definition of a
stream:
data Stream a = S a (Stream a)
-- Stream "destructors"
head (S a astream) = a
tail (S a astream) = astream
This would seem to be a definition that is
not well-founded, but it is nonetheless useful in programming and can be reasoned about. In any case, a stream is an infinite list of elements from which you may observe the first element, or place an element in front of to get another stream.
Relationship with F-coalgebras
Consider the
endofunctor
In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) are associated to topological spaces, an ...
in the
category of sets
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 the total functions from ''A'' to ''B'', and the composition ...
:
:
:
The ''final F-coalgebra''
has the following morphism associated with it:
:
This induces another coalgebra
with associated morphism
. Because
is ''final'', there is a unique morphism
:
such that
:
The composition
induces another F-coalgebra homomorphism
. Since
is final, this homomorphism is unique and therefore
. Altogether we have:
:
:
This witness the isomorphism
, which in categorical terms indicates that
is a fixpoint of
and justifies the notation.
Stream as a final coalgebra
We will show that
Stream A
is the final coalgebra of the functor
. Consider the following implementations:
out astream = (head astream, tail astream)
out' (a, astream) = S a astream
These are easily seen to be mutually inverse, witnessing the isomorphism. See the reference for more details.
Relationship with
Mathematical Induction
Mathematical induction is a method for proving that a statement ''P''(''n'') is true for every natural number ''n'', that is, that the infinitely many cases ''P''(0), ''P''(1), ''P''(2), ''P''(3), ... all hold. Informal metaphors help ...
We will demonstrate how the ''principle of induction'' subsumes mathematical induction.
Let
be some property of
Natural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called '' cardinal ...
. We will take the following definition of mathematical induction:
:
Now consider the function
:
:
It should not be difficult to see that
. Therefore, by the ''principle of induction'', if we wish to prove some property
of
, it suffices to show that
is ''F-closed''. In detail, we require:
:
That is,
:
This is precisely ''mathematical induction'' as stated.
See also
*
F-coalgebra
In mathematics, specifically in category theory, an F-coalgebra is a structure defined according to a functor F, with specific properties as defined below. For both algebras and coalgebras, a functor is a convenient and general way of organizin ...
*
Corecursion
In computer science, corecursion is a type of operation that is dual to recursion. Whereas recursion works analytically, starting on data further from a base case and breaking it down into smaller data and repeating until one reaches a base case, ...
*
Bisimulation
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa.
Intuitively two systems are bisimilar if ...
*
Anamorphism
*
Total functional programming
References
Further reading
;Textbooks
*
Davide Sangiorgi (2012). ''Introduction to Bisimulation and Coinduction''. Cambridge University Press.
*
Davide Sangiorgi and
Jan Rutten
Jan, JaN or JAN may refer to:
Acronyms
* Jackson, Mississippi (Amtrak station), US, Amtrak station code JAN
* Jackson-Evers International Airport, Mississippi, US, IATA code
* Jabhat al-Nusra (JaN), a Syrian militant group
* Japanese Article N ...
(2011). ''Advanced Topics in Bisimulation and Coinduction''. Cambridge University Press.
;Introductory texts
*
Andrew D. Gordon (1994). — mathematically oriented description
*
Bart Jacobs and
Jan Rutten
Jan, JaN or JAN may refer to:
Acronyms
* Jackson, Mississippi (Amtrak station), US, Amtrak station code JAN
* Jackson-Evers International Airport, Mississippi, US, IATA code
* Jabhat al-Nusra (JaN), a Syrian militant group
* Japanese Article N ...
(1997)
A Tutorial on (Co)Algebras and (Co)Inductionalternate link — describes induction and coinduction simultaneously
* Eduardo Giménez and Pierre Castéran (2007)
"A Tutorial on [Co-/nowiki>Inductive Types in Coq"">o-">"A Tutorial on
[Co-
/nowiki>Inductive Types in Coq"
Coinduction
— short introduction
;History
* Davide Sangiorgi.
On the Origins of Bisimulation and Coinduction
, ACM Transactions on Programming Languages and Systems, Vol. 31, Nb 4, Mai 2009.
;Miscellaneous
Co-Logic Programming: Extending Logic Programming with Coinduction
— describes the co-logic programming paradigm
Theoretical computer science
Logic programming
Functional programming
Category theory
Mathematical induction
{{comp-sci-theory-stub