Ancillary-file links:
Ancillary files (details):
- INT1Proof.html
- INT2.trs
- INT2Proof.html
- INTbt.trs
- INTbtProof.html
- INTbud.trs
- INTbudProof.html
- INTdt.trs
- INTdtProof.html
- INTdub.trs
- INTdubProof.html
- INTubd.trs
- INTubdProof.html
- INTut.trs
- INTutProof.html
- NAT1.trs
- NAT1Proof.html
- NAT2.trs
- NAT2Proof.html
- NATbt.trs
- NATbtProof.html
- NATbud.trs
- NATbudProof.html
- NATdt.trs
- NATdtProof.html
- NATdub.trs
- NATdubProof.html
- NATubd.trs
- NATubdProof.html
- NATut.trs
- NATutProof.html
- index.html
References & Citations
Computer Science > Logic in Computer Science
Title: Datatype defining rewrite systems for naturals and integers
(Submitted on 22 Aug 2016 (v1), last revised 17 Feb 2021 (this version, v6))
Abstract: 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.
Submission history
From: Antoine Amarilli [view email] [via LOGICAL proxy][v1] Mon, 22 Aug 2016 16:25:23 GMT (12kb)
[v2] Mon, 13 Jan 2020 15:29:52 GMT (28kb)
[v3] Tue, 14 Jul 2020 17:51:54 GMT (34kb)
[v4] Fri, 8 Jan 2021 13:58:28 GMT (27kb)
[v5] Thu, 14 Jan 2021 14:52:55 GMT (261kb,A)
[v6] Wed, 17 Feb 2021 13:57:55 GMT (267kb,AD)
Link back to: arXiv, form interface, contact.