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 ε 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Beckmann, A., Buss, S.R., Pollett, C.: Ordinal notations and well-orderings in bounded arithmetic. Annals of Pure and Applied Logic, 197–223 (2003)
Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 275–293. Springer, Heidelberg (1996)
Cantor, G.: Beiträge zur Begründung der transfiniten Mengenlehre. Mathematische Annalen xlvi, 481–512 (1895)
Cantor, G.: Beiträge zur Bgründung der transfiniten Mengenlehre. Mathematische Annalen xlix, 207–246 (1897)
Cantor, G.: Contributions to the Founding of the Theory of Transfinite Numbers. Dover Publications, Inc., New York (1952); Translated by P.E.B. Jourdain
Church, A., Kleene, S.C.: Formal definitions in the theory of ordinal numbers. Fundamenta mathematicae 28, 11–21 (1937)
Dershowitz, N.: Trees, ordinals, and termination. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 243–250. Springer, Heidelberg (1993)
Dershowitz, N., Okada, M.: Proof-theoritic techniques for term rewriting theory. In: 3rd IEEE Symp. on Logic in Computer Science, pp. 104–111 (1988)
Dershowitz, N., Reingold, E.M.: Ordinal arithmetic with list structures. In: Logical Foundations of Computer Science, pp. 117–126 (1992)
Devlin, K.: The Joy of Sets: Fundamentals of Contemporary Set Theory, 2nd edn. Springer, Heidelberg (1992)
Gallier, J.H.: What’s so special about Kruskal’s theorem and the ordinal Γ0? A survey of some results in proof theory. Annals of Pure and Applied Logic, 199–260 (1991)
Gentzen, G.: Die widerspruchsfreiheit der reinen zahlentheorie. Mathematische Annalen 112, 493–565 (1936); English translation in Szabo, M. E. (ed.) The Collected Works of Gerhard Gentzen, pp. 132–213. North Holland, Amsterdam (1969)
Greve, D.A.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 321–333. Springer, Heidelberg (1998)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Moore, J.S.: ACL2 homepage, See URL http://www.cs.utexas.edu/users/moore/acl2
Kaufmann, M., Moore, J.S. (eds.): Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29 (November 2000)
Kunen, K.: Set Theory - an Introduction to Independence Proofs. Studies in Logic and the Foundations of Mathematics, vol. 102. North-Holland, Amsterdam (1980)
Manolios, P.: Correctness of pipelined machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 161–178. Springer, Heidelberg (2000)
Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin (August 2001)
Manolios, P., Namjoshi, K., Sumners, R.: Linking theorem proving and modelchecking with well-founded bisimulation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 369–379. Springer, Heidelberg (1999)
Manolios, P., Vroon, D.: Ordinal arithmetic in ACL2. Submitted to the 4th International Workshop on the ACL2 Theorem Prover and Its Applications (2003)
Medina-Bulo, I., Palomo-Lozano, F., Alonso-Jimenez, J.A.: Implementation in ACL2 of well-founded polynomial orderings. In: Kaufmann, M., Moore, J.S. (eds.) Proceedings of the ACL2 Workshop 2002 (2002)
Miller, L.W.: Normal functions and constructive ordinal notations. Journal of Symbolic Logic 41, 439–459 (1976)
Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the AMD5 K 86 floating-point division program. IEEE Trans. Comp. 47(9), 913–926 (1998)
Rogers Jr., H.: Theory of Recursive Functions and Effective Computability, 1st paperback edn. MIT Press, Cambridge (1987)
Ruiz-Reina, J.-L., Alonso, J.-A., Hidalgo, M.-J., Martin, F.-J.: Multiset relations: A tool for proving termination. In: Kaufmann, M., Moore, J.S. (eds.) [17]
Russinoff, D.M.: A mechanically checked proof of IEEE compliance of a registertransfer- level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. London Mathematical Society Journal of Computation and Mathematics 1, 148–200 (1998)
Schütte, K.: Proof Theory. Springer, Heidelberg (1977); Translated by J. N. Crossley from the revised version of Beweistheorie, 1st edn. (1960)
Setzer, A.: Ordinal systems. In: Cooper, B., Truss, J. (eds.) Sets and Proofs, pp. 301–331. Cambridge University Press, Cambridge (1999)
Setzer, A.: Ordinal systems part 2: One inaccessible. In: Logic Colloquium 1998. ASL Lecture Notes in Logic, vol. 13, pp. 426–448 (2000)
Sumners, R.: An incremental stuttering refinement proof of a concurrent program in ACL2. In: Kaufmann, M., Moore, J. (eds.) [17]
Sustik, M.: Proof of Dixon’s lemma using the ACL2 theorem prover via an explicit ordinal mapping 2003. In: Submitted to the 4th International Workshop on the ACL2 Theorem Prover and Its Applications (2003)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)
Veblen, O.: Continuous increasing functions of finite and transfinite ordinals. Transactions of the American Mathematical Society 9, 280–292 (1908)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manolios, P., Vroon, D. (2003). Algorithms for Ordinal Arithmetic. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive