Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

"Even" set can be represented as Inductively Defined sets with two rules:

"$0 \in E$" and "$X \in E \implies X+2 \in E$"

now my question is, how the Co-Inductively defined sets are defined? why do we need them? and what are the differences?

share|cite|improve this question
up vote 3 down vote accepted

Essentially, an inductive datatype is one that is characterised by introduction rules, whereas a coinductive datatype is characterised by elimination rules. Here is one of the simplest pair of examples. Let $X$ be a fixed set.

  • Finite lists of elements of $X$ constitute an inductive datatype. There are two introduction rules:

    • The empty list $\mathsf{nil}$ is a finite list.
    • If $x$ is an element of $X$ and $t$ is a finite list, then $\mathsf{cons}(x, t)$, i.e. the list obtained by prefixing $x$ to $t$, is also a finite list.
  • Streams of elements of $X$ constitute a coinductive datatype. There are two elimination rues:

    • If $s$ is a stream, then $\mathsf{head}(s)$ is an element of $X$.
    • If $s$ is a stream, then $\mathsf{tail}(s)$ is another stream.

Now, how do we capture this formally? We need to transform the introduction/elimination rules into recursion/corecursion principles. For the above example, we get the following:

  • If $A$ is any set equipped with a chosen constant $a$ and a map $c : X \times A \to A$, then there is a unique map $f : \mathsf{List}(X) \to A$ such that $f (\mathsf{nil}) = a$ and $f (\mathsf{cons}(x, t)) = c(x, f(t))$.

  • If $C$ is any set equipped with maps $h : C \to X$ and $t : C \to C$, then there is a unique map $g : C \to \mathsf{Stream}(X)$ such that $\mathsf{head}(g(c)) = h(c)$ and $\mathsf{tail}(g(c)) = g(t(c))$.

Now, for various reasons it is easy to convert a recursion principle on a set into an induction principle. In the case of $\mathsf{List}(X)$ it amounts to saying that any subset $Y$ of $\mathsf{List}(X)$ containing $\mathsf{nil}$ and closed under $\mathsf{cons}(x, -)$ for all $x$ in $X$ must be the whole of $\mathsf{List}(X)$. (In the case $X = \{ 0 \}$ this is ordinary mathematical induction!)

However, coinduction is a rather more unfamiliar concept. The coinduction principle associated with $\mathsf{Stream}(X)$ says this: for any equivalence relation $\sim$ on $\mathsf{Stream}(X)$, if $\mathsf{head}(s) = \mathsf{head}(s')$ and $\mathsf{tail}(s) \sim \mathsf{tail}(s')$ whenever $s \sim s'$, then in fact $\sim$ is the equality relation on $\mathsf{Stream}(X)$.

To get a really concrete description of $\mathsf{List}(X)$ and $\mathsf{Stream}(X)$ as sets we must solve what are basically fixed point equations: $$\mathsf{List}(X) \cong 1 + X \times \mathsf{List}(X)$$ $$\mathsf{Stream}(X) \cong X \times \mathsf{Stream}(X)$$ It is not hard to see that $$\mathsf{List}(X) = 1 + X + X^2 + X^3 + \cdots = \sum_{n \in \mathbb{N}} X^n$$ $$\mathsf{Stream}(X) = X \times X \times X \times \cdots = X^\mathbb{N}$$ are solutions, but we must still check that these satisfy the appropriate recursion/corecursion principle: fortunately, this is straightforward.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.