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.
- Text books
- 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 (1994). "A Tutorial on Co-induction and Functional Programming". CiteSeerX: 10
.1 .1 .37 .3914. — mathematically oriented description
- Bart Jacobs and Jan Rutten (1997). A Tutorial on (Co)Algebras and (Co)Induction (alternate link) — describes induction and coinduction simultaneously
- Eduardo Giménez and Pierre Castéran (2007). "A Tutorial on [Co-]Inductive Types in Coq"
- Coinduction — short introduction
- Co-Logic Programming: Extending Logic Programming with Coinduction — describes the co-logic programming paradigm
|P ≟ NP||This theoretical computer science–related article is a stub. You can help Wikipedia by expanding it.|