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

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

See also

• Corecursion
• Bisimulation