Abstract
We give algebraic presentations of the sets of natural numbers, integers, and rational numbers by convergent rewrite systems which moreover allow efficient computations of arithmetical expressions. We then use such systems in the general normalised completion algorithm, in order to compute Gröbner bases of polynomial ideals over ℚ.
This research was supported in part by the EWG CCL II, the HCM Network CON-SOLE, and the “GDR de programmation du CNRS”.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
L. Bachmair and H. Ganzinger. Buchberger's algorithm: A constraint-based completion procedure. In J.-P. Jouannaud, editor, First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 285–301, München, Germany, Sept. 1994. Springer-Verlag.
R. V. Book, editor. 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, Como, Italy, Apr. 1991. Springer-Verlag.
A. Boudet, E. Contejean, and C. Marché. AC-complete unification and its application to theorem proving. In Ganzinger [15], pages 18–32.
B. Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Ideal. PhD thesis, University of Innsbruck, Austria, 1965. (in German).
B. Buchberger. History and basic features of the critical pair / completion procedure. Journal of Symbolic Computation, 3(1), Feb. 1987.
B. Buchberger and R. Loos. Algebraic simplification. In Computer Algebra, Symbolic and Algebraic Computation. Computing Supplementum 4. Springer-Verlag, 1982.
R. Bündgen. Simulating Buchberger's algorithm by a Knuth-Bendix completion procedure. In Book [2].
R. Bündgen. Term Completion versus Algebraic Completion. PhD thesis, Universität Tübingen, 1991.
T. Chen and S. Anantharaman. Storm: A many-to-one associative-commutative matcher. In J. Hsiang, editor, 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, Kaiserslautern, Germany, Apr. 1995. Springer-Verlag.
D. Cohen and P. Watson. An efficient representation of arithmetic for term rewriting. In Book [2], pages 240–251.
E. Contejean and C. Marché. CiME: Completion Modulo E. In Ganzinger [15], pages 416–419. System Description available at http://www.lri.fr/∼demons/cime.html.
E. Contejean, C. Marché, and L. Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. Research report, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, 1997.
F.-J. de Vries and J. Yamada. On termination of rewriting with real numbers. In M. Takeichi, editor, Functional Programming II, JSSST'94, volume 10 of Lecture Notes on Software Gaku. Kindai-kagaku-sya, Tokyo, Nov. 1994.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.
H. Ganzinger, editor. 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, New Brunswick, NJ, USA, July 1996. Springer-Verlag.
A. Kandri-Rody, D. Kapur, and F. Winkler. Knuth-Bendix procedure and Buchberger algorithm — a synthesis. In Proc. of the 20th Int. Symp. on Symbolic and Algebraic Computation, Portland, Oregon, pages 55–67, 1989.
D. E. Knuth. The art of computer programming, volume 2. Addison-Wesley, 2nd edition, 1981.
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.
P. Le Chenadec. Canonical forms in finitely presented algebras. Pitman, London, 1986.
R. Loos. Term reduction systems and algebraic algorithms. In Proceedings of the Fifth GI Workshop on Artificial Intelligence, pages 214–234, Bad Honnef, West Germany, 1981. Available as Informatik Fachberichte, Vol. 47.
C. Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253–288, 1996.
L. Pottier. Algorithmes de complétion et généralisation en logique du premier ordre. Thèse de doctorat. Université de Nice, 1989.
L. Rabehasaina. Systèmes de réécriture pour l'arithmétique. Rapport de stage de magistère, Université Paris-sud, 1996.
H. R. Walters. A complete term rewriting system for decimal integer arithmetic. Tech. Report CS-9435, CWI, Amsterdam, 1994.
H. Zantema. Termination of term rewriting by semantic labelling. Technical Report 92-38, RUU-CS, University Utrecht, Dec. 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Contejean, E., Marché, C., Rabehasaina, L. (1997). Rewrite systems for natural, integral, and rational arithmetic. In: Comon, H. (eds) Rewriting Techniques and Applications. RTA 1997. Lecture Notes in Computer Science, vol 1232. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62950-5_64
Download citation
DOI: https://doi.org/10.1007/3-540-62950-5_64
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62950-4
Online ISBN: 978-3-540-69051-1
eBook Packages: Springer Book Archive