arithmetical data type;
division by zero;
error value;
common meadow;
fracterm;
fracterm calculus;
equational theory;
FRACTIONS;
D O I:
10.1145/3689211
中图分类号:
TP301 [理论、方法];
学科分类号:
081202 ;
摘要:
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 perpendicular to 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 = perpendicular to. 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.