Ordinal induction

[Edsko de Vries-3]

Hi,

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?

Thanks,

Edsko

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Dan Doel]

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.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Danko Ilik]

> 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?)

Maybe this coq contrib is relevant:
http://coq.inria.fr/distrib/current/contribs/Cantor.html

--
Danko Iliḱ

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Nils Anders Danielsson-3]

On 2009-10-21 16:49, Edsko de Vries wrote:
> Also, if I can ask a potentially very stupid question: is there a
> relation between ordinal induction and coinduction?

A function from the natural numbers can be seen as a coinductively
defined structure. Peter Hancock recently mentioned the following
definition of the Brouwer ordinals:

  mu X. nu Y. 1 + X * Y

  (http://article.gmane.org/gmane.comp.lang.agda/953)

--
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Edsko de Vries-4]

Hi Dan,

Thank you for your extensive answer. Much appreciated. The link to Dan  
Piponi's blog post was also very helpful. I think I have a better  
understanding of ordinals now.

Thanks again,

Edsko

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Dan Doel]

On Thursday 22 October 2009 9:50:18 am Edsko de Vries wrote:
> Thank you for your extensive answer. Much appreciated. The link to Dan
> Piponi's blog post was also very helpful. I think I have a better
> understanding of ordinals now.

Incidentally, while googling for Brouwer ordinal (which is, apparently, the
formulation I talked about), I came across this short paper which looks pretty
interesting:

  http://www.cs.nott.ac.uk/~pgh/nc.ps

It centers around the idea that you can keep extending my O:

  O₀ = 1 + O₀ = ℕ
  O₁ = O₀ + (O₀ → O₁)
  O₂ = O₁ + (O₁ → O₂)
  ⋮

where these are all intended to be inductive fixed points. So now we have a ℕ-
indexed series of ordinal encodings. Can we build an O-indexed one? We can:

  O_α = Σ β<α O_β ~ O_(lim f) = Σ n:ℕ O_(f n)

So now we have an O-indexed series of ordinal encodings, and O = O₁. Can we
have an O₂ indexed series? And so on. It also turns out you can use a modified
(for convenience) W-type constructor to express the above series. If I
understand correctly, it's:

  W A T = Z | S (W A T) | Sup (x:A) (T x -> W A T)

  O_i = W (Fin i) (n ↦ O_n)

for i : ℕ, at least, where 'Fin i' is the finite set with i elements (in the
case of i = 0, n ↦ O_n is intended to be the empty function, since Fin 0 is
empty). The author ties all this together with an inductive-recursive
definition of a type On, which in some sense represents the union of an On-
indexed series of ordinal representations. Ordinal arithmetic can be defined
almost identically to arithmetic on O in my previous message.

I'm not really sure how much further this goes in modeling the behavior of the
ordinals. However, it still doesn't get you coinduction-like behavior (I'm
pretty sure). The inductive case for a limit ordinal still represents a choice
to progress to some unbounded but well-founded and lesser value(s). So even
though we have ordinals that live unions of ordinal-indexed families, each
particular ordinal can be seen as corresponding to some ultimately terminating
procedure.

Cheers,

-- Dan

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Edsko de Vries-4]

Hi Dan,

Thanks for the additional reference and your explanation. I will have  
to take some time to study it, but I am now convinced that you are  
right: since the ordinals are well-founded, ordinal induction is just  
well-founded induction and therefore describes a terminating process.

It would be nice to see how ordinals can be used to do some (simple)  
proofs in Coq. While preparing a talk about ordinals for our research  
students (http://www.cs.tcd.ie/Edsko.de.Vries/talks/ordinals.pdf) I  
defined a small process language with an infinitely branching choice  
operator. I figured that I wouldn't be able to write an evaluator for  
this language in Coq because I thought that for a constructor (Sum :  
(nat -> Proc) -> Proc) of the language, given (Sum f), (f n) would not  
considered to be a subterm. Then I could do a termination proof using  
ordinals and then define the evaluator by transfinite recursion. But  
of course, it turns out that (f n) *is* considered a subterm and so  
the evaluator is easily definable :)

In fact, the whole reason I started looking at ordinals was a proof  
about modal logic and bisimulation, which Milner did by transfinite  
induction on the depth of the formula (which has an infinitely  
branching conjunction, and the depth must therefore be an ordinal).  
But since the depth of the trees is always finite (even if we cannot  
compute it without ordinals), 'ordinary' structural induction on these  
formulae should suffice (just like I could do structural induction on  
my process language). (Milner uses the depth to index the bisimulation  
too, so he has a separate need for it.)

Anyway, I feel a lot happier about transfinite induction now! Thanks  
again,

Edsko

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club