There's a subtle problem with inductive definitions. Consider the cannonical example of Nat, usually defined using something like the following pseudo-code:
Nat: Type
Z : Nat
S : Nat -> Nat
The problem is that given only this definition we cannot answer a simple question: is every n:Nat of the form S...Z? In other words, do the cannonical constructors of an inductively defined type exhaust the membership of that type?
The mathematician Andrej Bauer wrote an interesting blog post on this topic (
The elements of an inductive type), but he comes at it from a very different perspective than I do. His focus is on models of Nat, and he shows that there are various "exotic" models, which he describes thusly: "Let us call a model exotic if not every element of (the interpretation of) 𝚗𝚊𝚝 is obtained by finitely many uses of the successor constructor, starting from zero." It's an interesting post (as are the comments), but I think it misses the key point, which is that the problem is inherent in the structure of inductive definition; models are beside the point. In this article I take a stab at an alternative characterization of the problem and a possible solution.
The reason we cannot answer the question of whether an inductively defined type contains only those elements built up using the constructors, given only the inductive definition, is that the inductive part of the definition (here, S) makes the assumption that its argument is of the appropriate type, but that's the
only assumption it makes. In particular it makes no assumption as to the structure of that argument. We can make this a bit more explicit using informal English:
Z is a natural number
Assuming that n is a natural number, infer that Sn is a natural number.
So we've assumed that n:Nat, but we have not assumed that it has cannonical form. Maybe it was constructed solely using Z and S, maybe it wasn't - all we know (or rather assume) is that it is a Nat. For the purposes of inductive definition, it does not matter: S is a rule. If n is in fact of type Nat (no assumption here), then, no matter what its form or how we got it, Sn is of type Nat, end of story. So for all we know, Nat could be chock-full of non-canonical members.
That's not very satisfactory, since intuition tells us that of course there is nothing in Nat that is not constructed from Z and S. But our inductive definition does not
say this, and there is no way to
prove it from the definition alone.
Then how can we vindicate our intuitions, and show that every Nat is built up using nothing but S, starting from Z? We want something like the following proposition:
For all n:Nat, either n=Z or n=Sm for some m:Nat ;; where n=Sm means Sm is the canonical form of n)
Note that the inductive definition of Nat does not justify the second part of this proposition. It tells us that every n:Nat has a successor Sn:Nat, but it does not tell us that every n:Nat is the successor to some other Nat (that is, has a predecessor "some m" such that n=Sm). Even worse, it leaves open the possibility that every n:Nat could have any number of predecessors. It may seem intuitively obvious that every Nat has a unique successor and a unique predecessor, but again, the definition does not
say this; in fact it does not even
imply it if your intuition hasn't already been trained to expect it. Nor can it be used to
prove it.
We cannot justify this inductively, since induction will always involve assumptions as above, and if we try to build canonicity into our assumptions we just move the problem. For example it won't work to say "Assuming that n is either Z or a Nat of form Sm, then Sn is a Nat", since the same problem arises with respect to m. And we cannot go further and say "Assuming that n is a cannonical Nat..." because that is obviously circular - you only get canonical form
after you've defined S.
The only way I can see to do it is to use the dual notion of
coinduction. The idea is that we can introduce another operator P (Predecessor) and use it to show that every n:Nat can be expressed as (or reduced to, or equivalent to, choose your terminology) a canonical form. But not:
defined as a canonical form!
Coinduction does not define; it does not say what things
are (no metaphysics here); rather, it characterizes how they
behave, which is to say it
codefines them
. (See my previous post,
Definition and Co-definition, for more on the distinction.) The fact that every n:Nat has a predecessor (with PZ = Z) does not define Nat, it just says what you can do with a Nat once you have one. By the same token it is not quite true to say that Z and S define Nat; they define those elements of Nat that have canonical form, but they do not "close" Nat, in that they do not and cannot exclude the possibility of (undefined) non-canonical Nat forms.
So to get a complete and intuitively satisfying "definition" of Nat we need both an inductive definition of canonical forms and a coinductive codefinition of non-canonical forms. Here's one way to get started that I don't think works:
P : Nat -> Nat
Leaving aside the fact that this just looks like an alias for S (I'll address that problem in a minute), the form of this expression obscures the difference between inductive constructor and coinductive coconstructor. Informally, an inductive constructor of a type X takes things "into" X; a coinductive coconstructore takes things "from" X. We can therefore make this structure more conspicuous as follows:
S : Nat -> X
P : Nat <- X
and setting X == Nat. We could also have written P : X -> Nat, but that would make P look like a constructor for Nat rather than a coconstructor for X. It's really the reversal of the arrow that exposes the duality, rather than the swapping of the type variables.
So now we have P: Nat <- X, but that just looks like a funny way to write S. All it says is that if you have n:Nat, then you have Pn:Nat. Now the question is how to express the idea that P functions as a predecessor operation. The only way to do that is in terms of S.
PZ = Z
SPn = Sn ;; n = Z
SPn = n ;; n != Z
Note that we are not using S to define P. That is, we do not want to define P by saying P(Sn) = n; we want instead to start with the same minimal assumption we used to specify S, namely, "Assuming n:Nat, infer Pn...". In fact we're not really defining P at all! Instead we're specifying the relation between S and the result of
using P. There's really nothing in this "definition" that characterizes P as a predecessor operation, except for the fact that the successor operation S cancels it out. In a sense the operation P performs is completely hidden, and could be anything; all that matters is that once you use P, you can use S to cancel it out.
(Note that S : Nat -> X is also not a definition
of S. It does not define any mechanism, operation, algorithm, etc. that S performs. Constructors like S, and coconstructors like P, are not functions.)
This definition/codefinition answers our original question directly. Every n:Nat is equal to S(Pn), which is in canonical form.
I haven't said much about what coinduction really is, or why we should think of P as a coconstructor, etc. I'll address that in another post.
(Aside: some writers define "canonical form" as a form containing only canonical constructors, e.g. SSSZ; others defined it as one whose outermost form is a canonical constructor, e.g. Sn is in canonical form.)
