### Metric Coinduction

#### Posted by David Corfield

Dexter Kozen and Nicholas Ruozzi have a paper Applications of Metric Coinduction which begins

Mathematical induction is firmly entrenched as a fundamental and ubiquitous proof principle for proving properties of inductively defined objects. Mathematics and computer science abound with such objects, and mathematical induction is certainly one of the most important tools, if not the most important, at our disposal.

Perhaps less well entrenched is the notion of coinduction. Despite recent interest, coinduction is still not fully established in our collective mathematical consciousness. A contributing factor is that coinduction is often presented in a relatively restricted form. Coinduction is often considered synonymous with bisimulation and is used to establish equality or other relations on infinite data objects such as streams or recursive types.

In reality, coinduction is far more general. For example, it has been recently been observed that coinductive reasoning can be used to avoid complicated $\epsilon-\delta$ arguments involving the limiting behavior of a stochastic process, replacing them with simpler algebraic arguments that establish a

coinduction hypothesisas an invariant of the process, then automatically deriving the property in the limit by application of a coinduction principle. The notion of bisimulation is a special case of this: establishing that a certain relation is a bisimulation is tantamount to showing that a certain coinduction hypothesis is an invariant of some process.

The paper involves a series of applications of the ‘coinductive rule’ for complete metric spaces. Let $(V, d)$ be a complete metric space, and $H: V \to V$ a contractive function, i.e., there exists $0 \leq c \lt 1$ such that for all $u, v \in V$,

$d(H(u), H(v)) \leq c \cdot d(u, v).$

Any such map has a unique fixed point, $u^{*}$ in $V$.

The authors then consider the category $C$ whose objects are nonempty closed subsets of $V$ and whose arrows are the reverse set inclusions. If we now define $\bar{H}(A)$ as the closure of $H(A)$, for $A \subseteq V$, then $\bar{H}$ is an endofunctor on $C$. The terminal coalgebra for $\bar{H}$ is $\{u^{*}\}$, the singleton set of the fixed point.

Any nonempty closed subset, $A$, of $V$ which contains its own image under $H$ is a coalgebra for $\bar{H}$. The finality of the coalgebra $\{u^{*}\}$ expresses itself then in the coinductive rule, that $A$ as above must contain $u^{*}$.

A couple of things I’m wondering now. Whether I’ve quite grasped the distinction between coinduction and corecursion. From what I wrote there, this might seem better described as a ‘corecursive rule for complete metric spaces’. Please modify those $n$Lab entries as necessary.

And second, relating to my current interest in ‘symmetry breaking’ in mathematics, couldn’t Kozen and Ruozzi have defined their category $C$ to be nonempty closed subsets of $V$ with *inclusions* as morphisms? Then $\{u^{*}\}$ would have been the initial algebra of $\bar{H}$, and all would go through as before, producing an ‘inductive rule for complete metric spaces’.

Surely the only way coinduction starts to look different from induction is when you have good reason to fix a non-self-dual category as the setting. So working in $Set$, algebras are about constructing sets from specific terms and constructors, whereas coalgebras are about unfolding the behaviour of a system. But this depends on certain features of $Set$.

## Re: Metric Coinduction

I'd say yes. But I'd also warn anybody that the distinction between ‘induction’ and ‘recursion’ (and their duals) is not always observed in the literature.

There are actually three levels here. We produces

proofsby (co)induction; that is, we define (which amounts to establishing the existence of, since they are necessarily unique) elements of a truth value. By (co)recursion, we define elements of a set, most fundamentally elements of a hom-set into a final coalgebra or out of an initial algebra. And then we can also define (co)inductive types, which are objects of a category.Many people say ‘induction’ for all $3$ levels. Many people say ‘induction’, ‘recursion’, and then ‘induction’ again, while many people say ‘induction’, ‘recursion’, and then ‘recursion’ again. I'm inclined to say (which I just thought of, but now it looks obvious) to say ‘induction’, ‘recursion’, and ‘$2$-recursion’.

For example, give the polynomial $X \mapsto X + 1$, we rely on abstract nonsense to assure us that the category of sets has an initial algebra for this endofunctor; in this way, we $2$-recursively define the set $\mathbf{N}$ of natural numbers. Then when we run across some algebra $A$ for this endofunctor, such as a metric space equipped with a point (the theorem that you cite doesn't hold for the empty space) and a contractive endomap, we recursively define an algebra homomorphism $r$ from $\mathbf{N}$ to $A$. Then when we run across some algebra homomorphism $f$ from $\mathbf{N}$ to $A$, we inductively (or $0$-recursively) conclude that $f$ equals $r$.