自然数和整数的数据类型定义重写系统
摘要：数据类型定义的重写系统（DDRS）是一个代数（等式）规范，用于指定数据类型。从左到右解释等式时，DDRS定义了一个必须是地面完整的项重写系统。首先，我们为整数环定义了两个包含十二个重写规则的DDRS，并证明了它们的地面完整性。然后，我们根据一元视图引入基于后缀一元追加构造器（一种记数法）的自然数和整数算术。接下来，我们根据二进制和十进制视图来指定算术。二进制和十进制视图的特点是，每个正规形式都类似于常见的数字表示法，即一个数字，或者一个没有前导零的数字字符串，或者后者的否定版本。二进制和十进制表示法中的整数算术是基于（后缀）数字追加函数的。对于每个视图，我们定义了一个DDRS，而且在每种情况下，所得到的数据类型都是扩展了相应的自然数的规范术语代数。然后，对于每个视图，我们考虑了基于树构造器的另一种DDRS，该构造器产生可比较的正规形式，该形式允许该视图中更加复杂的表达式。对于所有考虑的DDRS，都证明了其地面完整性。
作者：Jan A. Bergstra and Alban Ponse
论文ID：1608.06212
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22