Coinduction and Bisimulation

A previous post explored the concept of structural induction. In this post, we will explore the dual of structural induction, namely, structural coinduction, and the related concept of bisimulation.

Throughout this post, we will consider the example of the co-natural numbers \(\bar{\mathbb{N}}\), also called the extended natural numbers. Roughly speaking, the co-natural numbers are the extension of the natural numbers to include an infinite number \(\infty\).

Like structural induction, the goal of structural coinduction is to define a certain set (e.g. \(\bar{\mathbb{N}}\)). We proceed as follows.

First, we choose some ambient set \(X\). We will define the co-natural numbers syntactically, i.e., as finite and infinite strings (sequences of symbols from some alphabet). The ambient set is the set \(X = \Sigma^{\infty}\) of all finite and infinite sequences of symbols from the alphabet \(\Sigma = \{s, z\}\) (where \(s\) represents the successor and \(z\) represents zero).

The powerset \(\mathcal{P}(X)\) represents all potential candidate sets. Our goal is to select a particular such candidate.

We define an operation \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) that "refines" a stock of elements \(A \subseteq X\) into a finer stock of elements \(F(A)\). We will define the co-natural numbers in terms of an operation that adds prefixes to strings, such that, after \(n\) applications of the operation \(F\), all remaining elements have a "valid" prefix consisting of \(n\) elements.

We start with everything (i.e., the entire set \(X\)) and then refine this into the set \(F(X)\). We then iterate this process indefinitely:

\[X \supseteq F(X) \supseteq F(F(X)) \supseteq F(F(F(X))) \supseteq \dots .\]

We want there to be a descending chain as indicated, since we think of the process as progressive refinement. Note that, if \(F\) is monotone, then this descending chain condition will be satisfied, since \(X \supseteq F(X)\) by definition and hence \(F(X) \supseteq F(F(X))\), etc.

We want this process to terminate at a fixed point, i.e., some set \(\nu F \subseteq X\) such that \(F(\nu F) = \nu F\). However, unlike structural induction, which employs the least fixed point, we instead utilize the greatest fixed point. Note that, since we utilize the greatest fixed point in a descending chain, this means that the process stops as soon as \(X\) is sufficiently refined so that it becomes closed under \(F\), i.e., it cannot be refined anymore. Thus, we "discard" only what is strictly necessary, and nothing more. If \(F\) is monotone, then the greatest fixed point is guaranteed to exist. This yields a general method for coinductive definitions: specify an ambient set \(X\), a monotone map \(F\) on \(\mathcal{P}(X)\), and define the generated set as \(\nu F\).

A similar procedure permits us to define structurally corecursive relations and functions.

Moreover, this produces an attendant coinductive proof principle: we can show that \(A \subseteq \nu F\) whenever \(A \subseteq F(A)\). However, a more useful proof principle is bisimulation, namely, a certain structurally corecursive relation on a coinductively-defined set.

We will now proceed to describe structural coinduction and bisimulation in more detail. We begin with some preliminaries about fixed points of monotone maps.

Fixed Points

Definition (Monotone Map). Let \(X\) be any set. A function \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) is monotone if \(F(A) \subseteq F(B)\) whenever \(A \subseteq B\) for any \(A,B \subseteq X\).

Note: Monotone maps can be defined more generally for arbitrary posets (partially-ordered sets), but we do not require this level of generality. We are interested in the poset \((\mathcal{P}(X), \subseteq)\).

Definition (Post-Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A set \(A \subseteq X\) is a post-fixed point of \(F\) if \(A \subseteq F(A)\).

Definition (Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A set \(A \subseteq X\) is a fixed point of \(F\) if \(F(A) = A\).

Definition (Greatest Post-Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A post-fixed point \(A \subseteq X\) is the greatest post-fixed point of \(F\) if \(B \subseteq A\) for every post-fixed point \(B \subseteq X\) of \(F\).

Note that greatest post-fixed points are necessarily unique, since, if \(A\) and \(B\) are both greatest post-fixed points, then, by definition, \(A \subseteq B\) and \(B \subseteq A\), so \(A = B\).

Definition (Greatest Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A fixed point \(\nu F \subseteq X\) is the greatest fixed point of \(F\) if \(A \subseteq \nu F\) for every fixed point \(A \subseteq X\) of \(F\).

Note that greatest fixed points are necessarily unique, since, if \(A\) and \(B\) are both greatest fixed points, then, by definition, \(A \subseteq B\) and \(B \subseteq A\), so \(A = B\). Thus, we simply write \(\nu F\) to denote the greatest fixed point.

The greatest fixed point is also called a coinductively-defined set. As we will demonstrate, the map \(F\) represents "rules" for producing elements and the greatest fixed point \(\nu F\) is closed under these production rules.

As we indicated previously, there is a descending chain

\[X \supseteq F(X) \supseteq F^2(X) \supseteq F^3(X) \supseteq \dots .\]

Intuitively, we start with the ambient set \(X\) and successively refine it until it can be refined no further. This process terminates at the greatest fixed point \(\nu F\). We might attempt to compute this fixed point by the intersection

\[\bigcap_{n \in \mathbb{N}}F^n(X)\]

where \(F^n\) is defined by ordinary mathematical induction as

• \(F^0(X) = X\),
• \(F^{n+1}(X) = F(F^n(X))\).

However, there is a technical issue with this approach: it is not the case, in general, that

\[F\left(\bigcap_{n \in \mathbb{N}}X_n\right) = \bigcap_{n \in \mathbb{N}}F(X_n),\]

for descending sequences of sets \(X_n\). A map \(F\) satisfying this condition is called \(\omega\)-cocontinuous. If indeed the map satisfies this condition, then

\[F\left(\bigcap_{n \in \mathbb{N}}F^n(X)\right) = \bigcap_{n \in \mathbb{N}}F(F^n(X)) = \bigcap_{n \in \mathbb{N}}F^n(X).\]

Many classes of maps \(F\) will indeed satisfy this condition. However, we seek a definition that will work for any monotone map. For a set \(A\) to be a fixed point of \(F\), it must also be a post-fixed point of \(F\). We desire the greatest fixed point, so we take the union of all post-fixed points.

Note that we cannot define the greatest fixed point as the union of all fixed points since the union of fixed points is not guaranteed to be a fixed point. However, the union of post-fixed points is guaranteed to be a post-fixed point. Since the greatest post-fixed point is also the greatest fixed point, this suffices.

This leads to the following theorems.

Theorem (Greatest Fixed Point). Let \(X\) be any set and let \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. Then:

\[\nu F = \bigcup\{S \subseteq X \mid S \subseteq F(S)\}.\]

Proof. Suppose that \(x \in \nu F\). Then, by definition, there exists a set \(S \subseteq X\) such that \(S \subseteq F(S)\) and \(x \in S\). By construction, \(S \subseteq \nu F\) and, since \(F\) is monotone, \(F(S) \subseteq F(\nu F)\), and hence \(x \in S \subseteq F(S) \subseteq F(\nu F)\), so \(x \in F(\nu F\)). Since \(x\) was arbitrary, \(\nu F \subseteq F(\nu F)\).

Conversely, suppose that \(x \in F(\nu F)\). Since \(\nu F \subseteq F(\nu F)\) and \(F\) is monotone, \(F(\nu F) \subseteq F(F(\nu F))\). Thus, there exists a set \(S = F(\nu F)\) such that \(S \subseteq F(S)\) and \(x \in S\), so, by definition, \(x \in \nu F\). Since \(x\) was arbitrary, \(F(\nu F) \subseteq \nu F\).

Thus, \(F(\nu F) = \nu F\) and \(\nu F\) is a fixed point of \(F\).

Now, suppose that \(F(S) = S\) for some set \(S \subseteq X\). Suppose \(x \in S\). Then \(S \subseteq F(S)\), so, by definition, \(x \in \nu F\). Since \(x\) was arbitrary, \(S \subseteq \nu F\). Thus, \(\nu F\) is the greatest fixed point. \(\square\)

Theorem. Let \(X\) be any set and let \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A set \(A\) is the greatest post-fixed point of \(F\) if and only if it is the greatest fixed point of \(F\).

Proof. Suppose that \(A\) is the greatest post-fixed point of \(F\). Then, by definition, \(A \subseteq F(A)\). Since \(F\) is monotone, \(F(A) \subseteq F(F(A))\), so \(F(A)\) is a post-fixed point of \(F\). Since \(A\) is the greatest post-fixed point of \(F\), it follows that \(F(A) \subseteq A\). Thus, \(F(A) = A\) and \(A\) is a fixed point of \(F\). If \(B\) is any other fixed point of \(F\), then \(B\) is likewise a post-fixed point of \(F\), and, since \(A\) is the greatest post-fixed point of \(F\), it follows that \(B \subseteq A\). Thus, \(A\) is the greatest fixed point of \(F\).

Conversely, suppose that \(A\) is the greatest fixed point of \(F\). Then, by definition, \(A = F(A)\) and hence \(A \subseteq F(A)\) and so \(A\) is a post-fixed point of \(F\). Suppose \(B\) is any other post-fixed point of \(F\). Then \(B \subseteq F(B)\). By the Greatest Fixed Point Theorem,

\[A = \bigcup \{S \subseteq X \mid S \subseteq F(S)\}.\]

It follows that \(B \subseteq A\). Since \(B\) was arbitrary, it follows that \(A\) is the greatest post-fixed point of \(F\). \(\square\)

Coinductive Proofs

Combining the previous theorems on post-fixed and fixed points, we immediately arrive at the following corollary:

Corollary (Coinductive Proof Principle). Let \(X\) be any set and let \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. For any post-fixed point \(A\), \(A \subseteq \nu F\).

It isn't obvious why this represents a proof principle or how to apply the principle, so some explanation is required. Typically, this is applied in the case that we want to establish that a coinductive set contains certain elements (often this is not obvious). For instance, we can prove that \(\infty \in \bar{\mathbb{N}}\).

If we establish \(A \subseteq F(A)\), then this proves that \(A \subseteq \nu F\). Thus, if we show that a set is closed under the operation \(F\), then this ensures that each of the elements in this set are members of the greatest fixed point \(\nu F\).

In the next section, we will show that \(\{\infty\} \subseteq F(\{\infty\})\) for a particular operation \(F\), thus demonstrating that \(\infty \in \bar{\mathbb{N}}\), i.e., that the co-natural numbers do contain such an element.

The Co-Natural Numbers

As an example, consider the co-natural numbers \(\bar{\mathbb{N}}\). We will define the co-natural numbers syntactically. The ambient set is the set

\[X = \Sigma^{\infty}\]

where

\[\Sigma = \{z, s\}\]

and \(s\) and \(z\) are any distinct sets whatsoever, where \(s\) represents the successor operation and \(z\) represents zero. The set \(\Sigma^{\infty}\) is the set of all finite and infinite sequences of elements of \(\Sigma\). We write sequences using notation such as

\[sssz\]

which represents the finite sequence \((a_i)_{i=1}^4\) such that \(a_1 = s\), \(a_2 = s\), \(a_3 = s\), and \(a_4 = z\). The sequence represents the string of symbols in the order they appear from left to right.

We define a monotone map \(F : \mathcal{P}(\Sigma^{\infty}) \rightarrow \mathcal{P}(\Sigma^{\infty})\) as follows:

\[F(A) = \{z\} \cup \{sa \mid a \in A\}.\]

Here, \(sa\) denotes the concatenation of \(s\) to the sequence \(a\), defined as the sequence

• \((sa)(0) = s\),
• \((sa)(n+1) = a(n)\).

Note that we have defined the monotone map representing the co-natural numbers in exactly the same way we would define the monotone map representing the natural numbers; however, we use an ambient set representing finite and infinite strings and we select the greatest fixed point. The map \(F\) still represents a "construction" process: we construct elements \(F(A)\) from elements \(A\).

The "refinement" happens in the chain

\[X \supseteq F(X) \supseteq F^2(X) \supseteq \dots .\]

At stage \(F(X)\), the only surviving elements are \(z\) and all strings beginning with \(s\).

"Invalid" strings such as \(szzz\) remain. At stage \(F^2(X)\), the string \(szzz\) gets mapped to \(sszzz\); thus, it is "valid" up to the second index. At stage \(n\), all elements are likewise "valid" up to index \(n\). At stage \(n\), all surviving elements have a valid prefix of length \(n\). Finally, in the limit, the only things remaining are those strings that are valid for all indices \(n\).

One special element exists in our set: the infinite number \(\infty\) which is the infinite constant sequence \(ssss\dots\).

We will prove that \(\infty \in \bar{\mathbb{N}}\) by coinduction. To apply the coinductive proof principle, we need to show that

\[\{\infty\} \subseteq F(\{\infty\}),\]

which then entails that \(\{\infty\} \subseteq \nu F\), i.e., \(\infty \in \nu F = \bar{\mathbb{N}}\).

We define \(\infty\) as the constant infinite sequence

\[\infty(n) = s,\]

i.e.,

\[\infty = ssssss\dots .\]

We need to show that \(s\infty = \infty\). First, \((s\infty)(0) = \infty(0)\) by definition, so consider \(n+1\). Then \((s\infty)(n+1) = \infty(n)\) by definition, and \(\infty(n) = s = \infty(n+1)\) by construction (since it is constant), so \((s\infty)(n+1) = \infty(n+1)\). Thus, in all cases, \((s\infty)(n) = \infty(n)\) so \(s\infty = \infty\). This means that

\[\infty \in \{sa \mid a \in \{\infty\}\},\]

i.e., that \(\{\infty\} \subseteq F(\{\infty\})\), so, by the coinductive proof principle, \(\{\infty\} \subseteq \nu F = \bar{\mathbb{N}}\), i.e., \(\infty \in \bar{\mathbb{N}}\). We have thus proved that the co-natural numbers contain an "infinite" number \(\infty\).

Canonicity

Next, we want to establish that the set \(\bar{\mathbb{N}} = \nu F\) is canonical, namely, that it contains the desired elements and nothing more, namely, just the elements that can be constructed from the "rules" implicit in the definition of \(F\). The canonical set (i.e., intended set) is

\[C = \{s^nz \mid n \in \mathbb{N} \} \cup \{\infty\},\]

where \(s^n\) denotes the \(n\)-fold iteration of \(s\) and \(\infty\) is the infinite iteration of \(s\). Of course, we could simply specify this as the definition of the co-natural numbers, but this definition is not a coinductive definition, so we would not be able to exploit coinductive techniques.

We then define the rank-\(n\) approximants \(A_n\) as the sets

\[A_n = F^n(X).\]

First, we determine the form of these approximants. Note that

\[A_0 = F^0(X) = X = \{s^kz \mid k \lt 0\} \cup \{s^0x \mid x \in X\}.\]

Suppose that

\[A_n = \{s^kz \mid k \lt n\} \cup \{s^nx \mid x \in X\}\]

and consider \(A_{n+1} = F^{n+1}(X) = F(A_n)\). By definition of \(F\), it follows that

\[F(A_n) = \{s^kz \mid k \lt n+1\} \cup \{s^{n+1}x \mid x \in X\}.\]

Thus, by induction on the rank \(n\), it follows for all ranks \(n \in \mathbb{N}\) that

\[A_n = \{s^kz \mid k \lt n\} \cup \{s^nx \mid x \in X\}.\]

Next, although, as we noted previously, it is not the case in general that

\[\nu F = \bigcap_{n \in \mathbb{N}}A_n,\]

it is nonetheless indeed the case for the co-natural numbers as we have defined them. We will first show that

\[\bigcap_{n \in \mathbb{N}}A_n = C.\]

Suppose \(x \in C\). Then, either \(x = s^kz\) for some \(k \in \mathbb{N}\) or \(x = \infty\). If \(x = s^kz\), there are two cases: \(k \lt n\) or \(k \ge n\). If \(k \lt n\), then \(x \in A_n\) by definition. If \(k \ge n\), then \(x = s^ns^{k-n}z\) and \(s^{k-n}z \in X\) so \(x \in A_n\) by definition. If \(x = \infty\), then it is easy to show by induction on \(n\) that \(x = s^n\infty\), and thus, \(x \in A_n\). In all cases and for all \(n \in \mathbb{N}\), \(x \in A_n\), thus

\[C \subseteq \bigcap_{n \in \mathbb{N}}A_n.\]

Next, we will show the converse, namely,

\[\bigcap_{n \in \mathbb{N}}A_n \subseteq C.\]

We will proceed by contradiction. Suppose that \(x \in \bigcap_{n \in \mathbb{N}}A_n\) and \(x \notin C\). Then, for every \(n \in \mathbb{N}\), \(x \in A_n\). If \(x \in \{s^kz \mid k \lt n\}\) for any \(n \in \mathbb{N}\), then \(x \in C\), a contradiction. Thus, if \(x \in A_n\) for all \(n \in \mathbb{N}\) and \(x \notin C\), then \(x \in \{s^nx \mid x \in X\}\) for all \(n \in \mathbb{N}\). This implies that \(x = \infty\), and hence \(x \in C\), a contradiction.

Thus, as required,

\[\bigcap_{n \in \mathbb{N}}A_n = C.\]

Finally, we want to indicate that \(\nu F = C\). Since

\[F(C) = \{z\} \cup \{sc \mid c \in C\} = \{s^n \mid n \in \mathbb{N}\} \cup \{\infty\} = C,\]

\(C\) is therefore a fixed point of \(F\). We will show that it is the greatest fixed point. Suppose \(F(B) = B\) for some \(B \subseteq X\). We will show by induction that, for all \(n \in \mathbb{N}\),

\[B \subseteq A_n.\]

When \(n=0\), by definition, \(B \subseteq A_0 = X\). Suppose \(B \subseteq A_n\) for some \(n \in \mathbb{N}\). Then, since \(F\) is monotone and \(B\) is a fixed point, \(B \subseteq F(B) \subseteq F(A_n) = A_{n+1}\).

It follows that

\[B \subseteq \bigcap_{n \in \mathbb{N}}A_n = C.\]

Thus, \(C\) is the greatest fixed point, i.e., \(C = \nu F\).

We have thus established that \(\nu F\) is canonical.

Corecursion

Since relations are sets in set theory, relations can likewise be defined as coinductive sets. Relations defined this way are called corecursive. Definitions by corecursion are generally only useful when the codomain is a coinductive set since this will allow us to establish properties about the relation using coinductive techniques. Since functions are relations satisfying certain properties, functions can be defined using corecursion also.

Bisimulations are important examples of corecursive relations. They will be detailed in a subsequent section.

We will define a corecursive function that adds two co-natural numbers as the greatest fixed point of a monotone map \(G : \mathcal{P}((\bar{\mathbb{N}} \times \bar{\mathbb{N}}) \times \bar{\mathbb{N}}) \rightarrow \mathcal{P}((\bar{\mathbb{N}} \times \bar{\mathbb{N}}) \times \bar{\mathbb{N}})\) defined as

\begin{align*}G(R) &= \{((a,z), a) \mid a \in \bar{\mathbb{N}}\} \\&\cup \{((z,b), b) \mid b \in \bar{\mathbb{N}}\} \\&\cup \{((sa,b),sc) \mid ((a,b),c) \in R\} \\&\cup \{((a, sb),sc) \mid ((a,b), c) \in R\}.\end{align*}

We then define the function as

\[\mathrm{add} = \nu G.\]

We need to prove that this is indeed a function. To do so requires the technique of bisimulation which we will merely preview here. Suppose that there exist \(a, b, v, v' \in \bar{\mathbb{N}}\) such that \(\mathrm{add}(a, b) = v\) and \(\mathrm{add}(a,b) = v'\). We define a relation as follows:

\[B = \{(c,c') \in \bar{\mathbb{N}} \times \bar{\mathbb{N}} \mid \exists a,b \in \bar{\mathbb{N}} . (a,b,c) \in \mathrm{add} \land (a,b,c') \in \mathrm{add}\}.\]

If we can show that \(B\) is a bisimulation and \(vBv'\), then, since the co-natural numbers enjoy extensionality (which we will describe later), it follows that \(v=v'\). For now, we just preview the technique.

If \(v=z\), then \(((a,b),z) \in \mathrm{add}\), so, according to the definition of \(G\), it must be the case that \(a=b=z\). Then it follows that \(v'=z\). Thus, \(zBz\). By canonicity, the only other possibility is \(v=sc\) and \(v'=sc'\) for some \(c,c' \in \bar{\mathbb{N}}\), so, according to the definition of \(G\), it must be the case either that \((sa', b), sc) \in \mathrm{add}\) and \((sa', b), sc') \in \mathrm{add}\) and \(((a', b),c) \in \mathrm{add}\) and \(((a', b),c') \in \mathrm{add}\), in which case \(cBc'\), or else it must the case that \((a, sb'), sc) \in \mathrm{add}\) and \((a, sb'), sc') \in \mathrm{add}\) and \(((a, b'),c) \in \mathrm{add}\) and \(((a, b'),c') \in \mathrm{add}\), in which case \(cBc'\). Regardless, \((sc)B(sc')\) with \(cBc'\). Thus, \(B\) is a bisimulation and so \(v \sim_B v'\), which, by extensionality, implies that \(v = v'\).

Bisimulation

A bisimulation is a binary relation \(R \subseteq X \times Y\) that is a post-fixed point of a particular monotone map \(\overline{(F,G)} : \mathcal{P}(X \times Y) \rightarrow \mathcal{P}(X \times Y)\), i.e.,

\[R \subseteq \overline{(F,G)}(R).\]

In particular, the monotone map \(\overline{(F,G)}\) is the lifting of monotone maps \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) and \(G : \mathcal{P}(Y) \rightarrow \mathcal{P}(Y)\): each such pair of monotone maps naturally induces a monotone map on \(\mathcal{P}(X \times Y)\).

The most common case is when \(F=G\) and \(X=Y\) and \(R \subseteq X \times X\), in which case we simply write \(\bar{F} : \mathcal{P}(X \times X) \rightarrow \mathcal{P}(X \times X)\) for this lifting.

For any relation \(R \subseteq X \times Y\) and set \(U \subseteq X\), we define

\[R[U] = \{y \in Y \mid \exists x \in U . xRy\}\]

and likewise for any set \(V \subseteq Y\), we define

\[R^{-1}[V] = \{x \in X \mid \exists y \in V . xRy\}.\]

We then define the lifting as follows for any relation \(R \subseteq X \times Y\):

\[\overline{(F,G)}(R) = \{(x,y) \in X \times Y \mid \forall U \subseteq X . x \in F(U) \Rightarrow y \in G(R[U]) \land \forall V \subseteq Y . y \in G(V) \Rightarrow x \in F(R^{-1}[V])\}.\]

Thus, given \(F\) and \(G\), a bisimulation is any post-fixed point of \(\overline{(F,G)}\).

Given monotone maps \(F\) and \(G\), we say that \(x \in X\) is bisimilar to \(y \in Y\), written \(x \sim_{F,G} y\), if there exists some bisimulation \(R\) such that \(xRy\). Equivalently, \(\sim_{F,G}\) is the greatest bisimulation: this definition says that

\[\sim_{F,G} = \bigcup \{R \subseteq X \times Y \mid R \subseteq \overline{(F,G)}(R)\}\]

which, by the Fixed Point Theorem, indicates that \(\sim_{F,G}\) is precisely the greatest fixed point of \(\overline{(F,G)}\), i.e., the greatest bisimulation. In the case that we are considering relations \(R \subseteq X \times X\) on a set \(X\) and a single monotone map \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\), then we simply write \(x \sim_F y\).

Bisimilarity is an example of a corecursive relation. Since, in set theory, relations are themselves sets, a corecursive relation is simply a coinductively-defined set that happens to be defined as the greatest fixed point of a monotone map on the powerset of a product set. This is precisely how bisimilarity is defined: as the greatest fixed point of \(\overline{(F,G)}\).

Bisimilarity is behavioral equivalence. We say that a coinductively-defined set is extensional whenever behavioral equivalence is identity, i.e., two elements of the set are bisimilar if and only if they are equal. So, extensionality means that, if \(x,y \in \nu F\), then \(x \sim_F y\) if and only if \(x = y\).

Example

Let's work out what bisimilarity means for the co-natural numbers. Suppose \(x,y \in \bar{\mathbb{N}}\) and \(x \sim_F y\), where

\[F(A) = \{z\} \cup \{sa \mid a \in A\}.\]

By definition, this means that there exists a bisimulation \(R\) such that \(xRy\). Since \(R\) is a bisimulation, by definition, \(R \subseteq \bar{F}(R)\), and thus \((x,y) \in \bar{F}(R)\), which means that

• \(\forall U \subseteq X (x \in F(U) \Rightarrow y \in F(R[U]))\), and
• \(\forall V \subseteq X (y \in F(V) \Rightarrow x \in F(R^{-1}[V]))\).

Since \(\emptyset \subseteq X\), this means that \(x \in F(\emptyset) \Rightarrow y \in F(R[\emptyset])\) which means that \(x \in \{z\} \Rightarrow y \in \{z\}\), i.e., \(x = z \Rightarrow y = z\). Similarly, \(y \in F(\emptyset) \Rightarrow x \in F(R^{-1}[\emptyset])\) means that \(y = z \Rightarrow x = z\). Combining these results yields

\[x = z \Leftrightarrow y = z.\]

Suppose \(x \ne z\). Let \(x' \in \bar{\mathbb{N}}\). Since \(\{x'\} \subseteq X\), \(x \in F(\{x'\}) \Rightarrow y \in F(R[\{x'\}])\). Then, since \(x \in F(\{x'\})\) and \(x \ne z\), this means that \(x = sx'\). Likewise, since \(x \ne z\) and \(x = y \Leftrightarrow y = z\), it follows that \(y \ne z\), and thus \(y \in F(R[\{x'\}]\) means

\[y \in \{sa \mid a \in R[\{x'\}]\},\]

i.e., there exists a \(y' \in X\) such that \(x'Ry'\) and \(y = sy'\). Moreover, since \(y \in \nu F\), canonicity implies that \(y' \in \nu F = \bar{\mathbb{N}}\). Thus, we have

\[x = sx' \Rightarrow \exists y' \in \bar{\mathbb{N}} (y = sy' \land x'Ry').\]

A symmetric argument shows that

\[y = sy' \Rightarrow x = \exists x' \in \bar{\mathbb{N}} (sx' \land x'Ry').\]

By canonicity, the terms \(x\) and \(y\) either have form \(z\) or \(sn\) for \(n \in \bar{\mathbb{N}}\). By the previous results, the only two possibilities for \(xRy\) are:

• \(zRz\),
• \((sx')R(sy')\), where \(x',y' \in \bar{\mathbb{N}}\) and \(x'Ry'\).

Extensionality

Next, we will show that the co-natural numbers are extensional, namely, bisimilarity coincides with equality.

Let \(x,y \in \bar{\mathbb{N}}\) be arbitrary and suppose that \(x \sim y\). We define the following infinite sequences:

\[\tilde{x}_n = \begin{cases}x_n & \text{if } n \in \mathrm{dom}(x) \\ * & \text{otherwise}\end{cases},\]

\[\tilde{y}_n = \begin{cases}y_n & \text{if } n \in \mathrm{dom}(y) \\ * & \text{otherwise}\end{cases}.\]

These sequences simply promote finite sequences to infinite sequences with an infinite tail consisting of a single trailing symbol \(*\), e.g., \(ssz\) becomes \(ssz******\dots\).

Clearly, \(\tilde{x} = \tilde{y}\) if and only if \(x = y\).

We prove the following property holds for all \(n \in \mathbb{N}\) by ordinary induction:

\[P(n) = \tilde{x}_n = \tilde{y}_n.\]

When \(n=0\), by the definition of bisimilarity for the co-natural numbers, we have either \(z \sim z\) or \(sx' \sim sy'\) where \(x' \sim y'\). In either case, \(x_0 = y_0\).

Suppose \(\tilde{x}_n = \tilde{y}_n\). Then either \(\tilde{x}_n = \tilde{y}_n = *\), in which case \(\tilde{x}_{n+1} = \tilde{y}_{n+1} = *\), or else \(sx' \sim sy'\) where \(x' \sim y'\), so, by inductive hypothesis, \(\tilde{x'}_n = \tilde{y'}_n\), so \(\tilde{x}_{n+1} = \tilde{y}_{n+1}\).

Conclusion

Coinduction is a powerful technique for defining certain sets and establishing their properties. There are many applications of coinduction beyond the simple use case of the co-natural numbers explored here.

There is also a category-theoretic approach (described briefly in this blog post). In this approach, rather than fixing an ambient set, an ambient category is fixed. Then, instead of a monotone map, a functor on the ambient category is employed. Then, a coinductively-defined object is specified, up to isomorphism, by a universal property, namely, as the carrier of the final coalgebra associated with the respective functor.