| Summary: | A datatype defining rewrite system (DDRS) is an algebraic (equational)
specification intended to specify a datatype. When interpreting the equations
from left-to-right, a DDRS defines a term rewriting system that must be
ground-complete. First we define two DDRSs for the ring of integers, each
comprising twelve rewrite rules, and prove their ground-completeness. Then we
introduce natural number and integer arithmetic specified according to unary
view, that is, arithmetic based on a postfix unary append constructor (a form
of tallying). Next we specify arithmetic based on two other views: binary and
decimal notation. The binary and decimal view have as their characteristic that
each normal form resembles common number notation, that is, either a digit, or
a string of digits without leading zero, or the negated versions of the latter.
Integer arithmetic in binary and decimal notation is based on (postfix) digit
append functions. For each view we define a DDRS, and in each case the
resulting datatype is a canonical term algebra that extends a corresponding
canonical term algebra for natural numbers. Then, for each view, we consider an
alternative DDRS based on tree constructors that yields comparable normal
forms, which for that view admits expressions that are algorithmically more
involved. For all DDRSs considered, ground-completeness is proven.
|
|---|