# Inductively and Co-Inductively defined sets

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

-

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.

-