Coinduction

(Redirected from Coinductive)

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.

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."[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.

Description

edit

In [4] 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

edit

Let   be a set and   be a monotone function  , 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 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

edit
Principle of induction: If   is F-closed, then  
Principle of coinduction: If   is F-consistent, then  

Discussion

edit

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

edit

Defining a set of datatypes

edit

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:

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, i.e. functions from  . Intuitively, the argument is similar to the argument that   (see Repeating decimal).

Coinductive datatypes in programming languages

edit

Consider the following definition of a stream:[5]

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

edit

Source:[6]

Consider the endofunctor   in the category of sets:

 
 

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 fixpoint of   and justifies the notation.

Stream as a final coalgebra

edit

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.

We will demonstrate how the principle of induction subsumes mathematical induction. Let   be some property of natural numbers. 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

edit

References

edit
  1. ^ "Co-Logic Programming | Lambda the Ultimate".
  2. ^ "Gopal Gupta's Home Page".
  3. ^ "Logtalk3/Examples/Coinduction at master · LogtalkDotOrg/Logtalk3". GitHub.
  4. ^ Benjamin C. Pierce. "Types and Programming Languages". The MIT Press.
  5. ^ Dexter Kozen, Alexandra Silva. "Practical Coinduction". CiteSeerX 10.1.1.252.3961.
  6. ^ Ralf Hinze (2012). "Generic Programming with Adjunctions". Generic and Indexed Programming. Lecture Notes in Computer Science. Vol. 7470. Springer. pp. 47–129. doi:10.1007/978-3-642-32202-0_2. ISBN 978-3-642-32201-3.

Further reading

edit
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
History
Miscellaneous