Datatype defining rewrite systems for naturals and integers

摘要

A datatype defining rewrite system (DDRS) is an algebraic (equational)specification intended to specify a datatype. When interpreting the equationsfrom left-to-right, a DDRS defines a term rewriting system that must beground-complete. First we define two DDRSs for the ring of integers, eachcomprising twelve rewrite rules, and prove their ground-completeness. Then weintroduce natural number and integer arithmetic specified according to unaryview, that is, arithmetic based on a postfix unary append constructor (a formof tallying). Next we specify arithmetic based on two other views: binary anddecimal notation. The binary and decimal view have as their characteristic thateach normal form resembles common number notation, that is, either a digit, ora string of digits without leading zero, or the negated versions of the latter.Integer arithmetic in binary and decimal notation is based on (postfix) digitappend functions. For each view we define a DDRS, and in each case theresulting datatype is a canonical term algebra that extends a correspondingcanonical term algebra for natural numbers. Then, for each view, we consider analternative DDRS based on tree constructors that yields comparable normalforms, which for that view admits expressions that are algorithmically moreinvolved. For all DDRSs considered, ground-completeness is proven.