A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
Jan A Bergstra, John V Tucker
TL;DR
This work provides a finite, sound, and complete equational axiomatisation for the equational theory of common meadows—arithmetic data types formed by extending fields with an absorptive error element $\bot$ and a total division operator. By introducing fracterms and a fracterm-flattening mechanism, the authors reduce arbitrary terms to flat fractions over polynomial-sumterm representations, enabling a constructive completeness proof and decidability of the theory. The development connects classical ring/field theory with computational needs, offering a rigorous algebraic foundation for reasoning about division by zero and errors in programming semantics, and highlighting applications in formal verification and abstract data type theory. The paper also outlines the broader research programme, compares common meadows with alternative totalisation schemes, and poses several open questions for future exploration.
Abstract
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.