[FOM] Fwd: invitation to comment

[Hendrik Boom]

On Tue, May 24, 2011 at 12:41:26AM +0200, Jeffrey Sarnat wrote:
> >
> As a computer scientist, I found Cantor normal form for epsilon_0 to be easy
> to understand once I realized that exponentiation at base omega is exactly
> the multiset ordering from term rewriting theory. If we choose to implement
> multisets as lists sorted in descending order, then this becomes even more
> straightforward: the empty list is smaller than all non-empty lists, and
> non-empty lists are ordered lexicographically by their heads followed by
> their tails. Moreover, ordinal addition and multiplication are easy to
> explain in terms of their type-theoretic analogs, which makes it easy to
> visualize how data structures built up from these three primitives would be
> ordered, and why the resulting ordering should be well founded (although
> multiplication is technically unnecessary, it is pedagogically helpful to
> consider).
> 
> My experiences with introducing other computer scientists to the dark art of
> ordinal analysis have led me to believe that this approach works well: I can
> usually get people to count at least as high as Gamma_0 in about an hours
> worth of hand-waiving along these lines. For those who are interested, a
> (slightly) more detailed account of this approach can be found in Section
> 3.1 of my dissertation.
> 
>         Jeff Sarnat
>         http://www.pps.jussieu.fr/~sarnat/

I found that ordinal exponentiation and the resulting polynomials was 
useful in proving termination when committing the program transformation 
that uses a stack to implement recursion.

-- hendrik