Coinduction
Encyclopedia
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
. Coinductively defined 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, the co-logic paradigm (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 LP, model checking, bisimilarity proofs, etc." Experimental implementations of Co-LP are available from U.T.Dallas and in Logtalk
(for examples see ) and SWI-Prolog
.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects.
Coinduction is the mathematical dual
Dual (category theory)
In category theory, a branch of mathematics, duality is a correspondence between properties of a category C and so-called dual properties of the opposite category Cop...
to structural induction
Structural induction
Structural induction is a proof method that is used in mathematical logic , computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction...
. Coinductively defined types are known as codata and are typically infinite data structures, such as streams
Stream (type theory)
In type theory and functional programming, a stream is an infinite list given by the inductive definition:data Stream a = Cons a...
.
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
Corecursion
In computer science, corecursion is a type of operation that is dual to recursion. Corecursion and codata allow total languages to work with infinite data structures such as streams. Corecursion is often used in conjunction with lazy evaluation. Corecursion can produce both finite and infinite data...
functions, in conjunction with lazy evaluation
Lazy evaluation
In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...
. 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, the co-logic paradigm (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 LP, model checking, bisimilarity proofs, etc." Experimental implementations of Co-LP are available from U.T.Dallas and in Logtalk
Logtalk
Logtalk is an object-oriented logic programming language that extends the Prolog language with a feature set suitable for programming in the large. It provides support for encapsulation and data hiding, separation of concerns and enhanced code reuse...
(for examples see ) and SWI-Prolog
SWI-Prolog
SWI-Prolog is an open source implementation of the programming language Prolog, commonly used for teaching and semantic web applications.It has a rich set of features, libraries forconstraint logic programming,multithreading,unit testing,GUI,...
.
See also
- F-coalgebraF-coalgebraIn mathematics, specifically in category theory, an F-coalgebra is a structure defined according to a functor F. For both algebra and coalgebra, a functor is a convenient and general way of organizing a signature...
- CorecursionCorecursionIn computer science, corecursion is a type of operation that is dual to recursion. Corecursion and codata allow total languages to work with infinite data structures such as streams. Corecursion is often used in conjunction with lazy evaluation. Corecursion can produce both finite and infinite data...
- BisimulationBisimulationIn theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
- AnamorphismAnamorphismAnamorphosis is a distorted projection or perspective requiring the viewer to use special devices or occupy a specific vantage point to reconstitute the image...
- Total functional programmingTotal functional programmingTotal functional programming is a programming paradigm that restricts the range of programs to those that are provably terminating....
Further reading
- Davide SangiorgiDavide SangiorgiDavide Sangiorgi is professor of computer science at the University of Bologna. He is the chairman of IFIP Working Group 2.2 on the formal description of programming concepts.- Selected publications :...
. "On the Origins of Bisimulation and Coinduction". - Coinduction — short introduction
- A Tutorial on Co-induction and Functional Programming — mathematically oriented description
- A Tutorial on (Co)Algebras and (Co)Induction (alternate link) — describes induction and coinduction simultaneously
- Co-Logic Programming: Extending Logic Programming with Coinduction — describes the co-logic programming paradigm