Coinduction

<h2 id="description">Description</h2>
In his book Types and Programming Languages,<a class="footnote-ref" id="fnref:4" href="#fn:4">4</a> <a href="/facts/Benjamin_C._Pierce/m9DKUgML">Benjamin C. Pierce</a> gives a concise statement of both the principle of induction and the principle of coinduction. While this article is not primarily concerned with induction, it is useful to consider their somewhat generalized forms at once. In order to state the principles, a few preliminaries are required.

<h3>Preliminaries</h3>
Let 
 
 
 
 U
 
 
 {\displaystyle U}
 
 be a set and 
 
 
 
 F
 
 
 {\displaystyle F}
 
 be a <a href="/facts/Monotonic_function/MjQK0YL2">monotone function</a> 
 
 
 
 
 2
 
 U
 
 
 →
 
 2
 
 U
 
 
 
 
 {\displaystyle 2^{U}\rightarrow 2^{U}}
 
, that is:

 
 
 
 X
 ⊆
 Y
 ⇒
 F
 (
 X
 )
 ⊆
 F
 (
 Y
 )
 
 
 {\displaystyle X\subseteq Y\Rightarrow F(X)\subseteq F(Y)}

Unless otherwise stated, 
 
 
 
 F
 
 
 {\displaystyle F}
 
 will be assumed to be monotone.

<ul><li>X is F-closed if 
 
 
 
 F
 (
 X
 )
 ⊆
 X
 
 
 {\displaystyle F(X)\subseteq X}
 
</li>
<li>X is F-consistent if 
 
 
 
 X
 ⊆
 F
 (
 X
 )
 
 
 {\displaystyle X\subseteq F(X)}
 
</li>
<li>X is a <a href="/facts/Fixed_point_(mathematics)/vVVddTKc">fixed point</a> if 
 
 
 
 X
 =
 F
 (
 X
 )
 
 
 {\displaystyle X=F(X)}
 
</li></ul>
These terms can be intuitively understood in the following way. Suppose that 
 
 
 
 X
 
 
 {\displaystyle X}
 
 is a set of assertions, and 
 
 
 
 F
 (
 X
 )
 
 
 {\displaystyle F(X)}
 
 is the operation that yields the consequences of 
 
 
 
 X
 
 
 {\displaystyle X}
 
. Then 
 
 
 
 X
 
 
 {\displaystyle X}
 
 is F-closed when one cannot conclude anymore than has already been asserted, while 
 
 
 
 X
 
 
 {\displaystyle X}
 
 is F-consistent when all of the assertions are supported by other assertions (i.e. there are no "non-F-logical assumptions").
The <a href="/facts/Knaster%E2%80%93Tarski_theorem/QeXjysqQ">Knaster–Tarski theorem</a> tells us that the least fixed-point of 
 
 
 
 F
 
 
 {\displaystyle F}
 
 (denoted 
 
 
 
 μ
 F
 
 
 {\displaystyle \mu F}
 
) is given by the intersection of all F-closed sets, while the greatest fixed-point (denoted 
 
 
 
 ν
 F
 
 
 {\displaystyle \nu F}
 
) is given by the union of all F-consistent sets. We can now state the principles of induction and coinduction.

<h3>Definition</h3>
<ul><li>Principle of induction: If 
 
 
 
 X
 
 
 {\displaystyle X}
 
 is F-closed, then 
 
 
 
 μ
 F
 ⊆
 X
 
 
 {\displaystyle \mu F\subseteq X}
 
</li>
<li>Principle of coinduction: If 
 
 
 
 X
 
 
 {\displaystyle X}
 
 is F-consistent, then 
 
 
 
 X
 ⊆
 ν
 F
 
 
 {\displaystyle X\subseteq \nu F}
 
</li></ul>
<h2 id="discussion">Discussion</h2>
The principles, as stated, are somewhat opaque, but can be usefully thought of in the following way. Suppose you wish to prove a property of 
 
 
 
 μ
 F
 
 
 {\displaystyle \mu F}
 
. By the principle of induction, it suffices to exhibit an F-closed set 
 
 
 
 X
 
 
 {\displaystyle X}
 
 for which the property holds. Dually, suppose you wish to show that 
 
 
 
 x
 ∈
 ν
 F
 
 
 {\displaystyle x\in \nu F}
 
. Then it suffices to exhibit an F-consistent set that 
 
 
 
 x
 
 
 {\displaystyle x}
 
 is known to be a member of.

<h2 id="examples">Examples</h2>
<h3>Defining a set of data types</h3>
See also: <a href="/facts/Data_type/fcx5hgVL">Data type</a>
Consider the following grammar of datatypes:

 
 
 
 T
 =
 ⊥
 
 
 |
 
 
 ⊤
 
 
 |
 
 
 T
 ×
 T
 
 
 {\displaystyle T=\bot \;|\;\top \;|\;T\times T}

That is, the set of types includes the "bottom type" 
 
 
 
 ⊥
 
 
 {\displaystyle \bot }
 
, the "top type" 
 
 
 
 ⊤
 
 
 {\displaystyle \top }
 
, and (non-homogenous) lists. These types can be identified with strings over the alphabet 
 
 
 
 Σ
 =
 {
 ⊥
 ,
 ⊤
 ,
 ×
 }
 
 
 {\displaystyle \Sigma =\{\bot ,\top ,\times \}}
 
. Let 
 
 
 
 
 Σ
 
 ≤
 ω
 
 
 
 
 {\displaystyle \Sigma ^{\leq \omega }}
 
 denote all (possibly infinite) strings over 
 
 
 
 Σ
 
 
 {\displaystyle \Sigma }
 
. Consider the function 
 
 
 
 F
 :
 
 2
 
 
 Σ
 
 ≤
 ω
 
 
 
 
 →
 
 2
 
 
 Σ
 
 ≤
 ω
 
 
 
 
 
 
 {\displaystyle F:2^{\Sigma ^{\leq \omega }}\rightarrow 2^{\Sigma ^{\leq \omega }}}
 
:

 
 
 
 F
 (
 X
 )
 =
 {
 ⊥
 ,
 ⊤
 }
 ∪
 {
 x
 ×
 y
 :
 x
 ,
 y
 ∈
 X
 }
 
 
 {\displaystyle F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}}

In this context, 
 
 
 
 x
 ×
 y
 
 
 {\displaystyle x\times y}
 
 means "the concatenation of string 
 
 
 
 x
 
 
 {\displaystyle x}
 
, the symbol 
 
 
 
 ×
 
 
 {\displaystyle \times }
 
, and string 
 
 
 
 y
 
 
 {\displaystyle y}
 
." We should now define our set of datatypes as a fixpoint of 
 
 
 
 F
 
 
 {\displaystyle F}
 
, but it matters whether we take the least or greatest fixpoint.
Suppose we take 
 
 
 
 μ
 F
 
 
 {\displaystyle \mu F}
 
 as our set of datatypes. Using the principle of induction, we can prove the following claim:

 All datatypes in 
 
 
 
 μ
 F
 
 
 {\displaystyle \mu F}
 
 are finite
To arrive at this conclusion, consider the set of all finite strings over 
 
 
 
 Σ
 
 
 {\displaystyle \Sigma }
 
. Clearly 
 
 
 
 F
 
 
 {\displaystyle F}
 
 cannot produce an infinite string, so it turns out this set is F-closed and the conclusion follows.
Now suppose that we take 
 
 
 
 ν
 F
 
 
 {\displaystyle \nu F}
 
 as our set of datatypes. We would like to use the principle of coinduction to prove the following claim:

 The type 
 
 
 
 ⊥
 ×
 ⊥
 ×
 ⋯
 ∈
 ν
 F
 
 
 {\displaystyle \bot \times \bot \times \cdots \in \nu F}

Here 
 
 
 
 ⊥
 ×
 ⊥
 ×
 ⋯
 
 
 {\displaystyle \bot \times \bot \times \cdots }
 
 denotes the infinite list consisting of all 
 
 
 
 ⊥
 
 
 {\displaystyle \bot }
 
. To use the principle of coinduction, consider the set:

 
 
 
 {
 ⊥
 ×
 ⊥
 ×
 ⋯
 }
 
 
 {\displaystyle \{\bot \times \bot \times \cdots \}}

This set turns out to be F-consistent, and therefore 
 
 
 
 ⊥
 ×
 ⊥
 ×
 ⋯
 ∈
 ν
 F
 
 
 {\displaystyle \bot \times \bot \times \cdots \in \nu F}
 
. This depends on the suspicious statement that

 
 
 
 ⊥
 ×
 ⊥
 ×
 ⋯
 =
 (
 ⊥
 ×
 ⊥
 ×
 ⋯
 )
 ×
 (
 ⊥
 ×
 ⊥
 ×
 ⋯
 )
 
 
 {\displaystyle \bot \times \bot \times \cdots =(\bot \times \bot \times \cdots )\times (\bot \times \bot \times \cdots )}

The formal justification of this is technical and depends on interpreting strings as <a href="/facts/Sequence/gV2S4uqp">sequences</a>, i.e. functions from 
 
 
 
 
 N
 
 →
 Σ
 
 
 {\displaystyle \mathbb {N} \rightarrow \Sigma }
 
. Intuitively, the argument is similar to the argument that 
 
 
 
 0.
 
 
 
 0
 ¯
 
 
 
 1
 =
 0
 
 
 {\displaystyle 0.{\bar {0}}1=0}
 
 (see <a href="/facts/Repeating_decimal/yo5T4m2M">Repeating decimal</a>).

<h3>Coinductive datatypes in programming languages</h3>
Consider the following definition of a <a href="/facts/Stream_(computing)/2jtBAp0U">stream</a>:<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a>

data Stream a = S a (Stream a)

-- Stream "destructors"
head :: Stream a -> a
head (S a astream) = a
tail :: Stream a -> Stream a
tail (S a astream) = astream

This would seem to be a definition that is <a href="/facts/Non-well-founded_set_theory/RkmGMC70">not well-founded</a>, but it is nonetheless useful in programming and can be reasoned about. In any case, a stream is an infinite list of elements from which you may observe the first element, or place an element in front of to get another stream.

<h3>Relationship with F-coalgebras</h3>
Further information: <a href="/facts/F-coalgebra/VLE0yJjG">F-coalgebra</a>
Consider the <a href="/facts/Functor/l2u3rIBE">endofunctor</a> 
 
 
 
 F
 
 
 {\displaystyle F}
 
 in the <a href="/facts/Category_of_sets/LF5ykYl0">category of sets</a>:

 
 
 
 
 
 
 
 F
 (
 x
 )
 
 
 
 =
 A
 ×
 x
 
 
 
 
 F
 (
 f
 )
 
 
 
 =
 ⟨
 
 
 i
 d
 
 
 A
 
 
 ,
 f
 ⟩
 
 
 
 
 
 
 {\displaystyle {\begin{aligned}F(x)&=A\times x\\F(f)&=\langle \mathrm {id} _{A},f\rangle \end{aligned}}}

The final F-coalgebra 
 
 
 
 ν
 F
 
 
 {\displaystyle \nu F}
 
 has the following morphism associated with it:

 
 
 
 
 o
 u
 t
 
 :
 ν
 F
 →
 F
 (
 ν
 F
 )
 =
 A
 ×
 ν
 F
 
 
 {\displaystyle \mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F}

This induces another coalgebra 
 
 
 
 F
 (
 ν
 F
 )
 
 
 {\displaystyle F(\nu F)}
 
 with associated morphism 
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 
 {\displaystyle F(\mathrm {out} )}
 
. Because 
 
 
 
 ν
 F
 
 
 {\displaystyle \nu F}
 
 is final, there is a unique morphism

 
 
 
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 :
 F
 (
 ν
 F
 )
 →
 ν
 F
 
 
 {\displaystyle {\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F}

such that

 
 
 
 
 o
 u
 t
 
 ∘
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 =
 F
 
 (
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 )
 
 ∘
 F
 (
 
 o
 u
 t
 
 )
 =
 F
 
 (
 
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 ∘
 
 o
 u
 t
 
 
 )
 
 
 
 {\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)}

The composition 
 
 
 
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 ∘
 
 o
 u
 t
 
 
 
 {\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }
 
 induces another F-coalgebra homomorphism 
 
 
 
 ν
 F
 →
 ν
 F
 
 
 {\displaystyle \nu F\rightarrow \nu F}
 
. Since 
 
 
 
 ν
 F
 
 
 {\displaystyle \nu F}
 
 is final, this homomorphism is unique and therefore 
 
 
 
 
 
 i
 d
 
 
 ν
 F
 
 
 
 
 {\displaystyle \mathrm {id} _{\nu F}}
 
. Altogether we have:

 
 
 
 
 
 
 
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 ∘
 
 o
 u
 t
 
 
 
 
 =
 
 
 i
 d
 
 
 ν
 F
 
 
 
 
 
 
 
 o
 u
 t
 
 ∘
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 =
 F
 
 (
 
 
 
 F
 (
 
 o
 u
 t
 
 )
 
 ¯
 
 
 )
 
 ∘
 
 o
 u
 t
 
 )
 
 
 
 =
 
 
 i
 d
 
 
 F
 (
 ν
 F
 )
 
 
 
 
 
 
 
 
 {\displaystyle {\begin{aligned}{\overline {F(\mathrm {out} )}}\circ \mathrm {out} &=\mathrm {id} _{\nu F}\\\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )&=\mathrm {id} _{F(\nu F)}\end{aligned}}}

This witnesses the isomorphism 
 
 
 
 ν
 F
 ≃
 F
 (
 ν
 F
 )
 
 
 {\displaystyle \nu F\simeq F(\nu F)}
 
, which in categorical terms indicates that 
 
 
 
 ν
 F
 
 
 {\displaystyle \nu F}
 
 is a fixed point of 
 
 
 
 F
 
 
 {\displaystyle F}
 
 and justifies the notation.<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a>[verification needed]

<h4>Stream as a final coalgebra</h4>
We will show that Stream A is the final coalgebra of the functor 
 
 
 
 F
 (
 x
 )
 =
 A
 ×
 x
 
 
 {\displaystyle F(x)=A\times x}
 
. Consider the following implementations:

out astream = (head astream, tail astream)
out' (a, astream) = S a astream

These are easily seen to be mutually inverse, witnessing the isomorphism. See the reference for more details.

<h3>Relationship with mathematical induction</h3>
Further information: <a href="/facts/Mathematical_induction/KxAPqNrH">Mathematical induction</a>
We will demonstrate how the principle of induction subsumes mathematical induction.
Let 
 
 
 
 P
 
 
 {\displaystyle P}
 
 be some property of <a href="/facts/Natural_numbers/u65og8JE">natural numbers</a>. We will take the following definition of mathematical induction:

 
 
 
 0
 ∈
 P
 ∧
 (
 n
 ∈
 P
 ⇒
 n
 +
 1
 ∈
 P
 )
 ⇒
 P
 =
 
 N
 
 
 
 {\displaystyle 0\in P\land (n\in P\Rightarrow n+1\in P)\Rightarrow P=\mathbb {N} }

Now consider the function 
 
 
 
 F
 :
 
 2
 
 
 N
 
 
 
 →
 
 2
 
 
 N
 
 
 
 
 
 {\displaystyle F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }}
 
:

 
 
 
 F
 (
 X
 )
 =
 {
 0
 }
 ∪
 {
 x
 +
 1
 :
 x
 ∈
 X
 }
 
 
 {\displaystyle F(X)=\{0\}\cup \{x+1:x\in X\}}

It should not be difficult to see that 
 
 
 
 μ
 F
 =
 
 N
 
 
 
 {\displaystyle \mu F=\mathbb {N} }
 
. Therefore, by the principle of induction, if we wish to prove some property 
 
 
 
 P
 
 
 {\displaystyle P}
 
 of 
 
 
 
 
 N
 
 
 
 {\displaystyle \mathbb {N} }
 
, it suffices to show that 
 
 
 
 P
 
 
 {\displaystyle P}
 
 is F-closed. In detail, we require:

 
 
 
 F
 (
 P
 )
 ⊆
 P
 
 
 {\displaystyle F(P)\subseteq P}

That is,

 
 
 
 {
 0
 }
 ∪
 {
 x
 +
 1
 :
 x
 ∈
 P
 }
 ⊆
 P
 
 
 {\displaystyle \{0\}\cup \{x+1:x\in P\}\subseteq P}

This is precisely mathematical induction as stated.

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/F-coalgebra/VLE0yJjG">F-coalgebra</a></li>
<li><a href="/facts/Corecursion/w9voxGRn">Corecursion</a></li>
<li><a href="/facts/Bisimulation/mqupHSps">Bisimulation</a></li>
<li><a href="/facts/Anamorphism/nPgySzu3">Anamorphism</a></li>
<li><a href="/facts/Total_functional_programming/Eh2XhpDx">Total functional programming</a></li></ul>

<h2 id="further-reading">Further reading</h2>
Textbooks
<ul><li><a href="/facts/Davide_Sangiorgi/pSTJNFb6">Davide Sangiorgi</a> (2012). Introduction to Bisimulation and Coinduction. Cambridge University Press.</li>
<li><a href="/facts/Davide_Sangiorgi/pSTJNFb6">Davide Sangiorgi</a> and Jan Rutten (2011). Advanced Topics in Bisimulation and Coinduction. Cambridge University Press.</li></ul>
Introductory texts
<ul><li><a href="/facts/Andrew_D._Gordon/XTDJElgC">Andrew D. Gordon</a> (1994). "A Tutorial on Co-induction and Functional Programming". 1994. pp. 78–95. <a href="/facts/CiteSeerX_(identifier)/SceDmd3c">CiteSeerX</a> <a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3914">10.1.1.37.3914</a>. — mathematically oriented description</li>
<li>Bart Jacobs and Jan Rutten (1997). <a href="http://citeseer.ist.psu.edu/jacobs97tutorial.html">A Tutorial on (Co)Algebras and (Co)Induction</a> (<a href="https://www.cs.ru.nl/B.Jacobs/PAPERS/JR.pdf">alternate link</a>) — describes induction and coinduction simultaneously</li>
<li>Eduardo Giménez and Pierre Castéran (2007). <a href="http://www.labri.fr/perso/casteran/RecTutorial.pdf">"A Tutorial on [Co-]Inductive Types in Coq"</a></li>
<li><a href="http://www.cs.ucsd.edu/groups/tatami/handdemos/doc/coind.htm">Coinduction</a> — short introduction</li></ul>
History
<ul><li><a href="/facts/Davide_Sangiorgi/pSTJNFb6">Davide Sangiorgi</a>. "<a href="http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf">On the Origins of Bisimulation and Coinduction</a>", <a href="/facts/ACM_Transactions_on_Programming_Languages_and_Systems/nk6hTKJI">ACM Transactions on Programming Languages and Systems</a>, Vol. 31, Nb 4, Mai 2009.</li></ul>
Miscellaneous
<ul><li><a href="http://www.utdallas.edu/~gupta/ppdp06.pdf">Co-Logic Programming: Extending Logic Programming with Coinduction</a> — describes the co-logic programming paradigm</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">"Co-Logic Programming | Lambda the Ultimate". <a href="http://lambda-the-ultimate.org/node/2513" target="_blank">http://lambda-the-ultimate.org/node/2513</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">"Gopal Gupta's Home Page". <a href="http://www.utdallas.edu/~gupta/" target="_blank">http://www.utdallas.edu/~gupta/</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">"Logtalk3/Examples/Coinduction at master · LogtalkDotOrg/Logtalk3". GitHub. <a href="https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction" target="_blank">https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Pierce, Benjamin C. Types and Programming Languages. MIT Press. <a href="/wiki/Benjamin_C._Pierce" target="_blank">/wiki/Benjamin_C._Pierce</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">Kozen, Dexter; Silva, Alexandra. "Practical Coinduction". CiteSeerX 10.1.1.252.3961. <a href="/wiki/Dexter_Kozen" target="_blank">/wiki/Dexter_Kozen</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">Hinze, Ralf (2012). "Generic Programming with Adjunctions". Generic and Indexed Programming. Lecture Notes in Computer Science. Vol. 7470. Springer. pp. 47–129. doi:10.1007/978-3-642-32202-0_2. ISBN 978-3-642-32201-3. <a href="978-3-642-32201-3" target="_blank">978-3-642-32201-3</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
</ol>

Coinduction open-in-new

Coinduction