Rewrite systems for integer arithmetic

Abstract

We present three term rewrite systems for integer arithmetic with addition, multiplication, and, in two cases, subtraction. All systems axe 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.