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 ε0. We use a compact notation for the ordinals up to ε0 (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.
CITATION STYLE
Manolios, P., & Vroon, D. (2003). Algorithms for ordinal arithmetic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 243–258). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_19
Mendeley helps you to discover research relevant for your work.