Abstract
We present three term rewrite systems for integer arithmetic with addition, multiplication, and, in two cases, subtraction. All systems are ground confluent and terminating; termination is proved by semantic labelling and recursive path order.
The first system represents numbers by successor and predecessor. In the second, which defines non-negative integers only, digits are represented as unary operators. In the third, digits are represented as constants. The first and the second system are complete; the second and the third system have logarithmic space and time complexity, and are parameterized for an arbitrary radix (binary, decimal, or other radices). Choosing the largest machine representable single precision integer as radix, results in unbounded arithmetic with machine efficiency.
Partial support received from the Foundation for Computer Science Reasearch in the Netherlands (SION) under project 612-17-418, “Generic Tools for Program Analysis and Optimization”.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley, 1984.
L.G. Bouma and H.R. Walters. Implementing algebraic specifications. In J.A. Bergstra, J. Heering, and P. Klint, editors, Algebraic Specification, ACM Press Frontier Series, pages 199–282. The ACM Press in co-operation with Addison-Wesley, 1989. Chapter 5.
D. Cohen and P. Watson. An efficient representation of arithmetic for term rewriting. In R. Book, editor, Proceeding of the Fourth International Conference on Rewriting Techniques and Application (Como, Italy), LNCS 488, pages 240–251. Springer Verlag, Berlin, 1991.
N. Dershowitz. Termination of rewriting. J. Symbolic Computation, 3(1&2):69–115, Feb./April 1987. Corrigendum: 4, 3, Dec. 1987, 409–410.
N. Dershowitz, J.-P. Jouannaud, and J.W. Klop. More Problems in Rewriting. In C. Kirchner, editor, Proceeding of the Fifth International Conference on Rewriting Techniques and Application (Montreal, Canada), LNCS 690. Springer Verlag, Berlin, 1993.
S.J. Garland and J.V. Guttag. A Guide to LP, The Larch Prover. MIT, November 1991.
J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Volume 2., pages 1–116. Oxford University Press, 1992.
H.R. Walters. Hybrid implementations of algebraic specifications. In H. Kirchner and W. Wechler, editors, Proceedings of the Second International Conference on Algebraic and Logic Programming, volume 463 of Lecture Notes in Computer Science, pages 40–54. Springer-Verlag, 1990.
H.R. Walters. A complete term rewriting system for decimal integer arithmetic. Technical Report CS-9435, Centrum voor Wiskunde en Informatica, 1994. Available by ftp from ftp.cwi.nl:/pub/gipe as Wal94.ps.Z.
H. Zantema. Termination of term rewriting by semantic labelling. Technical Report RUU-CS-93-24, Utrecht University, July 1993. Accepted for publication in Fundamenta Informaticae.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Walters, H.R., Zantema, H. (1995). Rewrite systems for integer arithmetic. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_67
Download citation
DOI: https://doi.org/10.1007/3-540-59200-8_67
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59200-6
Online ISBN: 978-3-540-49223-8
eBook Packages: Springer Book Archive