We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value $\bot$ whose main purpose is to always return a value for division. To rings and fields, we add a division operator $x/y$ and study a class of algebras called common meadows wherein $x/0 = \bot$. The set of equations true in all common meadows is named the equational theory of common meadows. We give a finite equational axiomatisation of the equational theory of common meadows and prove that it is complete and that the equational theory is decidable.
翻译:我们分析了模拟带有错误概念的数值结构的抽象数据类型。具体而言,我们关注包含一个错误值 $\bot$ 的算术数据类型,其主要目的是始终为除法返回一个值。在环和域的基础上,我们添加了一个除法算子 $x/y$,并研究了一类称为公共牧场的代数结构,其中 $x/0 = \bot$。所有公共牧场中成立的等式集合被称为公共牧场的等式理论。我们给出了公共牧场等式理论的一个有限等式公理化,并证明其是完备的,且该等式理论是可判定的。