mmmodularity!

» by Scott Kilpatrick

Thanks again to Aaron for correcting a misconception I had about the (perhaps most general) principle of coinduction in the comments of the last post. He pointed out that a mixture of inductive and coinductive rules in an inference system gives rise to mixed fixed points, which come up in the mu calculus, for example.

At this point, though, I am ready to retire my pursuit.

It all started with the Henglein and Nielsen POPL paper I shared a while back. In it they define an inference system to prove regular expression containment and claim that it constitutes a “coinductive axiomatization,” on account of a “coinduction rule,” in their words.

They point out that this rule would be wholly unsound without some restriction on its applicability. For example, if the premise is proved with an application of the hypothesis rule, then E <= F can be proved for all E and F. One of their primary contributions is a “semantic side condition” on this rule: the derivation in the conclusion of this rule must have a certain form, and that form guarantees that the resulting proof term `fix f.c` — which they interpret as a coercion from a thing for E to a thing for F — is a total computation. (A major result of their paper asserts that if c is a total function from E-things to F-things then the regexp E is contained in the regexp F.) So, equipped with that semantic side condition, a derivation of `|- c : E <= F` involving the coinduction rule yields a recursive, but total, coercion.

Henglein uses a similar trick in his 1997 paper with Brandt, Coinductive Axiomatization of Recursive Type Equality and Subtyping (CiteSeerX). In that system, the “coinduction” is manifested in the subtyping rule for arrows, presented below.

Here they avoid the possibility of an immediate, unsound use of the hypothesis by specializing it to the arrow case: recursive use of the hypothesis-embedded conclusion in each premise does not actually gain anything.

As far as I can tell, these “coinduction” rules do not imply a coinductive interpretation of either set of inference rules, fully or mixed. Instead, the semantic side condition on the (regular expression) coinduction rule proves that the usual, inductive interpretation of the inference rules — which allows for typical proofs by induction on the structure of derivations* — is sound. Both of their inference systems are coinductive in spirit only, due to the recursive style of moving the conclusion into the hypotheses of the premises.

* In a comment after the last post I stated that I had thought they used “rule induction” in some proofs but then couldn’t find them upon later inspection. My original thought was correct: proofs by rule induction (on derivations of the allegedly coinductive judgments) are indeed present in both papers.

EDIT: Just now, I read in the notes at the end of Pierce’s chapter on recursive types and (co)induction in TAPL that he describes their earlier inference system as inductive! On pp. 312:

Brandt and Henglein (1997) laid bare the underlying coinductive nature of Amadio and Cardelli’s system, giving a new inductive axiomatization of the subtype relation […]. The so-called ARROW/FIX rule of the axiomatization embodies the coinductiveness of the system. The paper describes a general method for deriving an inductive axiomatization for relations that are naturally defined by coinduction […].

CASE CLOSED.

EDIT #2. Fritz Henglein has kindly weighed in on this discussion in the comments below! I retract my statement that his systems are “coinductive in spirit only,” not because he caught me but because his explanation below really does make it clear. In particular, he points to the revised version of the earlier paper (pdf), appearing in Fundamenta Informaticae 1998, in which they discuss this very issue (Section 4).