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$。在所有公共牧场中均成立的等式集合被称为公共牧场的等式理论。我们给出了公共牧场等式理论的一个有限等式公理化,并证明了该公理化的完备性以及该等式理论的可判定性。