Coinduction

This article has multiple issues. Please help or discuss these issues on the talk page. (Learn how and when to remove these template messages) This article may be too technical for most readers to understand. Please to make it understandable to non-experts, without removing the technical details. (October 2011) (Learn how and when to remove this template message) This article relies too much on references to primary sources. Please improve this by adding secondary or tertiary sources. (November 2019) (Learn how and when to remove this template message) (Learn how and when to remove this template message)

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, 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 Logtalk (for examples see ^[3]) and SWI-Prolog.

See also[]

• F-coalgebra
• Corecursion
• Bisimulation
• Anamorphism
• Total functional programming

References[]

Further reading[]

Textbooks

• Davide Sangiorgi (2012). Introduction to Bisimulation and Coinduction. Cambridge University Press.
• Davide Sangiorgi and (2011). Advanced Topics in Bisimulation and Coinduction. Cambridge University Press.

Introductory texts

• Andrew D. Gordon (1994). "A Tutorial on Co-induction and Functional Programming". 1994: 78–95. CiteSeerX 10.1.1.37.3914. Cite journal requires |journal= (help) — mathematically oriented description
• and (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

History

• Davide Sangiorgi. "On the Origins of Bisimulation and Coinduction", ACM Transactions on Programming Languages and Systems, Vol. 31, Nb 4, Mai 2009.

Miscellaneous

• Co-Logic Programming: Extending Logic Programming with Coinduction — describes the co-logic programming paradigm