Coinduction
From Wikipedia, the free encyclopedia
In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects. Mathematically, it is dual to structural induction.
As a definition or specification, coinduction describes how an object may be broken down 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.
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." [1]
[edit] References
- Coinduction -- short introduction
- A Tutorial on Co-induction and Functional Programming -- mathematically oriented description
- A Tutorial on (Co)Algebras and (Co)Induction -- describes induction and coinduction simultaneously
- Co-Logic Programming: Extending Logic Programming with Coinduction -- describes the co-logic programming paradigm
