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.

Applicative Programming (acm D.1.1), Semantics of Programming Languages (acm F.3.2)
Theory of computing (msc 68Qxx), Grammars and rewriting systems (msc 68Q42), Abstract data types; algebraic specification (msc 68Q65)
CWI
Department of Computer Science [CS]
Extensible programming environments

Walters, H.R, & Zantema, H. (1995). Rewrite systems for integer arithmetic. Department of Computer Science [CS]. CWI.