HOME

TheInfoList



OR:

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 U be a set and F 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 ...
2^U \rightarrow 2^U, that is: : X \subseteq Y \Rightarrow F(X) \subseteq F(Y) Unless otherwise stated, F will be assumed to be monotone. : X is ''F-closed'' if F(X) \subseteq X : X is ''F-consistent'' if X \subseteq F(X) : X is a fixed point if X = F(X) These terms can be intuitively understood in the following way. Suppose that X is a set of assertions, and F(X) is the operation which takes the implications of X. Then X is ''F-closed'' when you cannot conclude anymore than you've already asserted, while X 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 F (denoted \mu F) is given by the intersection of all ''F-closed'' sets, while the ''greatest fixed-point'' (denoted \nu F) 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 X is ''F-closed'', then \mu F \subseteq X : ''Principle of coinduction'': If X is ''F-consistent'', then X \subseteq \nu F


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 \mu F. By the ''principle of induction'', it suffices to exhibit an ''F-closed'' set X for which the property holds. Dually, suppose you wish to show that x \in \nu F. Then it suffices to exhibit an ''F-consistent'' set which x is known to be a member of.


Examples


Defining a set of datatypes

Consider the following grammar of datatypes: : T = \bot \;, \;\top \;, \; T \times T That is, the set of types includes the "bottom type" \bot, the "top type" \top, and (non-homogenous) lists. These types can be identified with strings over the alphabet \Sigma = \. Let \Sigma^* denote all strings over \Sigma. Consider the function F: 2^ \rightarrow 2^: : F(X) = \ \cup \ In this context, x \times y means "the concatenation of string x, the symbol \times, and string y." We should now define our set of datatypes as a fixpoint of F, but it matters whether we take the ''least'' or ''greatest'' fixpoint. Suppose we take \mu F as our set of datatypes. Using the ''principle of induction'', we can prove the following claim: : All datatypes in \mu F are ''finite'' To arrive at this conclusion, consider the set of all finite strings over \Sigma. Clearly F cannot produce an infinite string, so it turns out this set is ''F-closed'' and the conclusion follows. Now suppose that we take \nu F as our set of datatypes. We would like to use the ''principle of coinduction'' to prove the following claim: : The type \bot \times \bot \times ... \in \nu F Here \bot \times \bot \times ... denotes the infinite list consisting of all \bot. To use the ''principle of coinduction'', consider the set: : \ This set turns out to be ''F-consistent'', and therefore \bot \times \bot \times ... \in \nu F . This depends on the suspicious statement that : \bot \times \bot \times ... = \bot \times \bot \times ... \times \bot \times \bot \times ... 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 \mathbb \rightarrow \Sigma. Intuitively, the argument is similar to the argument that 0.\bar1 = 0 (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 ...
F 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 ...
: : F(x) = A \times x : F(f) = \langle id_A, f \rangle The ''final F-coalgebra'' \nu F has the following morphism associated with it: : \mathrm: \nu F \rightarrow F(\nu F) = A \times \nu F This induces another coalgebra F(\nu F) with associated morphism F(\mathrm). Because \nu F is ''final'', there is a unique morphism : \overline: F(\nu F) \rightarrow \nu F such that : \mathrm \circ \overline = F(\overline) \circ F(\mathrm) = F(\overline) \circ \mathrm) The composition \overline \circ \mathrm induces another F-coalgebra homomorphism \nu F \rightarrow \nu F. Since \nu F is final, this homomorphism is unique and therefore \mathrm_. Altogether we have: : \overline \circ \mathrm = \mathrm_ : \mathrm \circ \overline = F(\overline) \circ \mathrm) = \mathrm_ This witness the isomorphism \nu F \simeq F(\nu F), which in categorical terms indicates that \nu F is a fixpoint of F and justifies the notation.


Stream as a final coalgebra

We will show that
Stream A
is the final coalgebra of the functor F(x) = A \times x. 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 P 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: : P(0) \and (P(n) \Rightarrow P(n+1)) \Rightarrow P(\mathbb) Now consider the function F: 2^ \rightarrow 2^: : F(X) = \ \cup \ It should not be difficult to see that \mu F = \mathbb. Therefore, by the ''principle of induction'', if we wish to prove some property P of \mathbb, it suffices to show that P is ''F-closed''. In detail, we require: : F(P) \subseteq P That is, : \ \cup \ \subseteq P 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