The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Wednesday 21 October 2009 11:49:18 am Edsko de Vries wrote:
> Is there an accessible reference to the use of ordinal induction in
> type theory? For example, an introduction to Brouwer ordinals and
> induction on them? (This would be ordinal induction, right?)
> 
> Also, if I can ask a potentially very stupid question: is there a
> relation between ordinal induction and coinduction?

I'm no expert on this, but I'd tentatively answer your last question as "no". 
The encoding of the ordinals I'm familiar with is:

    O = 0 | S O | Lim (Nat -> O) (*)

taken inductively. That definition actually corresponds almost exactly to 
their use in a blog post by Dan Piponi:

  http://blog.sigfpe.com/2008/10/whats-use-of-transfinite-ordinal.html

where he talks about using transfinite ordinals to prove the termination of 
one player games. 0 corresponds to game over. 'S o' is a game where you can 
make a single move, followed by playing 'o', or, I suppose you could peel off 
multiple Ss as a single 'move', if that's how you choose to interpret things. 
Finally, you have limit ordinals, and the moves you're allowed to make for 
those are to choose any ordinal less than/contained in the limit, and then 
play that game.

But, those are essentially the three cases for induction of the above type. 0 
means you've arrived at the end. You can peel off Ss as another case. And for 
a limit ordinal, you must choose some ordinal(s) less than the limit, by 
calling the relevant function and proceeding by induction on those. And of 
course, the whole point of the above association of ordinals with these games 
is to prove their ultimate termination. Limit ordinals represent points in 
the 
process where there is no finite bound on the size of the sub-problem, but 
the 
sub-problems are nevertheless finite (in some sense. Obviously in ω^ω, the 
sub-problem ω^n is transfinite, but we've chosen some finite exponent from 
the 
unbounded set of exponents to continue with).

In particular, there's no way to do induction on these ordinals to, say, 
build 
a list with omega-many elements by consing, which is the sort of thing that's 
representable by coinduction (of course, even with coinduction, you never 
actually get to do anything infinitely many times. We might conceive of 
streams as having infinitely many elements, but a program will only ever be 
able to inspect a finite number of them).

A somewhat related set of types are the so-called W-types, defined as the 
inductive fixed point:

    W A T = Σ x:A (T x → W A T)

These are also called well-founded trees. In fact, the definition of the 
ordinals above is a special case, like so (a lot of inductive types are a 
special case of W-types, actually, except that they don't gel very well with 
intensional equality):

    A is a type with 3 elements: 0, 1 and 2
    T 0 = ⊥ (the type with no elements)
    T 1 = ⊤ (the type with one element)
    T 2 = Nat

    Z     = (0 , absurd)
    S n   = (1 , const n)
    Lim f = (2 , f)

Some time ago, when I was trying to figure out W-types (and I still don't 
have 
much intuition about them), I was confused about what kept them from being 
infinite (in depth). But it's the same thing as the ordinals, and what makes 
these different from coinductive types: their values can't refer to 
themselves 
in their own definition, since they're inductive, of course. This is true 
even 
in inductives that contain functions. So, for instance, you can't write 
something like:

   inf := Lim (fun n => inf)

So all Os and W-types are well-founded in this way, and you can only build up 
a finitely deep structure of them, and so induction on them eventually 
terminates.

Of course, there may be other encodings of ordinals in type theory, but I 
don't think you'll get something like coinduction from them unless the 
encoding is in some way coinductive (whether actually coinductive, or 
mimicking coinduction with existential quantification).

I hope that made some sense. :)

-- Dan

(*) This isn't a completely adequate type, of course. There are elements that 
don't really correspond to a proper ordinal, like 'Lim f' where:

  f(n) = n mod 2

But I haven't fooled with a more exact representation enough to know how 
they'd end up. Even if you tighten up the requirements for f to be monotone, 
there are lots of duplicate elements, since:

  f(n) = n

and

  f(n) = n + 1

both represent the same limit ordinal.