First, to dispel a possible cognitive dissonance: reasoning about infinite structures is not a problem, we do it all the time. As long as the structure is finitely describable, that's not a problem. Here are a few common types of infinite structures:
- languages (sets of strings over some alphabet, which may be finite);
- tree languages (sets of trees over some alphabet);
- execution traces of a non-deterministic system;
- real numbers;
- sets of integers;
- sets of functions from integers to integers; …
Coinductivity as the largest fixpoint
Where inductive definitions build a structure from elementary building blocks, coinductive definitions shape structures from how they can be deconstructed. For example, the type of lists whose elements are in a set A is defined as follows in Coq:
Inductive list (A:Set) : Set :=
| nil : list A
| cons : A -> list A -> list A.
Informally, the list type is the smallest type that contains all values built from the nil and cons constructors, with the axiom that $\forall x \, y, \: \mathtt{nil} \ne \mathtt{cons} \: x \: y$. Conversely, we can define the largest type that contains all values built from these constructors, keeping the discrimination axiom:
CoInductive colist (A:Set) : Set :=
| conil : colist A
| cocons : A -> colist A -> colist A.
list is isomorphic to a subset of colist. In addition, colist contains infinite lists: lists with cocons upon cocons.
CoFixpoint flipflop : colist ℕ := cocons 1 (cocons 2 flipflop).
CoFixpoint from (n:ℕ) : colist ℕ := cocons n (from (1 + n)).
flipflop is the infinite (circular list) $1::2::1::2::\ldots$; from 0 is the infinite list of natural numbers $0::1::2::\ldots$.
A recursive definition is well-formed if the result is built from smaller blocks: recursive calls must work on smaller inputs. A corecursive definition is well-formed if the result builds larger objects. Induction looks at constructors, coinduction looks at destructors. Note how the duality not only changes smaller to larger but also inputs to outputs. For example, the reason the flipflop and from definitions above are well-formed is that the corecursive call is guarded by a call to the cocons constructor in both cases.
Where statements about inductive objects have inductive proofs, statements about coinductive objects have coinductive proofs. For example, let's define the infinite predicate on colists; intuitively, the infinite colists are the ones that don't end with conil.
CoInductive Infinite A : colist A -> Prop :=
| Inf : forall x l, Infinite l -> Infinite (cocons x l).
To prove that colists of the form from n are infinite, we can reason by coinduction. from n is equal to cocons n (from (1 + n)). This shows that from n is larger than from (1 + n), which is infinite by the coinduction hypothesis, hence from n is infinite.
Bisimilarity, a coinductive property
Coinduction as a proof technique also applies to finitary objects. Intuitively speaking, inductive proofs about an object are based on how the object is built. Coinductive proofs are based on how the object can be decomposed.
When studying deterministic systems, it is common to define equivalence through inductive rules: two systems are equivalent if you can get from one to the other by a series of transformations. Such definitions tend to fail to capture the many different ways non-deterministic systems can end up having the same (observable) behavior in spite of having different internal structure. (Coinduction is also useful to describe non-terminating systems, even when they're deterministic, but this isn't what I'll focus on here.)
Nondeterministic systems such as concurrent systems are often modeled by labeled transition systems. An LTS is a directed graph in which the edges are labeled. Each edge represents a possible transition of the system. A trace of an LTS is the sequence of edge labels over a path in the graph.
Two LTS can behave identically, in that they have the same possible traces, even if their internal structure is different. Graph isomorphism is too strong to define their equivalence. Instead, an LTS $\mathscr{A}$ is said to simulate another LTS $\mathscr{B}$ if every transition of the second LTS admits a corresponding transition in the first. Formally, let $S$ be the disjoint union of the states of the two LTS, $L$ the (common) set of labels and $\rightarrow$ the transition relation. The relation $R \subseteq S \times S$ is a simulation if
$$ \forall (p,q)\in R, %\forall p'\in S, \forall\alpha\in L,
\text{ if } p \stackrel\alpha\rightarrow p'
\text{ then } \exists q', \;
q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R
$$
$\mathscr{A}$ simulates $\mathscr{B}$ if there is a simulation in which all the states of $\mathscr{B}$ are related to a state in $\mathscr{A}$. If $R$ is a simulation in both directions, it is called a bisimulation. Simulation is a coinductive property: any observation on one side must have a match on the other side.
There are potentially many bisimulations in an LTS. Different bisimulations might identify different states. Given two bisimulations $R_1$ and $R_2$, the relation given by taking the union of the relation graphs $R_1 \cup R_2$ is itself a bisimulation, since related states give rise to related states for both relations. (This holds for infinite unions as well. The empty relation is an unintersting bisimulation, as is the identity relation.) In particular, the union of all bisimulations is itself a bisimulation, called bisimilarity. Bisimilarity is the coarsest way to observe a system that does not distinguish between distinct states.
Bisimilarity is a coinductive property. It can be defined as the largest fixpoint of an operator: it is the largest relation which, when extended to identify equivalent states, remains the same.
References
