一句话：提出并证明自然数与整数算术的数据类型定义重写系统（DDRS），覆盖一元、二进制和十进制视图的 ground-complete 重写规则。
论文研究如何用代数等式规格定义数据类型，并将其从左到右解释为项重写系统，且要求该系统 ground-complete。作者首先为整数环定义两个各含十二条规则的数据类型定义重写系统（DDRS），并证明其 ground-completeness。随后，他们引入按一元视图指定的自然数与整数算术，即基于后缀一元追加构造子的算术；接着指定基于二进制和十进制记法的算术，其特点是每个范式都类似常见数字表示：单个数字、无前导零的数字串，或其负数形式。二进制和十进制记法下的整数算术基于后缀数字追加函数。对每种视图，作者定义 DDRS，并表明所得数据类型是扩展自然数规范项代数的规范项代数。然后，针对每种视图，还考虑基于树构造子的替代 DDRS，其范式可比，但表达式在算法上更复杂。所有考虑的 DDRS 均被证明具有 ground-completeness。
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.Comment: arXiv admin note: text overlap with arXiv:1406.3280
@article{paperbot1334,
title = {Datatype defining rewrite systems for naturals and integers},
author = {Jan A. Bergstra and Alban Ponse},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:17)2021}
}