Jan A. Bergstra ; Alban Ponse - Datatype defining rewrite systems for naturals and integers

lmcs:6031 - Logical Methods in Computer Science, February 18, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:17)2021
Datatype defining rewrite systems for naturals and integers

Authors: Jan A. Bergstra ; Alban Ponse

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.

Volume: Volume 17, Issue 1
Published on: February 18, 2021
Submitted on: January 15, 2020
Keywords: Computer Science - Logic in Computer Science,D.3.1


Consultation statistics

This page has been seen 121 times.
This article's PDF has been downloaded 70 times.