Algorithms for Ordinal Arithmetic
Panagiotis Manolios and Daron Vroon.
Nineteenth International Conference on Automated Deduction (CADE), pages 243-257. Springer-Verlag, July 2003. © Springer-Verlag.
Abstract
Proofs of termination are essential for establishing the correct
behavior of computing systems. There are various ways of
establishing termination, but the most general involves the use
of ordinals. An example of a theorem proving system in which
ordinals are used to prove termination is ACL2. In ACL2, every
function defined must be shown to terminate using the ordinals up
to epsilon0. We use a compact notation for the ordinals up
to epsilon0 (exponentially more succinct than the one used by
ACL2) and define efficient algorithms for ordinal addition,
subtraction, multiplication, and exponentiation. In this paper
we describe our notation and algorithms, prove their correctness,
and analyze their complexity.
Gzipped Postscript (87K) © Springer-Verlag.
PDF (233K) © Springer-Verlag.
Postscript (230K) © Springer-Verlag.