三个扩展自然数数据类型的整数数据类型定义重写系统
Three Datatype Defining Rewrite Systems for Datatypes of Integers each extending a Datatype of Naturals
摘要：
十进制算术是根据三种视图指定的：一元、二进制和十进制表示法。二进制和十进制观点的特点是，每个范式都类似于普通的数字表示法，也就是说，要么是一个数字，要么是一串没有前导零的数字，要么是后者的否定版本。一元视图包括基于0的整数算术规范、后继函数$S$和前导函数，具有负范式$-S^i(0)$。在二进制和十进制记数法中的算术运算是基于（后缀）数字追加函数。对于每个视图，我们定义了一个地面汇合和终止的数据类型定义重写系统（DDRS），在每种情况下，所得到的数据类型是一个典型的项代数，扩展了相应的规范项代数自然数。然后，对于每个视图，我们考虑一个替代DDRS的基础上，产生可比的范式，这对于二进制和十进制的观点承认，在算法上更涉及的表达式的树构造器。纳入这些DDRS是因为它们更接近现有文献。对于这些DDRS，我们还提供接地完整性结果。最后，我们定义了一个DDRS的整数环（包括15个重写规则），并证明了它的地面完全性。
英文摘要：
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 $S$, and predecessor function, with negative normal forms $-S^i(0)$. 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
