A Complete Term Rewriting System for Decimal Integer Arithmetic
H. R. Walters · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1994
We present a term rewriting system for decimal integers with addition and subtraction. We prove that the system is confluent and terminating. CR Subject Classification (1991): D.1.1 [Programming Techniques]: Applicative (Functional) Programming; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages, Algebraic approaches to semantics. AMS Subject Classification (1991): 68Q40: Symbolic computation, 68Q42: Rewriting Systems and 68Q65: Algebraic specification. Keywords & Phrases: integers, term rewriting, specification languages, formal semantics, confluence, termination. 1. Introduction In [CW91] a term rewriting system is presented of the integers with addition and multiplication. This specification is proved to be locally confluent using the LP theorem prover (Larch Prover). Termination is not established, and it is shown why common termination proof methods (Knuth Bendix Ordering and Recursive Path Ordering) fail on this rewrite system. The termination of that ...