Three Datatype Defining Rewrite Systems for Datatypes of Integers each extending a Datatype of Naturals
arXiv:1406.3280
Abstract
Integer arithmetic is specified according to three views: unary, 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. The unary view comprises a specification of integer arithmetic based on 0, successor function , and predecessor function, with negative normal forms . Integer arithmetic in binary and decimal notation is based on (postfix) digit append functions. For each view we define a ground-confluent and terminating datatype defining rewrite system (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 yield comparable normal forms, which for that binary and decimal view admits expressions that are algorithmically more involved. These DDRSes are incorporated because they are closer to existing literature. For these DDRSes we also provide ground-completeness results. Finally, we define a DDRS for the ring of Integers (comprising fifteen rewrite rules) and prove its ground-completeness.
33 pages; 19 tables. All DDRSes in S.2 are proven ground-complete (gc). In S.3, the DDRS for Z_{ut} contains 16 equations and is proven gc; the DDRS for Z_{bt} has one more equation ([bt22]) and is proven gc; the DDRSes for N_{dt} (Table 14) and Z_{dt} (Table 16) are proven gc in [13]. In Appendix C, corrected versions of the DDRSes for N_{u'} and Z_{u'} are proven gc