Complete term rewrite systems for decimal arithmetic and other total recursive functions
Richard Kennaway · 2007
We present a strongly normalising and confluent term rewrite system which describes addition, subtraction, and multiplication of positive and negative integers represented in base 10. We prove a general theorem giving an easily checkable syntactic condition on term rewrite systems which implies strong normalisation. The rewrite system for decimal arithmetic satisfies the condition. The method immediately extends to allow, for any definition of a total recursive function on integers, the construction of a strongly normalising term rewrite system which represents that function.