"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?
"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:
Streams of elements of $X$ constitute a coinductive datatype. There are two elimination rues:
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.