In
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, coinduction is a technique for defining and proving properties of systems of
concurrent interacting
objects.
Coinduction is the
mathematic
Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
al
dual to
structural induction. Coinductively defined
data type
In computer science and computer programming, a data type (or simply type) is a collection or grouping of data values, usually specified by a set of possible values, a set of allowed operations on these values, and/or a representation of these ...
s are known as codata and are typically
infinite data structures
In computer science, a data structure is a data organization 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, and the functi ...
, 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 stream ...
.
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 specificati ...
, coinduction describes how an object may be "observed", "broken down" or "destructed" into simpler objects. As a
proof
Proof most often refers to:
* Proof (truth), argument or sufficient evidence for the truth of a proposition
* Alcohol proof, a measure of an alcoholic drink's strength
Proof may also refer to:
Mathematics and formal logic
* Formal proof, a co ...
technique, it may be used to show that an equation is satisfied by all possible
implementation
Implementation is the realization of an application, execution of a plan, idea, scientific modelling, model, design, specification, Standardization, standard, algorithm, policy, or the Management, administration or management of a process or Goal ...
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 (computer science), expression until its value is needed (non-strict evaluation) and which avoids repeated eva ...
. 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
Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
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 the language
Logtalk (for examples see ) and
SWI-Prolog.
Description
In his book ''Types and Programming Languages'',
Benjamin C. Pierce gives a concise statement 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 that yields the consequences of
. Then
is ''F-closed'' when one cannot conclude anymore than has already been asserted, while
is ''F-consistent'' when all of the 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 that
is known to be a member of.
Examples
Defining a set of data types
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 (possibly infinite) 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:
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:
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 call ...
, i.e. functions from
. Intuitively, the argument is similar to the argument that
(see
Repeating decimal
A repeating decimal or recurring decimal is a decimal representation of a number whose digits are eventually periodic (that is, after some place, the same sequence of digits is repeated forever); if this sequence consists only of zeros (that i ...
).
Coinductive datatypes in programming languages
Consider the following definition of a
stream
A stream is a continuous body of water, body of surface water Current (stream), flowing within the stream bed, bed and bank (geography), banks of a channel (geography), channel. Depending on its location or certain characteristics, a strea ...
:
data Stream a = S a (Stream a)
-- Stream "destructors"
head :: Stream a -> a
head (S a astream) = a
tail :: Stream a -> Stream 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 the
category of sets
In the mathematical field of category theory, the category of sets, denoted by Set, is the category whose objects are sets. The arrows or morphisms between sets ''A'' and ''B'' are the functions from ''A'' to ''B'', and the composition of mor ...
:
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 witnesses the isomorphism
, which in categorical terms indicates that
is a fixed point 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
We will demonstrate how the ''principle of induction'' subsumes mathematical induction.
Let
be some property of
natural numbers
In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positiv ...
. 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 (category theory), dual to recursion (computer science), recursion. Whereas recursion works analysis, analytically, starting on data further from a base case and breaking it dow ...
*
Bisimulation
*
Anamorphism
*
Total functional programming
References
Further reading
;Textbooks
*
Davide Sangiorgi (2012). ''Introduction to Bisimulation and Coinduction''. Cambridge University Press.
*
Davide Sangiorgi and
Jan Rutten (2011). ''Advanced Topics in Bisimulation and Coinduction''. Cambridge University Press.
;Introductory texts
*
Andrew D. Gordon
Andrew D. Gordon is a British computer scientist employed by software synthesis company Cogna as Chief Science Officer, and by the University of Cambridge. Formerly, he worked for Microsoft Research. His research interests include programming l ...
(1994). {{cite CiteSeerX , citeseerx = 10.1.1.37.3914 , title = A Tutorial on Co-induction and Functional Programming , year = 1994 , pages = 78–95 — mathematically oriented description
*
Bart Jacobs and
Jan Rutten (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