1 Introduction
Arithmetical structures are many and varied. Classically, we think of the integers
$\mathbb {Z}$
, rationals
$\mathbb {Q}$
, reals
$\mathbb {R}$
, and complex numbers
$\mathbb {C}$
, as well as modular arithmetics
$\mathbb {Z}_n$
, p-adics and derived systems. To these should be added a number of arithmetical structures developed for computer programming such as fixed point, floating point and interval arithmetics. Whilst the algebra of the classical structures is very well understood through the axiomatic theories of rings and fields, the algebra of the computer arithmetics is barely developed. This is a problem as the algebraic properties of these structures are fundamental in specifying, designing and reasoning about computer programs, e.g., in predicting precision, anticipating and finding errors, and subsequent validation and verification.
In a series of papers, we have been investigating a few key semantic features of computer arithmetics and exploring their algebraic properties [Reference Bergstra and Tucker9, Reference Bergstra and Tucker10, Reference Bergstra, Tucker and Roggenbach11, Reference Bergstra and Tucker16, Reference Bergstra, Tucker and Jansen17]. Our approach is to start from field theory, especially the field of rational numbers, and impose algebraic conditions on fields that represent some of the semantic constraints placed on computer arithmetics, such as bounds, finiteness, and the need for additional operations. To develop a theory of arithmetical abstract data types for computer programming, we apply methods that have been developed from universal algebra and logic.
So, the axiomatic concept of a field has a number of shortcomings as a specification of an arithmetical structure for computing. First, a field is a commutative ring with 1 in which all non-zero elements are invertible. Thus, strictly speaking, division is not an operator in a field. Thus, we add division
$x \div y$
to the primary field operations of
$x + y, - x, x \cdot y$
to make an algebra we call a meadow [Reference Bergstra and Tucker9]. Secondly, in computing, applying an operator must return a value for all of its arguments, i.e., an operator must be a total function. Thus, for our meadows we must find a way of defining a value for
$x \div 0$
.
1.1 Totalising division
We have studied several ways of making division total in a meadow. Although the possible semantics and their algebra and logic ramify, the methods of study cohere and begin to form a subject with diverse results and applications: see Section 10 for some of this background. Of those we have studied, one semantics stands out: for all x,
$$ \begin{align*}\ x \div 0 = \bot\end{align*} $$
where
$\bot $
is a new element added to the meadow and having the property of absorption: if
$\bot $
is an argument to any operation then it returns the value
$\bot $
. We can think of
$\bot $
as an error value. Such an algebra we call a common meadow, which has the form of an enlargement of a field F:
$$ \begin{align*}(F \cup \{ \bot \} \ | \ 0, 1, \bot, x+y, -x, x \cdot y, x \div y).\end{align*} $$
A common meadow based upon the rational numbers
$\mathbb {Q}$
can serve as an idealised model of the simple arithmetic of the pocket calculator. Let
$\mathsf {CM}$
be the class of common meadows.
Common meadows were introduced in [Reference Bergstra, Ponse, de Nicola and Hennicker8]. The introduction of
$\bot $
into a field invalidates some key algebraic laws such as
$$ \begin{align*}x + (- x) = 0 \text{ and } x \cdot 0 = 0 \text{ because } x + (- \bot) = x + \bot = \bot \text{ and } x \cdot \bot = \bot. \end{align*} $$
Subsequently, we have found sets of equations to axiomatise calculations in common meadows, among which is a set
$E_{\mathsf {ftc-cm}}$
studied in [Reference Bergstra and Tucker13, Reference Bergstra and Tucker16]; the subscript
$\mathsf {ftc-cm}$
stands for fracterm calculus for common meadows and the equations are listed in Table 1 and 2 in Section 3.3 below. These equations have proved to be a useful tool for understanding the effects of totalising division, intuitively and formally. The axioms are close to classical axioms and entail an important property for working with fractions, called flattening. From the universal algebra and logic of equational axiomatisations, we know much about the class of algebras of
$E_{\mathsf {ftc-cm}}$
, notably its closure under algebraic constructions, its equational and first-order logic, and its model theory (after Birkhoff [Reference Birkhoff18] and Mal’tsev [Reference Mal’tsev26]).
$E_{\mathsf {wcr},\bot }$
: equational axioms for weak commutative rings with
$\bot $
.
$E_{\mathsf {ftc-cm}}$
: Equational axioms for fracterm calculus for common meadows.
1.2 Axiomatising common division
In this paper, we focus on the equational axioms in
$E_{\mathsf {ftc-cm}}$
and, in particular, on the scope of their semantics which extend beyond the common meadows
$\mathsf {CM}$
. First, we examine the consequences of having a total division operation
$x \div y$
on commutative rings rather than fields. We consider two forms of division: the first is derived indirectly from a unary inverse operator, which we will refer to as inverse based common division; later, the second is defined for integral domains directly as a binary operation, which we will refer to as direct common division. Both inverse based common division and directly defined common division are made total by setting
$x/0$
equal to the error value
$\bot $
. In a field the two forms of division are equivalent and so we have the option of using either; this we have done in developing some common meadow theory for which the axiomatisation
$E_{\mathsf {ftc-cm}}$
was designed.
Now, as pointed out in [Reference Dias and Dinis21], in addition to common meadows, the class
$\mathsf {CR_{\div , \bot }}$
of commutative rings with
$1$
equipped with an inverse based common division operator also satisfy
$E_{\mathsf {ftc-cm}}$
. We axiomatise the class of common meadows relative to the commutative rings with inverse common division using this conditional equation, Additional Value Law,
$$ \begin{align*}\mathsf{AVL}: \ \ \frac{1}{x} = \bot \to 0 \cdot x = x.\end{align*} $$
From [Reference Bergstra and Tucker16], we know that
$E_{\mathsf {ftc-cm}}$
is a finite equational base for the equational theory of common meadows from which it follows that
$E_{\mathsf {ftc-cm}}$
is a finite equational base for the equational theory of commutative rings with common division. Here we prove the Theorem (5.1).
Theorem 1.1.
$E_{\mathsf {ftc-cm}}$
provides a complete equational axiomatisation of the conditional equational theory of the class of commutative rings with inverse based common division.
From [Reference Bergstra and Tucker13], we know that
$E_{\mathsf {ftc-cm}}$
is not a finite base for the conditional equational theory of common meadows. Here we show that
$E_{\mathsf {ftc-cm}} + \mathsf {AVL}$
does not axiomatise the conditional equational theory of common meadows. However, on adding a simple proof rule
$\mathsf {R_{cm}}$
to conditional equation logic to define proof system
$\vdash _{R_{cm}}$
we can prove completeness.
Theorem 1.2.
$\mathsf {CM} \models e_1 \wedge e_2 \ldots \wedge e_n \to e$
if, and only if,
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL} \vdash _{\mathsf {R_{cm}}} E \to e_1 \wedge e_2 \ldots \wedge e_n \to e$
.
This leaves us with the open question.
Problem 1.1. Is the conditional equational theory of the class
$\mathsf {CM}$
of common meadows axiomatisable with finitely many conditional equations?
We conjecture the answer: no.
Finally, in contrast to the inverse defined division, we note that the directly defined common division does not satisfy all the axioms of
$E_{\mathsf {ftc-cm}}$
over all rings. Surprisingly, this latter common division does satisfy the equations in
$E_{\mathsf {ftc-cm}}$
under a new equality relation for partial algebras called eager equality [Reference Bergstra and Tucker14, Reference Bergstra and Tucker15].
1.3 Structure of the paper
In Section 2, we describe the totalisation of partial operations by the addition of
$\bot $
in the general case of an arbitrary algebraic structure. In Section 3, we summarise the situation for rings and fields, introducing the division operators based on inverse, and the common meadow axiomatisation
$E_{\mathsf {ftc-cm}}$
and its model class. In Section 4, we prove a number of basic facts about commutative rings with inverse based common division, including results about their relationship with common meadows. In Section 5 we examine some homomorphisms. In Section 6, after some examples, we show that
$E_{\mathsf {ftc-cm}} + \mathsf {AVL}$
alone does not deliver completeness. In Section 7, we customise the logic with a new rule
$\mathsf {R_{cm}}$
to prove the completeness theorem for common meadows above. In Section 8, we look at integral domains and, at this point, we introduce the second form of direct division. In Section 9, we introduce eager equality and observe the validity of
$E_{\mathsf {ftc-cm}}$
for the second form of division. Lastly, in Section 10, we sketch our investigation into the various ways of totalising division, which is the background to this paper.
We need only the basics of ring and field theory [Reference van der Waerden31], universal algebra [Reference Burris and Sankapannavar19, Reference Mal’tsev26, Reference Meinke, Tucker, Abramsky, Gabbay and Maibaum27], and abstract data type theory [Reference Ehrich, Wolf and Loeckx24].
2 Algebras and equations with an absorptive element
The idea of making partial operations total with an absorptive element is quite general. We will summarise the process for an algebraic structure as discussed in [Reference Bergstra and Tucker12].Footnote 1 The basic algebra we need is to be found in the classic works of Birkhoff [Reference Birkhoff18] and, later, Mal’cev [Reference Mal’tsev26].
2.1 Algebras with absorption
Let A be an algebra with signature
$\Sigma $
, which may have partial operations. The definition of an absorptive element for a general algebraic structure is as follows.
Definition 2.1. A
$\Sigma $
-algebra A has an absorptive element
$a \in A$
if for each operation f of
$\Sigma $
, if one of its arguments equals a then so does its value.
The following partial result is relevant for our arithmetical data types as they are equipped with at least one binary operation ( [Reference Bergstra and Tucker12, Proposition 2.1]).
Lemma 2.1. If there is at least one function f in
$\Sigma $
with two or more arguments on a
$\Sigma $
-algebra A then an absorptive element in the algebra A is unique. Let
$\bot $
be a standard notation for an absorptive element.
Our use of
$\bot $
in an algebra will imply that it is absorptive with respect to all the operations of the algebra.
Definition 2.2. Let A be a
$\Sigma $
-algebra and assume
$\bot \not \in A$
. Then the
$\bot $
-enlargement of A is an algebra
$A_\bot $
with signature
$\Sigma _\bot = \Sigma \cup \{\bot \}$
and carrier set
$A_\bot = A \cup \{\bot \}$
, which is an enlargement of A in which
$\bot $
is absorptive.
Definition 2.3. As a notation we will use
$A_\bot $
for the construction of the
$\bot $
-extension of A. For any class
$\mathsf {K}$
of
$\Sigma $
-algebras, define
$$ \begin{align*}\mathsf{K}_\bot = \{ A_\bot \ | \ A \in \mathsf{K}\}.\end{align*} $$
Note we have only added
$\bot $
to an algebra; we have not yet employed it to make partial operations total.
2.2 Equations and absorption
First, we consider the definability of the classes. Let
$\Sigma $
be a signature and
$T(\Sigma , X)$
be the algebra of all terms over
$\Sigma $
containing variables from X. The value of a term
$t \in T(\Sigma , X)$
on elements a from a
$\Sigma $
algebra A is denoted 
or
$t(a)$
. If
$X = \emptyset $
we write
$T(\Sigma )$
for the algebra of all closed terms.
Let
$Eqn(\Sigma )$
and
$CEqn(\Sigma )$
be the set of all equations
$t = r$
and conditional equations
$t_1 = r_1 \wedge \ldots \wedge t_n = r_n \to t=r$
over
$\Sigma $
, respectively. Let
$\mathsf {Alg}(\Sigma , E)$
be the class of all
$\Sigma $
-algebras satisfying the axioms of
$E \subset Eqn(\Sigma )$
or of
$E \subset CEqn(\Sigma )$
. Common terms for these types of axiomatisable classes are variety and quasivariety, based on equivalent characterisations of these classes in terms of algebraic constructions [Reference Meinke, Tucker, Abramsky, Gabbay and Maibaum27].
The class
$\mathsf {Alg}(\Sigma , E)$
has an initial algebra
$I(\Sigma , E)$
that can be constructed as a quotient
$T(\Sigma )/\equiv $
by:
$$ \begin{align*}T(\Sigma)/\equiv \ \models t = t' \iff E \vdash t = t',\end{align*} $$
wherein
$\vdash $
is proof via equational logic or conditional equational logic. By equational logic we mean manipulating equations on the basis of reflexivity, symmetry, transitivity of equality, and the substitution of equal terms into equations. The less well known conditional equational logic is more involved requiring rules to access the conditions [Reference Meinke, Tucker, Abramsky, Gabbay and Maibaum27]. However, from Birkhoff and Mal’cev, we can also rely on first order derivations:
Lemma 2.2. Equations and conditional equations are provable from E by equational and conditional equational logic respectively if, and only if, they are provable from E in first order logic.
The following is [Reference Bergstra and Tucker12, Proposition 2.2]:
Theorem 2.1. Let
$\Sigma $
be a signature which contains at least one function symbol f with two or more arguments. For any nonempty class
$\mathsf {K}$
of
$\Sigma $
-algebras in which f is total, the class
$\mathsf {K}_\bot $
cannot be defined by conditional equations, i.e., is not a quasivariety.
If only unary functions are present in
$\Sigma $
then
$\mathsf {K}_\bot $
can be specified by the conditional equations
$f(x) = \bot \to x = \bot $
for each operation f.
It follows from Theorem 2.1 that in most cases there is no way to find a conditional equational specification for
$\mathsf {K}_\bot $
that is complete for first order formulae. In particular:
Corollary 2.2. Given a signature
$\Sigma $
which contains at least one function symbol f with two or more arguments, and any equationally defined class
$\mathsf {K} = \mathsf {Alg}(\Sigma , E)$
in which f is total, then the class
$\mathsf {K}_\bot $
is not definable by conditional equations, i.e., is not a quasivariety.
Rather than looking for equational axioms to capture the algebras of
$\mathsf {K}_\bot $
, what can be done instead, is to look for a finite axiomatisation of the full equational, or conditional equational, theory of
$\mathsf {K}_\bot $
. In general:
Definition 2.4. The equational theory of the class
$\mathsf {K}$
is the set
$$ \begin{align*}EqnThy(\mathsf{K}) = \{ e \in Eqn(\Sigma) \ | \ \forall A \in \mathsf{K}. A \models e \}\end{align*} $$
of all equations over
$\Sigma $
that are true in all the algebras in
$\mathsf {K}$
. The conditional equational theory of the class
$\mathsf {K}$
is the set
$$ \begin{align*}CEqnThy(\mathsf{\mathsf{K}}) = \{ c \in CEqn(\Sigma) \ | \ \forall A \in \mathsf{K}. A \models c \}\end{align*} $$
of all conditional equations over
$\Sigma $
that are true in all the algebras in
$\mathsf {K}$
.
Lemma 2.3. Let
$\mathsf {K}$
and L be classes of
$\Sigma $
algebras. If
$\mathsf {K} \subset L$
then
$EqnThy(\mathsf {L}) \subset EqnThy(\mathsf {K})$
and
$CondEqnThy(\mathsf {L}) \subset CondEqnThy(\mathsf {K})$
.
Definition 2.5. A set E of equations or conditional equations is complete or is a basis for the equational theory, or conditional theory, of the class
$\mathsf {K}$
if, respectively,
$$ \begin{align*}e \in EqnThy(\mathsf{K}) \iff E \vdash e \ \textrm{or} \ e \in CEqnThy(\mathsf{K}) \iff E \vdash e.\end{align*} $$
2.3
$\bot $
-enlargement for partial algebras
Notice that earlier A was total or partial and
$\mathsf {K}_\bot $
simply added
$\bot $
and ensured the operations respected it. The notion of a
$\bot $
-extension applied to total algebras does little useful work. However, it is useful to partial algebras: suppose the application of a function f on arguments is undefined in a partial
$\Sigma $
-algebra A then we can take
$\bot $
as the result of f on those arguments in
$A_\bot $
:
Definition 2.6. Let A be a partial algebra containing at least two elements. Then define the enlargement
$B=\mathsf {Enl}_\bot (A)$
to be a total algebra as follows:
$B = A \cup \{\bot \}$
where
$\bot $
is an absorptive element, and for
$b_1, ..., b_n \in A$
$$ \begin{align*}f(b_1,\dots,b_n) = \bot \text{ in } B \text{ if, and only if, } f(b_1,\dots,b_n) \text{ is undefined in } A. \end{align*} $$
Following Definition 2.6, in the case of A partial, the enlargement notation
$\mathsf {Enl}_\bot (A)$
implies that the partial operations of A have been made total using
$\bot $
. Of course,
$A_\bot $
is a partial algebra.
Definition 2.7. For any class
$\mathsf {K}$
of
$\Sigma $
-algebras, define
$$ \begin{align*}\mathsf{Enl}_\bot(\mathsf{K}) = \{ \mathsf{Enl}_\bot(A) \ | \ A \in \mathsf{K}\}.\end{align*} $$
Conversely, we can go the other way from a total algebra with absorptive element
$\bot $
to a partial algebraic data type.
Definition 2.8. Let A be an algebra with
$\bot $
as an absorptive element, and such that A has at least two elements. Then define the transformation
$B=\mathsf {Pdt}_\bot (A)$
to be a partial algebra as follows:
$B = A -\{\bot \}$
and for
$b_1, ..., b_n, b \in B$
,
$$ \begin{align*}f(b_1,\dots,b_n) = b \text{ in } B \text{ if, and only if, } f(b_1,\dots,b_n) = b \text{ in } A. \end{align*} $$
We recall two basic facts from [Reference Bergstra and Tucker12]. We always assume that the carrier set of an algebra is non-empty.
Proposition 2.1. Let A be a total algebra with
$\bot $
as an absorptive element, and such that A has at least two elements. Then
$$ \begin{align*}\mathsf{Enl}_\bot(\mathsf{Pdt}_\bot(A)) = A. \end{align*} $$
Proof. The carrier sets of both structures are the same as
$\bot $
is first taken out and then put back by the operators. Let
$\Sigma $
be a signature for A and let f be an n-ary operator of
$\Sigma $
. Suppose f has interpretation F in A, interpretation G in
$\mathsf {Pdt}_\bot (A)$
and interpretation H in
$\mathsf {Enl}_\bot (\mathsf {Pdt}_\bot (A))$
. Let
$a_1,\ldots ,a_n \in A^n$
. It must be shown that
$F(a_1,\ldots ,a_n) = H(a_1,\ldots ,a_n)$
.
If for some
$i \in [1,n]$
,
$a_i = \bot $
then
$F(a_1,\ldots ,a_n) = \bot $
because F is absorptive in A. Thus, with
$\bot $
removed,
$G(a_1,\ldots ,a_n) $
is undefined; and, with
$\bot $
restored,
$H(a_1,\ldots ,a_n) = \bot $
.
If all
$a_i$
are non-
$\bot $
then there are two cases:
$F(a_1,\ldots ,a_n) = \bot $
in which case again
$G(a_1,\ldots ,a_n) $
is undefined so that
$H(a_1,\ldots ,a_n) = \bot $
; and, secondly,
$F(a_1,\ldots ,a_n) \neq \bot $
so
$G(a_1,\ldots ,a_n) = F(a_1,\ldots ,a_n) $
and also
$H(a_1,\ldots ,a_n) = G(a_1,\ldots ,a_n)$
.
The following observation has a similar proof.
Proposition 2.2. Let A be an algebra without
$\bot $
. Then
$$ \begin{align*}\mathsf{Pdt}_\bot(\mathsf{Enl}_\bot(A)) = A. \end{align*} $$
3 On axiomatising division
3.1 Rings, fields, and meadows
A commutative ring with
$1$
is a field if every non-zero element is invertible. In particular, rings and fields have the same operations to which we will add division.
Lemma 3.1. Let R be a commutative ring with 1. If
$a \cdot b =1$
and
$a \cdot c = 1$
then
$b=c$
.
Proof. Assume
$a \cdot b =1$
and
$a \cdot c = 1$
. Then using the axioms for identity, associativity, and commutativity:
$$ \begin{align*}b = 1 \cdot b = (a \cdot c) \cdot b = a \cdot (c \cdot b) = a \cdot (b \cdot c) = (a \cdot b) \cdot c =1 \cdot c= c.\end{align*} $$
Given the uniqueness, we can define a partial inverse operator
$x^{-1}$
in any commutative ring with 1.
Definition 3.1. Let R be a commutative ring with 1. Then it has a unique partial division operator defined by inverses
(i)
$ a \div b =_{def} a \cdot (b^{-1})$
where
(ii) if
$ a\cdot c = 1$
then
$a^{-1}= c$
, and
(iii) if for no
$c \in R$
,
$ a \cdot c = 1$
then
$a^{-1}$
is undefined.
We will write
$\frac {x}{y}$
and
$x \div y$
alternatively as synonyms.
Example 3.1. In this form of division we can calculate
$a \div b$
whenever
$b^{-1}$
exists. In
$\mathbb {Z}$
this is a limited form of division: the equation
$b \cdot x = 1$
has solutions only when
$b = 1$
and
$b = -1$
.
In the finite ring
$\mathbb {Z}_{n}$
there are more divisions. In
$\mathbb {Z}_{10}$
, the equation
$b \cdot x = 1 \ mod \ 10$
has solutions
$b = 1, 3, 7$
.
Definition 3.2. Extending a ring R with this operator
$\div $
creates a ring with partial division denoted
$R_{\div }$
. Extending a field F with this operator
$\div $
creates a partial meadow denoted
$F_{\div }$
.
Let
$\Sigma _r$
be a signature of rings and fields, and let
$\Sigma _{r,\div }$
be a signature of rings and fields with division. Thus,
$\Sigma _{r,\div }$
is the signature of a meadow.
3.2 Totalising division in a ring
To move from division as a partial operation to division as a total operation in a ring, we define common division.
Definition 3.3. Let
$R_{\div }$
be a commutative ring with partial division. Then, on adding the absorptive element
$\bot $
to the domain of the ring and re-defining its division operation by
(i) if
$ a\cdot c = 1$
then
$a^{-1}= c$
, and
(ii) if for no
$c \in R$
,
$ a \cdot c = 1$
then
$a^{-1}= \bot $
,
we have a total division operator; we call this total operation common division.
Recalling the general method of extending an algebra with
$\bot $
, and specifically Definition 2.6, we will use the following notations.
Definition 3.4. A commutative ring with inverse based common division is a total algebra of the form
$\mathsf {Enl}_\bot (R_{\div })$
. Let
$\mathsf {CR}_{\div , \bot }$
be the class of all such algebras. A common meadow is an algebra of the form
$\mathsf {Enl}_\bot (F_{\div })$
wherein F is field. Let
$\mathsf {CM}$
be the class of all common meadows.
An important algebra is the common meadow of rational numbers
$\mathbb {Q}_{\bot } = \mathsf {Enl}_\bot (\mathbb {Q}_{\div })$
.
Let
$\Sigma _{r,\div , \bot }$
be a signature of rings and fields with common division wherein
$\bot $
is a constant.
Lemma 3.2. Each common meadow is also a commutative ring with common division, but not every commutative ring with common division is a common meadow. In symbols,
$\mathsf {CM} \subsetneqq \mathsf {CR}_{\div , \bot }$
.
Here is a counter-example for the second clause of the lemma.
Example 3.2. An example of a commutative ring with common division that is not a common meadow is
$M =\mathsf {Enl}_\bot ((\mathbb {Z}_n)_{\div })$
with
$n = 10$
. Notice that in M,
$2 \cdot 3 = 6$
. There is no c such that
$2 \cdot c = 1\ \mod 10$
and so the inverse
$\frac {1}{2} = \bot $
. It follows that there is a non-zero element without proper inverse. We further notice that,
$$ \begin{align*}\frac{6}{2} = 6 \cdot \frac{1}{2} = 6 \cdot \bot = \bot \neq 3.\end{align*} $$
On the other hand, as
$3 \cdot 7 = 21\ \mod 10 = 1\ \mod 10$
, we have
$$ \begin{align*}\frac{6}{3} = 6 \cdot \frac{1}{3} = 6 \cdot 7\quad \mod 10 = 42\quad \mod 10 = 2.\end{align*} $$
On forgetting division, a commutative ring with partial division remains a ring and, similarly, a meadow whose division is partial remains a field. However, as noted earlier, the addition of the absorptive
$\bot $
breaks the axioms and laws of rings. Thus, of immediate technical interest is the impact of
$\bot $
on the familiar and fundamental properties of rings and fields. Indeed, what may be left after weakening the properties of commutative rings by adding
$\bot $
?
3.3 Equational axioms
Now, we present the axiom system
$E_{\mathsf {ftc-cm}}$
that is at the centre of our programme on common meadows and a focus of this paper. The equations for
$E_{\mathsf {ftc-cm}}$
split into two parts:
(i) a set
$E_{\mathsf {wcr},\bot }$
of equations for commutative rings now weakened by
$\bot $
, in Table 1; and
(ii) equations for division
$\div $
, in Table 2.
Notably, for (i), for some x,
$0 \cdot x \neq 0$
.
Definition 3.5. A model of
$E_{\mathsf {ftc-cm}}$
we will call a generalised common meadow. We denote the class of such algebras
$\mathsf {GCM} =\mathsf {Alg}(\Sigma _{r,\div , \bot }, E_{\mathsf {ftc-cm}})$
.
Because the generalised common meadows constitute a variety, the conditional equational theory—and indeed the first order theory – —of the class of generalised common meadows is finitely axiomatised by
$E_{\mathsf {ftc-cm}}$
.
3.3.1 Fracterms and flattening
An important feature of division is the introduction of fractional expressions. Now, in abstract data type theory, fractions can be given a clear formalisation as a syntactic object—as a term over a signature containing division with a certain form. Rather than fraction we will speak of a fracterm, following the terminology of [Reference Bergstra5] (item 25 of 4.2).
Definition 3.6. A fracterm is a term over
$\Sigma _{r,\div }$
whose leading function symbol is division
$\div $
. A flat fracterm is a fracterm with only one division operator.
For reasons of convention and clarity, we will change notation from
$\div $
to the familiar fraction notations when appropriate and so fracterms can have these forms
$p \div q, \ \frac {p}{q}, \ p/q$
and flat fracterms have these forms in which p and q do not involve any occurrence of division. Here is an appropriate context for changing from
$\div $
to the familiar fraction notation: the following simplification process is a fundamental property of working with fracterms.
Theorem 3.1 (Fracterm flattening [Reference Bergstra, Ponse, de Nicola and Hennicker8]).
For each term t over
$\Sigma _{r, \div , \bot }$
there exist p and q terms over
$\Sigma _{r}$
, i.e., both not involving
$\bot $
or division, such that
$$ \begin{align*}\displaystyle E_{\mathsf{ftc-cm}} \vdash t = \frac{p}{q},\end{align*} $$
i.e., t is provably equal to a flat fracterm. Furthermore, the transformation is computable.
Proof. Immediate by structural induction on the structure of t, noting that any occurrence of
$\bot $
can be replaced by
$1/0$
.
Thus, fracterms can be transformed uniformly into equivalent flat fracterms for use in any model of
$E_{\mathsf {ftc-cm}}$
, i.e., in any generalised meadow. One of several key properties is that the axioms of
$E_{\mathsf {ftc-cm}}$
guarantee flattening (Theorem 3.1).
3.3.2 A remark on (changing) terminology.
What we now call a generalised common meadow was originally called a common meadow in [Reference Bergstra, Ponse, de Nicola and Hennicker8]. However, as applications in computing mainly deal with enlargements of fields with division we have chosen to use common meadow for a smaller class of structures where the non-
$\bot $
elements constitute a field rather than for any model of the equations in Tables 1 and 2. For an arbitrary model of
$E_{\mathsf {ftc-cm}}$
we prefer to use generalised common meadow, or GCM, in an attempt to be concise and avoid overly logical jargon. We mention that in [Reference Dias and Dinis21] and [Reference Dias and Dinis22] the original terminology of [Reference Bergstra, Ponse, de Nicola and Hennicker8] is used.
4 Commutative rings with
$\bot $
We have developed these axioms
$E_{\mathsf {ftc-cm}}$
to make a theory of common meadows. How much lifts from fields to commutative rings with common division? The following observation is due to Dias and Dinis in [Reference Dias and Dinis21].
Proposition 4.1. Each commutative ring with inverse based common division satisfies all the equational axioms in
$E_{\mathsf {ftc-cm}}$
for common meadows.
Proof. This is a matter of straightforward inspection of all equations of
$E_{\mathsf {ftc-cm}}$
.
Example 4.1. There are models of
$E_{\mathsf {ftc-cm}}$
that are commutative rings and are not common meadows: starting with a ring that is not a field, e.g.,
$\mathbb {Z}$
, we take the
$\bot $
-enlargement of it and then expand the resulting structure with inverse based common division to obtain a generalised common meadow that is not a common meadow.
There are models of
$E_{\mathsf {ftc-cm}}$
that are not commutative rings: add a new constant c to the signature to make
$\Sigma _{r,\div , \bot ,c}$
and do not add any equations mentioning c to
$E_{\mathsf {ftc-cm}}$
. Consider the class
$\mathsf {Alg}(\Sigma _{r,\div , \bot ,c}, E_{\mathsf {ftc-cm}})$
. It is easy to see that an initial algebra A of this equational class is a generalised common meadow, as it satisfies
$E_{\mathsf {ftc-cm}}$
; but A is not a ring as neither
$c \cdot 0 = 0$
nor
$c = \bot $
can be shown from
$E_{\mathsf {ftc-cm}}$
, so that neither identity is true in A.
Consider the conditional formula – which is not a conditional equation—taken from [Reference Bergstra, Ponse, de Nicola and Hennicker8].
Definition 4.1. The following formulae is termed the Normal Value Law
$$ \begin{align*}\mathsf{NVL}: \ \ x \neq \bot \to 0 \cdot x = 0\end{align*} $$
or, equivalently,
$$ \begin{align*}\mathsf{NVL}: \ \ 0 \cdot x \neq 0 \to x = \bot.\end{align*} $$
Also, consider the conditional equation—taken from [Reference Bergstra, Ponse, de Nicola and Hennicker8].
Definition 4.2. The following conditional equation is termed the Additional Value Law
$$ \begin{align*}\mathsf{AVL}: \ \ \frac{1}{x} = \bot \to 0 \cdot x = x.\end{align*} $$
The following Propositions 4.2 and 4.3 are essentially contained in [Reference Dias and Dinis21, Proposition 5.4]. We add our proofs of these facts for completeness.
Proposition 4.2. The class
$\mathsf {CR}_{\div , \bot }$
of commutative rings with inverse based common division are precisely the models of
$E_{\mathsf {ftc-cm}}$
that satisfy
$\mathsf {NVL}$
.
Proof. That a commutative ring with inverse based common division satisfies
$\mathsf {NVL}$
is immediate because in a ring all elements x satisfy
$0 \cdot x = 0$
. For the other direction, suppose
$M \models E_{\mathsf {ftc-cm}} + \mathsf {NVL}$
. The non-
$\bot $
elements of M satisfy
$0\cdot x = 0$
so that M is an expansion of
$\mathsf {Enl}_\bot (R)$
for a ring R. Now if
$\frac {1}{p}$
is non-
$\bot $
for
$p \in M$
then
$0 \cdot \frac {1}{p} = 0$
and we find that
$$ \begin{align*}\frac{p}{p} = 1 + \frac{0}{p}= 1 + 0 \cdot \frac{1}{p}= 1 + 0 = 1\end{align*} $$
so that
$\frac {1}{p}$
is defined with the same value in the enlargement of R to a ring with inverse based common inverse.
Proposition 4.3. Within the class
$\mathsf {CR}_{\div , \bot }$
of commutative rings with inverse based common division, the common meadows are precisely those which satisfy the conditional equation
$\mathsf {AVL}$
.
Proof.
$\mathsf {AVL}$
is satisfied in any common meadow because
$ \frac {1}{x} = \bot $
is satisfied only by
$x=0$
and
$x=\bot $
, and in both cases
$0\cdot x = x$
. On the other hand, contrapositively, let R be a ring which is not a field, then for some non-zero
$a \in R$
it must be that there is no proper inverse for it, i.e., there is no
$c \in R$
with
$a \cdot c = 1$
. Thus, in
$\mathsf {Enl}_\bot (R_{\div })$
it is the case that
$\frac {1}{a} = \bot $
. However, as
$a \in R$
,
$0 \cdot a = 0$
, and
$0 \cdot a \neq a$
as
$a \neq 0$
so
$\mathsf {AVL}$
is not satisfied.
As an immediate consequence we find:
Proposition 4.4. The axiom system
$E_{\mathsf {ftc-cm}}$
for common meadows is not complete for the conditional equational theory of common meadows.
Proof.
$\mathsf {AVL}$
is true in all common meadows but it is invalid in any generalised common meadow M obtained by enlarging a ring that is not a field with
$\bot $
and inverse based common division. As
$M \models E_{\mathsf {ftc-cm}}$
(by Proposition 4.1) and
$M \not \models \mathsf {AVL}$
, by soundness, we find that
$E_{\mathsf {ftc-cm}} \not \vdash \mathsf {AVL}$
.
The result of Proposition 4.4 was obtained in [Reference Bergstra and Tucker13] with a different proof. Note, too, that the conditional equation
$$ \begin{align*}x \cdot x = 0 \to x = 0\end{align*} $$
is valid in all fields and in all common meadows. But it is not valid in all rings and for that reason also not valid in all rings enlarged with inverse based common division.
Given the significance of
$\mathsf {AVL}$
(Proposition 4.3), and its independence (Proposition 4.4), we examine
$E_{\mathsf {ftc-cm}} + \mathsf {AVL}$
:
Proposition 4.5.
$E_{\mathsf {ftc-cm}} + \mathsf {AVL} \vdash x \cdot x = 0 \to x = 0$
.
Proof. From [Reference Bergstra, Ponse, de Nicola and Hennicker8], we have
$E_{\mathsf {ftc-cm}} \vdash 0 \cdot x \cdot x = 0 \to 0 \cdot x = 0$
. Moreover,
$E_{\mathsf {ftc-cm}} \vdash \frac {1}{x} = \frac {x}{x \cdot x}$
. Thus from
$x \cdot x = 0$
we find
$\frac {1} {x} = \frac {x}{x \cdot x} = \frac {x}{0} = x \cdot \bot = \bot $
so that with
$\mathsf {AVL}$
we have
$0 \cdot x = x$
. Taking both facts together we find
$x = 0 \cdot x = 0$
.
We will return to these issues later. In contrast to Proposition 4.4, we have shown previously [Reference Bergstra and Tucker16] these facts.
Theorem 4.1. The equational axiom system
$E_{\mathsf {ftc-cm}}$
is complete for the equational theory of common meadows. For every equation e,
$$ \begin{align*}\displaystyle E_{\mathsf{ftc-cm}} \vdash e \ \textrm{if, and only if,} \ \mathsf{CM} \models e.\end{align*} $$
Theorem 4.2. The equational axiom system
$E_{\mathsf {ftc-cm}}$
for common meadows is complete for the equational theory of commutative rings with inverse based common division. For every equation e,
$$ \begin{align*}\displaystyle E_{\mathsf{ftc-cm}} \vdash e \ \textrm{if, and only if,} \ \mathsf{CR}_{\div, \bot} \models e.\end{align*} $$
Proof. From left to right is Proposition 4.1. For the other direction first notice that all common meadows are commutative rings with inverse based common division, so that the equational theory of commutative rings with inverse based common division is contained in the equational theory of common meadows—recall Lemma 2.3.
Therefore, completeness of
$E_{\mathsf {ftc-cm}}$
for the equational theory of commutative rings with inverse based common division follows immediately from the completeness of
$E_{\mathsf {ftc-cm}}$
for the equational theory of common meadows, i.e., Theorem 4.1.
In addition, Proposition 4.4 draws attention to the open Problem 1.1 of the Introduction.
4.1 Axiomatising the class of common meadows
The following facts are related to general results in [Reference Bergstra and Tucker12], recalled here as Theorem 2.1. More specifically, the following fact follows from Theorem 2.1 about
$\bot $
-enlargements.
Proposition 4.6. The class
$\mathsf {CM}$
of common meadows is not a quasivariety. The class
$\mathsf {CR}_{\div , \bot }$
of commutative rings with inverse based common division is not a quasivariety.
Here is a direct proof using a technique with initial algebras.
Proof. Consider the second statement. Suppose that conditional equational theory
$E_{ce}$
has precisely the commutative rings with inverse based common division as its models, i.e.,
$\mathsf {CR}_{\div , \bot } = \mathsf {Alg}(\Sigma , E_{ce})$
.
We introduce fresh constants c and d. We consider an initial algebra of
$E' = E \cup \{ c+ d = \bot \}$
. Now there is a commutative ring with inverse based common division
$M_1$
that satisfies
$E'$
by taking
$c= 0$
and
$d = \bot $
from which it follows that
$E' \not \vdash c = \bot $
. Similarly, there is a model
$M_2$
of
$E'$
in which
$d=0$
and
$c = \bot $
so that
$E' \not \vdash d= \bot $
. It follows that, in an initial algebra of
$E'$
,
$c+d = \bot $
while
$c \neq \bot $
and
$d\neq \bot $
. However, this latter situation cannot occur in any structure of the form
$\mathsf {Enl}_\bot (R_{\div })$
because
$c \in R$
and
$d \in R$
, whence
$c+d \in R$
, thereby contradicting
$c+ d = \bot $
.
This basic fact may be contrasted with Theorem 4.2 above. Indeed, while
$E_{\mathsf {ftc-cm}}$
completely axiomatises all equations true in all common meadows it fails, i.e., it is too weak, to define the class of common meadows. Common meadows can be defined with a first order theory but not with equations, or with conditional equations alone.
Proposition 4.7. There is a consistent conditional equational extension T of
$E_{\mathsf {ftc-cm}}$
which has no commutative ring with inverse based common division as a model.
Proof. We set
$$ \begin{align*}T = E_{\mathsf{ftc-cm}}~\cup \{0 \cdot \frac{1}{1+1} = 0 \to 0=1, \frac{1}{1+1} = \bot \to 0=1\}.\end{align*} $$
Let M be an initial algebra of
$E_{\mathsf {ftc-cm}}$
. Then
$0 \cdot \frac {1}{1+1} = 0$
is not valid in M because
$E_{\mathsf {ftc-cm}}$
allows a model (based on the prime field
$\mathbb {Z}_{2}$
of characteristic
$2$
) in which
$$ \begin{align*}0 \cdot \frac{1}{1+1} = 0 \cdot \bot = \bot \neq 0\end{align*} $$
and
$\frac {1}{1+1} = \bot $
is not valid because that equation fails in a common meadow of rational numbers. It follows that M satisfies T.
Now consider any commutative ring with inverse based common division, say
$M'= \mathsf {Enl}_\bot (R_\div )$
which is a model of T. In
$M'$
,
$0 \cdot \frac {1}{1+1} \neq 0$
so that
$ \frac {1}{1+1} \notin R$
and by definition of
$\mathsf {Enl}_\bot (R_\div )$
it must be the case that
$\frac {1}{1+1} = \bot $
in
$M'$
which contradicts
$M' \models T$
.
5 GCM homomorphisms
GCMs allow a rich world of homomophisms which has first been explored in general by Dias and Dinis in [Reference Dias and Dinis21], and in the context of finite GCMs in [Reference Dias and Dinis22], where however, homomorphisms are not required to respect division. Below we will insist that a GCM-homomorphism respects division as well. We start our discussion of GCM homomorphisms with two examples.
Example 5.1. The ring homomorphism
$\phi : \mathbb {Z}_4 \to \mathbb {Z}_2$
extends to a homomorphism from
$\bar {\phi }: \mathsf {Enl}_\bot ((\mathbb {Z}_4)_\div ) \to \mathsf {Enl}_\bot ((\mathbb {Z}_2)_\div )$
.
However, the ring homomorphism
$\phi : \mathbb {Z}_6 \to \mathbb {Z}_3$
does not extend to a homomorphism from
$\mathsf {Enl}_\bot ((\mathbb {Z}_6)_\div )$
to
$\mathsf {Enl}_\bot ((\mathbb {Z}_3)_\div )$
. To see this notice that in
$\mathsf {Enl}_\bot ((\mathbb {Z}_6)_\div )$
the inverse of
$2$
is
$\bot $
while in
$\mathsf {Enl}_\bot ((\mathbb {Z}_3)_\div )$
the inverse of
$2$
is
$2$
.
Proposition 5.1. Every generalised common meadow (GCM) allows a homomorphism
$\rho $
to a commutative ring with inverse common division.
Proof. Let M be a GCM, and using the notation of [Reference Dias and Dinis21] we write
$M_0 = \{a \in M \mid 0 \cdot a = 0\}$
.
$M_0$
is a commutative ring to which we add inverse common division,
$\mathsf {Enl}_{\bot }(M_0)$
.
We define
$\rho $
as follows:
$$ \begin{align*}\rho(a) = a \ \textrm{for} \ a \in M_0 \ \textrm{and} \ \rho(a) = \bot \ \textrm{for} \ a \not\in M_0.\end{align*} $$
To see that
$\rho $
is a homomorphism:
(i) Constants. As
$0,1 \in M_0$
and
$\bot \notin M_0$
,
$\rho $
preserves the constants.
(ii) Addition. To check
$\rho (a) + \rho (b) = \rho (a+ b)$
we have four cases:
(ii1) if
$a \in M_0$
and
$b \in M_0$
then
$0 \cdot (a+b) = 0 \cdot a + 0 \cdot b = 0 + 0 = 0$
so that
$\rho (a) + \rho (b) = a + b = \rho (a+ b)$
;
(ii2)
$a \in M_0$
and
$b \notin M_0$
then
$\rho (a) + \rho (b) = a + \bot = \bot = \rho (a+ b)$
, while assuming that
$a + b \in M_0$
and if
$a + b \in M_0$
we find a contradiction as follows
$0 \cdot b = 0 \cdot 0 + b = 0 \cdot a + 0 \cdot b = 0 \cdot (a + b) = 0$
, i.e.
$b \in M_0$
;
(ii3)
$a \notin M_0$
and
$b \in M_0$
, is dealt with as case (ii2); and finally
(ii4)
$a \notin M_0$
and
$b \notin M_0$
, from in [Reference Bergstra, Ponse, de Nicola and Hennicker8, Proposition 2.3.1(ce5)] we find that
$a+b \in M_0$
implies
$a \in M_0$
so that we know that
$a+b \notin M_0$
whence
$\rho (a) + \rho (b) = \bot + \bot = \bot = \rho (a+ b)$
.
(iii) Multiplication. This case works the same as addition.
(iv) Additive inverse. This is immediate.
(v) Multiplicative inverse. This has two subcases: (v1)
$a \in M_0$
and (v2)
$a \notin M_0$
.
For (v1), if
$a \in M_0$
there are two subcases: (v1i)
$ a^{-1} \in M_0$
, which is immediate and (v1ii)
$ a^{-1} \notin M_0$
. In case (v1ii) it cannot be the case that
$ a \cdot a^{-1} = 1$
as otherwise
$ 0 \cdot a^-1= (0 \cdot a) \cdot a^{-1} = 0 \cdot (a \cdot a^{-1}) = 0 \cdot 1 = 0$
thereby contradicting
$ a^{-1} \notin M_0$
so we find that
$\rho (a^{-1}) = \bot $
by definition of
$\rho $
in a common meadow and
$\rho (a)^{-1} = \bot $
by definition of a common meadow. In case
For (v2), i.e.,
$a \notin M_0$
we find that
$a^{-1} \notin M_0$
because otherwise
$ 0 \cdot a= (0 \cdot a^{-1}) \cdot a = 0 \cdot (a^{-1} \cdot a) = 0 \cdot 1 = 0$
.
5.1 GCM homomorphisms and
$\mathsf {AVL}$
We first notice that
$\mathsf {AVL}$
is a natural property for GCM’s.
Proposition 5.2. Let
$I(\Sigma _{\mathsf {cm}},E_{\mathsf {ftc-cm}})$
be an initial algebra for the equations
$E_{\mathsf {ftc-cm}}$
. Then
$I(\Sigma _{\mathsf {cm}},E_{\mathsf {ftc-cm}})$
satisfies
$\mathsf {AVL} $
.
Proof. To see this, we consider a closed term t such that
$\frac {1}{t} = \bot $
is provable from
$E_{\mathsf {ftc-cm}}$
. Using fracterm flattening (Theorem 3.1) we find that
$t = \frac {n}{m}$
for appropriate numerals n and m. Then
$\frac {1}{t} = \frac {m \cdot m}{n \cdot m}$
. Now
$\frac {m \cdot m}{n \cdot m}= \bot $
implies
$n \cdot m = 0$
. Now we use the fact that
$\mathbb {Q}_\bot $
is a model of
$E_{\mathsf {ftc-cm}}$
and for that reason a homomorphic image of the initial algebra so that in
$\mathbb {Q}_\bot $
it is the case that
$n \cdot m = 0$
from which it follows that either
$n= 0$
or
$m=0$
and in both cases
$0 \cdot t = t$
.
Now,
$\rho (M) \cong \mathsf {Enl}_\bot (\mathbb {Z}_\div )$
and so fails
$\mathsf {AVL} $
, so that
$\mathsf {AVL}$
is not preserved under homomorphisms of the form
$\rho $
.
We will now consider a different kind of homomorphism on GCM’s. Part (i) of the following observation is made in [Reference Dias and Dinis21].
Lemma 5.1. Let M be a GCM and let
$a \in M$
be such that
$a \neq \bot $
,
$a \neq 0$
and
$0 \cdot a = a$
. Let the function
$\phi _a \colon M \to M$
be defined by
$$ \begin{align*}\phi_a(b)= b + a,\end{align*} $$
and write
$x =_a y$
for
$\phi _a(x) = \phi _a(y)$
:
(i)
$\phi _a$
is a homomorphism, the image
$\phi _{a}(M)$
of which is again a non-trivial GCM (i.e.,
$\phi _a(0) \neq \phi _a(1)$
);
(ii) if M satisfies
$\mathsf {AVL}$
then the homomorphic image
$\phi _{a}(M)$
satisfies
$\mathsf {AVL}$
;
(iii) if
$a = \frac {1}{b}$
then
$a \cdot b =_a 1$
.
Proof. For (i), we refer to [Reference Dias and Dinis21], though the check that
$p =_a q \iff p + 0 \cdot a = q + 0 \cdot a$
is a congruence is immediate for all cases.
For (ii), consider
$c \in M$
such that
$\phi _a(\frac {1}{c}) = \bot $
, it must be verified that
$0 \cdot \phi _a(c) = \phi _a(c)$
. Now,
$\phi _a(\frac {1}{c}) = \bot $
implies that (working in M, and doing some of the work of the proof of (i))
$$ \begin{align*}\frac{1}{c} + 0 \cdot a = \frac{1}{c} + a = \bot + a = \bot\end{align*} $$
and
$$ \begin{align*}\frac{1}{c} + 0 \cdot a = \frac{1 + 0 \cdot a}{c} = \frac{1}{c + 0 \cdot a} = \frac{1}{\phi_a(c)}\end{align*} $$
so that
$\frac {1}{\phi _a(c)} = \bot $
and with
$\mathsf {AVL}$
in M one finds
$0 \cdot \phi _a(c) = \phi _a(c) $
as required.
For (iii):
$a \cdot b = b \cdot \frac {1}{b} = 1 + \frac {0}{b} = 1 + 0 \cdot a =_a 1$
.
Given a GCM M with non-
$\bot $
$a \in M$
such that
$0 \neq 0 \cdot a$
one may define a congruence
$=^{\prime }_a$
as follows:
(i)
$b =^{\prime }_a \bot \iff b + 0 \cdot a = b$
, and
(ii)
$b =^{\prime }_a c \iff (b = c\, \vee \, (b=^{\prime }_a \bot \wedge c =^{\prime }_a \bot ))$
.
It is a straightforward verification that
$=^{\prime }_a$
is a congruence relation with
$1 \not =^{\prime }_a \bot $
and consequently
$1 \not =^{\prime }_a 0$
.
$M/\! =^{\prime }_a $
is a non-trivial GCM. Note the natural homomorphism:
Proposition 5.3. The natural homomorphism
$\pi ^\bot _{a}: M \to M/\! =^{\prime }_a$
need not preserve the validity of
$\mathsf {AVL}$
.
Proof. Let a and b be fresh constants and let
$I_S$
be an initial algebra of the algebraic specification
$$ \begin{align*}S=(\Sigma_{\mathsf{cm}}\cup\{a,b\},E_{\mathsf{ftc-cm}} \cup \{\mathsf{AVL},\frac{1}{b} + 0 \cdot a = \frac{1}{b}\}).\end{align*} $$
Now,
$I_S$
satisfies
$\mathsf {AVL}$
while
$I_S/\!=^{\prime }_a $
does not.
To see the this, we notice that in
$I_S/\!=^{\prime }_a $
,
$\frac {1}{b} = \bot $
, i.e.,
$\frac {1}{b} =^{\prime }_a \bot $
while
$0 \cdot b \not =^{\prime }_a b$
. To see that
$0 \cdot b \not =^{\prime }_a b$
fails in
$I_S/\!=^{\prime }_a $
first notice that upon choosing
$\frac {1}{2}$
for a and
$\bot $
for b,
$I_S$
is mapped to an initial algebra
$M'$
of the specification
$S' =(\Sigma _{\mathsf {cm}}\cup \{a,b\},E_{\mathsf {ftc-cm}}\cup \{\mathsf {AVL},b = \frac {1}{2}, a = \bot \})$
which is also an initial algebra of
$S' =(\Sigma _{\mathsf {cm}}\cup \{a,b\},E_{\mathsf {ftc-cm}}\cup \{b = \frac {1}{2}, a = \bot \})$
in view of Proposition 5.2. Now
$M'$
satisfies
$ 0 \cdot b \neq 0$
(i.e.,
$0 \cdot \frac {1}{2} \neq 0 \cdot \frac {1}{2}$
) and (with
$b = \frac {1}{2}$
,
$a = \bot $
)
$b+ 0 \cdot a \neq b$
, and
$0 \cdot b + 0 \cdot a \neq 0 \cdot b$
. It follows that none of
$ 0 \cdot b = 0$
,
$ b + 0 \cdot a = b$
and
$0 \cdot b + 0 \cdot a = 0 \cdot b$
are provable from S so that neither of these equations is true in M, with as a consequence that in M
$0 \cdot b \neq b$
, thereby refuting the validity of
$0 \cdot b = b$
in
$I_S/\!=^{\prime }_a $
and for that reason refuting
$\mathsf {AVL}$
as well.
The example of Proposition 5.3 indicates that chains of homomorphisms applied to a GCM in order to get closer to a common meadow are best made up from homomorphisms of the type
$\phi _{0 \cdot a}(b) = b + 0 \cdot a$
, rather than
$\rho $
or
$\pi ^{\bot }_{a}$
.
Recall completeness for conditional equations (Definition 2.5), and that
$E_{\mathsf {ftc-cm}}$
does not axiomatise the conditional theory of common meadows—Proposition 4.4. However, it does more than axiomatise the equational theory of commutative rings—Proposition 4.2.
Theorem 5.1.
$E_{\mathsf {ftc-cm}}$
provides a complete equational axiomatisation of the conditional equational theory of the class of commutative rings with inverse based common division.
Proof. We need to show that whenever a conditional equation
$\psi $
is true in all commutative rings with inverse common division it is derivable from
$E_{\mathsf {ftc-cm}}$
, i.e.,
$\psi $
is true in all GCMs. So suppose that
$\psi $
is refuted in a GCM, say M. We will transform M into a commutative ring with common division
$M'$
which refutes
$\psi $
as well.
We write
$\psi \equiv t_1 = r_1 \wedge \ldots \wedge t_n = r_n \to t=r$
, and we assume that variables
$x_1,\ldots ,x_k$
occur in
$\psi $
and that substituting
$a_1, \ldots ,a_k$
for these variables provides an instance in M refuting
$\psi $
. Let
$b = t(a_1,\ldots ,a_k)$
and
$c = r(a_1,\ldots ,a_k)$
. Because
$b\neq c$
at least one of both, say b, differs from
$\bot $
.
We will consider three cases:
(i)
$c = \bot $
and
$b \neq \bot $
,
(ii)
$c \neq \bot $
and
$b \neq \bot $
and
$0 \cdot b = 0 \cdot c$
, and
(iii)
$c \neq \bot $
and
$b \neq \bot $
and
$0 \cdot b \neq 0 \cdot c$
.
(i) We assume first that
$c = \bot $
and
$b \neq \bot $
. We know that
$0 \cdot b \neq \bot $
and we consider the mapping
$\rho \circ \phi _{0 \cdot b}$
with
$\rho $
as used in the proof of Proposition 5.1 and
$\phi _{0 \cdot b}$
as used in the proof of Lemma 5.1. As
$\rho \circ \phi _{0 \cdot b}$
is a homomorphism it preserves all conditions of the conditional equation
$\phi $
.
Concerning the conclusion of
$\psi $
we notice that
$$ \begin{align*}\phi_{0 \cdot b}(b) = b+ 0 \cdot b = (1 + 0 )\cdot b = 1 \cdot b = b,\end{align*} $$
and in the image
$\phi _{0 \cdot b}(M)$
,
$\phi _{0 \cdot b}(b) \neq \bot $
because if
$ b =_{0 \cdot b} \bot $
then
$b + 0\cdot b = b = \bot $
contradicting the assumption on b and c. Clearly,
$\phi _{0 \cdot b}(c) = \phi _{0 \cdot b}(\bot )= \bot $
so that the conclusion of
$\psi $
remains false in the image of
$\phi _{0 \cdot b}$
on the substitution
$\phi _{0 \cdot b}(a_1),\ldots , \phi _{0 \cdot b}(a_k)$
. In
$\phi _{0 \cdot b}(M)$
then,
$0 = 0 \cdot b$
so that
$\rho $
acts as identity on
$\phi _{0 \cdot b}(b)$
, with the effect that
$\psi $
fails in
$\rho (\phi _{0 \cdot b}(M))$
, which is a commutative ring with inverse based common division.
(ii) Next, we consider the case that b and c are both non-
$\bot $
and that
$0 \cdot b = 0 \cdot c$
. Again, we may consider the homomorphism
$\rho \circ \phi _{0 \cdot b}$
and we find
$\rho (\phi _{0 \cdot b}(b)) = b$
as above and
$\rho (\phi _{0 \cdot b}(c) )= c$
so that again in
$\rho \circ \phi _{0 \cdot b}(M)$
the conditional equation
$\psi $
is invalid on the substitution
$\phi _{0 \cdot b}(a_1),\ldots , \phi _{0 \cdot b}(a_k)$
.
(iii) Finally, without loss of generality, we assume that
$0 \cdot b \neq 0 \cdot c$
. Suppose that both
$(0 \cdot b) \cdot (0 \cdot c) = 0 \cdot b$
and
$(0 \cdot c) \cdot (0 \cdot c) = 0 \cdot c$
then
$0 \cdot b = 0 \cdot c$
which contradicts the assumptions on b and c. We assume w.o.l.g. that
$(0 \cdot b) \cdot (0 \cdot c) \neq 0 \cdot b$
. Again we will use the homomorphism
$\rho \circ \phi _{0 \cdot b}$
. Now we find that
$0 \cdot \psi _{0 \cdot b}(b) = \phi _{0 \cdot b}(0)$
while
$0 \cdot \phi _{0 \cdot b}(c) \neq \phi _{0 \cdot b}(0)$
, as otherwise
$ 0 \cdot (0 \cdot c) =_{0 \cdot b} 0$
which would imply that
$(0 \cdot b) \cdot (0 \cdot c) \neq 0 \cdot b$
. It follows that
$\rho $
will leave
$\phi _{0 \cdot b}(b)$
unchanged while
$\rho (\phi _{0 \cdot b}(c)) = \bot $
with the effect that
$\phi $
fails in
$\rho (\phi _{0 \cdot b}(M))$
.
5.2
$\bot $
-splitting in GCMs
Definition 5.1. A GCM M features (non-trivial)
$\bot $
-splitting if
$\bot $
is the sum of two non-
$\bot $
elements in M.
Clearly, a common meadow will not feature non-trivial
$\bot $
-splitting and, more generally, nor will a commutative ring with inverse based common division.
Moreover, if in a GCM M,
$a, b \in M$
feature non-trivial
$\bot $
-splitting then
$0 \cdot a \neq 0$
as otherwise
$0 \cdot (a+ b) = 0 \cdot \bot $
so that
$0 \cdot b = \bot $
and then
$b = \bot $
; similarly, it follows that
$0 \cdot b \neq 0$
.
Example 5.2. Let a and b be two constants with associated axiom
$a + b= \bot $
. In the initial algebra I of
$E_{\mathsf {ftc-cm}} + \{ a + b= \bot \} $
we find
$0 \neq a \neq \bot $
,
$0 \neq b \neq \bot $
and
$ a\neq b$
. Thus, I allows non-trivial
$\bot $
-splitting.
Proposition 5.4. Let M be a GCM which satisfies
$\mathsf {AVL}$
. If M possesses non-trivial zero divisors then M features non-trivial
$\bot $
-splitting.
Proof. Suppose M allows non-trivial zero divisors, then for some
$a,b \in M$
,
$ a \cdot b = 0$
while
$a \neq 0 \neq b$
. Now, consider the sumterm
$t = \frac {1}{a} + \frac {1}{b}$
. We will find that t features non-trivial
$\bot $
-splitting. We have
$t = \frac {a + b}{a \cdot b} = \frac {a + b}{0}= \bot $
. Moreover, if
$\frac {1}{a} = \bot $
then with
$\mathsf {AVL}$
,
$0 \cdot a = a$
and from
$ a \cdot b = 0$
follows
$ 0 \cdot a \cdot b = 0$
, which implies
$0 \cdot a = 0$
. Both facts together yield
$a = 0$
, which contradicts the assumptions on a whence
$\frac {1}{a} \neq \bot $
. Similarly, it follows that
$\frac {1}{b} \neq \bot $
.
If a and b feature
$\bot $
-splitting the homomorphisms
$\phi _{0 \cdot a}$
and
$\phi _{0 \cdot b}$
do not commute. Indeed we find that
$b =_{0 \cdot a} \bot $
and that
$a =_{0 \cdot b} \bot $
. It follows that the union of
$=_{0 \cdot a}$
and
$=_{0 \cdot b}$
does not generate a congruence relation and that the transitions from M to
$M/\!=_{0 \cdot a}$
and to
$M/\!=_{0 \cdot b}$
exclude one-another. Moreover, if for non-
$\bot $
b it is the case that
$b =_{0 \cdot a} \bot $
then a and b feature non-trivial
$\bot $
-splitting in M. Indeed: if
$b + 0\cdot a = \bot + 0 \cdot a$
then
$b + 0\cdot a = \bot $
and
$0 \cdot (b + 0\cdot a) =0 \cdot \bot $
so that
$0 \cdot (a+b) = \bot $
and
$a + b = \bot $
.
Proposition 5.5. Given a GCM M which satisfies
$\mathsf {AVL}$
and which avoids non-trivial
$\bot $
-splitting, the union of the congruences
$=_{0 \cdot a}$
for all non-
$\bot $
elements a of M generates a non-trivial congruence
$=_{\mathsf {cm}}$
on M such that
$M/\!=_{\mathsf {cm}}$
is a common meadow.
Proof. In view of the absence of
$\bot $
-splitting, the union of the non-trivial congruences
$=_{0 \cdot a}$
and
$=_{0 \cdot b}$
generates the non-trivial congruence
$=_{0 \cdot (a+b)}$
. Further
$M/\!=_{\mathsf {cm}}$
is a commutative ring with inverse based common division, as any
$a \in M$
with
$0 \cdot a \neq 0$
will satisfy
$0 \cdot a =_{\mathsf {0\cdot a}} 0$
and for that reason also
$0 \cdot a =_{\mathsf {cm}} 0$
.
To see that
$M/\!=_{\mathsf {cm}}$
satisfies
$\mathsf {AVL}$
consider
$a \in M$
such that
$\frac {1}{a} =_{\mathsf {cm}} \bot $
. Then for some non-
$\bot $
,
$b \in |M|$
,
$\frac {1}{a} + 0 \cdot b=_{\mathsf {cm}} \bot + 0\cdot b= \bot $
. Because M avoids
$\bot $
-splitting and
$0 \cdot b \neq \bot $
,
$\frac {1}{a} = \bot $
so that with
$\mathsf {AVL}$
, in M,
$a = 0 \cdot a$
, and therefore
$0 \cdot a =_{\mathsf {cm}} a$
as required for the check of
$\mathsf {AVL}$
.
In case M allows non-trivial
$\bot $
-splitting, choices must be made which element of a
$\bot $
-splitting pair to map to
$0$
and which on to map to
$\bot $
as the ordering of factorisation now matters. Now, it is possible to use a a well-ordering of the non-
$\bot $
-elements in order to remove all
$\bot $
-splitting pairs.
Lemma 5.2. Given a GCM M that satisfies
$\mathsf {AVL}$
, with a non-
$\bot $
element
$a \in M$
with
$0 \neq 0 \cdot a$
, then there is a congruence
$=_{\mathsf {cm}}$
on M such that
$M/=_{\mathsf {cm}}$
is a common meadow and
$a \not =_{\mathsf {cm}} \bot $
.
Proof. Given M with properties as stated we first define the set
$U_M$
by
$$ \begin{align*}U_M = \{b \in M \mid 0 \neq b\, \&\, 0 \cdot b = b\, \&\, b \neq \bot \}.\end{align*} $$
Now, let
$\alpha $
be an ordinal with g a 1-1 mapping from the successor ordinals in
$\alpha $
to
$U_M$
such that
$g(1) = a$
. The congruences
$=^g_\beta $
for
$\beta \leq \alpha $
are as follows:
-
•
$=^g_0$
is the equality relation of M, -
• for a successor ordinal
$\beta +1$
: if
$0 \cdot g(\beta +1) =^g_{\beta }0$
or if
$0 \cdot g(\beta +1) =^g_{\beta }\bot $
then
$=^g_{\beta +1}$
is the same as
$=^g_{\beta }$
; otherwise
$=^g_{\beta +1}$
is the congruence relation generated by the union of
$=^g_{\beta }$
and
$=_{g(\beta +1)}$
, and -
• for a limit ordinal
$\beta $
,
$=^g_{\beta }\, = \bigcup _{\gamma < \beta } =^g_{\gamma }$
.
Now, we will find that
$=^g_{\alpha }$
is a nontrivial congruence on M such that in
$M/\!=^g_{\alpha }$
for every c either
$c = \bot $
or
$0 \cdot c = 0$
, so that
$M/\!=^g_{\alpha }$
is a commutative ring with inverse based common division, which satisfies
$\mathsf {AVL}$
(in view of Proposition 5.1 each factor GCM
$M/=^g_{\beta }$
satisfies
$\mathsf {AVL}$
), and which is a common meadow in view of Proposition 4.3. Moreover,
$a \not = \bot $
as in
$M/=_{g(1)} = M/=_a$
,
$a = 0$
and not
$ a = \bot $
, and all further congruences are consistent extensions of
$=_a$
.
5.3 Weak commutative rings with
$\bot$
Consider the effect on the standard properties of a ring of introducing the absorptive element
$\bot $
.
Definition 5.2. An algebra R satisfying the Equations 1–10 of Table 1 is called a weak commutative ring (
$WCR$
). An algebra
$R_\bot $
satisfying all the Equations 1–11 of Table 1 is called a weak commutative ring with
$\bot $
(
$WCR_{\bot }$
).
Every commutative ring is a weak commutative ring but not conversely. To see the latter, notice that a reduct of the common meadow
$\mathbb {Q}_\bot $
of rational numbers to the signature of rings is a weak commutative ring but it is not a ring because
$0 \cdot x = 0$
fails on
$x = \bot $
.
Lemma 5.3. For any given commutative ring R,
$R_\bot $
is a
$WCR_{\bot }$
. Further, a WCR of the form
$R_\bot $
satisfies
$\mathsf {NVL}$
$$ \begin{align*}0 \cdot x \neq 0 \to x = \bot,\end{align*} $$
and all WCR’s that satisfy this formula are of the form
$R_\bot $
.
Proof. Only the third part requires an argument. To see this it suffices that the non-
$\bot $
elements of
$R_\bot $
are closed under addition, additive inverse, and multiplication. We consider multiplication: if
$a \neq \bot $
and
$b \neq \bot $
then due to
$\mathsf {NVL}$
,
$0 \cdot a = 0$
and
$0 \cdot b = 0$
so that
$0 \cdot a \cdot b = 0 \cdot b = 0$
which contradicts
$a \cdot b = \bot $
. The other cases are dealt with similarly.
Let
$\Sigma _{r,\bot }$
be a signature of rings and fields with
$\bot $
. Now, given a WCR
$R_\bot $
the algebra
$(R_\bot )_\div $
is obtained by expanding
$R_\bot $
with a division function
$x \div y$
such that
$x \div y = x \cdot (1 \div y)$
and
$1 \div a$
is b if
$ a \cdot b = 1$
(such b is unique, see Lemma 3.1 and Definition 8.1 below), and
$1 \div a$
is undefined if no proper inverse b is available for a in
$R_\bot $
, where a proper inverse of x is an element
$x'$
so that
$x \cdot x' = 1$
. We notice that if
$R_\bot $
is non-trivial, then
$(R_\bot )_\div $
is a partial algebra.
Although
$\bot \in R_\bot $
already, for
$(R_\bot )_\div $
we totalise and define
$\mathsf {Enl}_\bot ((R_\bot )_\div )$
by having
$a \div b = \bot $
whenever
$a \div b$
is undefined in
$(R_\bot )_\div $
.
Proposition 5.6.
$\mathsf {Enl}_\bot ((R_\bot )_\div )$
satisfies
$E_{\mathsf {ftc-cm}}$
if, and only if,
$R_\bot $
satisfies
$\mathsf {NVL}$
:
$0 \cdot x \neq 0 \to x = \bot $
.
Proof. According to Lemma 5.3, if
$R_\bot $
satisfies
$\mathsf {NVL}$
then it is of the form
$\mathsf {Enl}_\bot (R)$
for some ring R. Then it follows that
$\mathsf {Enl}_\bot ((R_\bot )_\div )$
satisfies
$E_{\mathsf {ftc-cm}}$
.
For the other direction, assume that
$\mathsf {Enl}_\bot ((R_\bot )_\div )$
satisfies
$E_{\mathsf {ftc-cm}}$
and suppose
$a \in R_\bot $
satisfies
$0 \cdot a \neq 0$
and
$a \neq \bot $
. We consider
$b = 1 + 0 \cdot a$
. We first notice
$b \neq \bot $
, as otherwise:
$\bot = \bot + (-1) = b + (-1) = (1 + 0 \cdot a) + (-1) = 0 \cdot a$
so that
$a = (1+0) \cdot a = a + \bot = \bot $
. Thus if
$b^{-1}$
is defined in
$\mathsf {Enl}_\bot ((R_\bot )_\div )$
it must be a proper inverse of b. We find
$ b^{-1} = (1 + 0 \cdot a)^{-1} = 1 + 0 \cdot a = b$
, so that
$$ \begin{align*}1 = b \cdot b^{-1} = (1 + 0 \cdot a) \cdot (1 + 0 \cdot a) = 1 + (0 + 0) \cdot a + (0 \cdot a) \cdot (0 \cdot a) = 1 + 0 \cdot a\end{align*} $$
thus
$0 \cdot a = 0$
in contradiction with the assumptions on a.
We notice that a WCR which does not satisfy
$0 \cdot x \neq 0 \to x = \bot $
is easy to find: add a constant c and take an initial algebra of
$K = \mathsf {Alg}(\Sigma _{r, \bot , c}, E_{\mathsf {ftc-cm}})$
.
In [Reference Dias and Dinis21] one finds results concerning precisely which WCR’s have an expansion to a model of
$E_{\mathsf {ftc-cm}}$
(i.e., to a generalised common meadow).
Recalling from Section 2.3 the notation of [Reference Bergstra and Tucker12], for a common meadow M,
$\mathsf {Pdt}_\bot (M)$
is a meadow (= field with partial division). For a commutative ring with common division
$R_{\div , \bot }$
,
$\mathsf {Pdt}_\bot (R_{\div , \bot })$
is a commutative ring with partial division, and for an integral domain with common division
$R_{\div , \bot }$
,
$\mathsf {Pdt}_\bot (M)$
is an integral domain with partial division.
6 Examples of conditional equations
We are interested in an axiomatisation of the conditional equational theory of common meadows. First, we will look at some examples and see that the equations for common meadows (i.e.,
$E_{\mathsf {ftc-cm}}$
) allow the derivation of various conditional equations. Because
$\mathsf {AVL}$
is a conditional equation true in all common meadows but not valid in all models of
$E_{\mathsf {ftc-cm}}$
, we wonder if
$E_{\mathsf {ftc-cm}}+\mathsf {AVL}$
provides a complete axiomatisation of the conditional equational theory of common meadows. In Proposition 6.5 below we find that this is not the case, thus setting the stage for further investigation in Section 7.
6.1 Deriving conditional equations
Obviously, all non-trivial (
$0 \neq 1$
) commutative rings with inverse based common division satisfy the conditional equation
$0 = 1 \to 0 = \bot .$
More generally:
Proposition 6.1.
$E_{\mathsf {ftc-cm}} \vdash 0 = 1 \to 0 = \bot $
.
Proof.
$E_{\mathsf {ftc-cm}} \cup \{0=1 \} \vdash 0 =1 = \frac {1}{1} = \frac {1}{0} = \bot $
.
However, the structure
$A_0$
in which
$0=1, \bot \neq 0$
and
$$ \begin{align*}0 +0 = 0+1 = 0 \cdot 0 = 0 \cdot 1 =0, \ \bot + 0 = \bot + 1 = \bot + \bot= \bot\end{align*} $$
satisfies
$E_{\mathsf {wcr},\bot }$
while it rejects
$0 = 1 \to 0 = \bot $
. We find that
$E_{\mathsf {wcr},\bot } \not \vdash 0 = 1 \to 0 = \bot .$
It follows that
$E_{\mathsf {ftc-cm}}$
is not a conservative extension of
$E_{\mathsf {wcr},\bot }$
.
As a strengthening of
$E_{\mathsf {ftc-cm}} \vdash 0 = 1 \to 0 = \bot $
we find:
Proposition 6.2.
$E_{\mathsf {ftc-cm}} \vdash x = x+ 1 \to x = \bot .$
Proof. We will make implicit use of the axioms of
$E_{\mathsf {ftc-cm}}$
. Suppose
$x = x + 1$
then
$x -x = (x+1) - x= (x-x) + 1$
so that
$0 \cdot x = 0 \cdot x + 1$
. Now
$0 \cdot x = 1 + 0 \cdot x = \frac {1} {1 + 0 \cdot x} = \frac {1} {0 \cdot x} = \frac {1}{0} \cdot \frac {1}{ x}= \bot \cdot \frac {1}{ x} = \bot $
. Thus
$x = 1 \cdot x = (1 + 0) \cdot x = x + 0 \cdot x = x + \bot = \bot $
.
Similarly we find:
Proposition 6.3.
$E_{\mathsf {ftc-cm}} \vdash 0 \cdot x = \frac {1}{y} \to x = \bot .$
Proof.
$E_{\mathsf {ftc-cm}}$
implies
$\frac {y}{y} = 1 + \frac {0}{y}$
so that with
$0 \cdot x = \frac {1}{y}$
we find
$\frac {y}{y} = y \cdot \frac {1}{y} = y \cdot 0 \cdot x = 0\cdot x + 0 \cdot y = 1 + \frac {0}{y} = 1 + 0 \cdot \frac {1}{y} = 1 + 0 \cdot 0 \cdot x = 1 + 0 \cdot x$
Upon adding
$0 \cdot y$
on both sides
$0\cdot x + 0 \cdot y + 0\cdot y = 1 + 0\cdot x + 0\cdot y \ \textrm {and} \ 0\cdot x + 0 \cdot y = 1 + 0\cdot x + 0\cdot y$
so that
$0\cdot x + 0 \cdot y = 1 + 0\cdot x + 0\cdot y $
and with Proposition 6.2
$0\cdot x + 0 \cdot y = \bot $
. Then with
$0\cdot x + 0 \cdot y = 1 + 0\cdot x$
as derived above we have
$1 + 0\cdot x= \bot $
from which
$x= \bot $
easily follows.
Proposition 6.4. If
$M \models x + y = \bot \to t=r$
in all common meadows M then
$E_{\mathsf {ftc-cm}} \vdash x + y = \bot \to t=r$
.
Proof. Suppose t contains both x and y as free variables then, using arguments from [Reference Bergstra, Ponse, de Nicola and Hennicker8] or [Reference Bergstra and Tucker16],
$E_{\mathsf {ftc-cm}} \vdash t = t + 0\cdot x + 0 \cdot y = \bot $
, so that in all common meadows
$r = \bot $
. In this case apply fracterm flattening and choose terms p over the signature of rings such that
$E_{\mathsf {ftc-cm}} \vdash r = \frac {p}{q}$
. It follows that in all common meadows (and for that reason in all fields F),
$q = 0$
so that
$E_{\mathsf {ftc-cm}} \vdash q = 0$
and
$E_{\mathsf {ftc-cm}} \vdash r = \bot $
, whence
$E_{\mathsf {ftc-cm}} \vdash t = r$
.
We may then focus on the case that both t and r contain at most one variable of x and y. We assume that t does not contain y and then we distinguish two cases:
(i) x occurs in t and y occurs in r, in which case
$E_{\mathsf {ftc-cm}} \vdash t = t + 0\cdot x$
and
$E_{\mathsf {ftc-cm}} \vdash r = r + 0\cdot y$
so that in all common meadows
$\bot = t + 0 \cdot x + 0 \cdot y = t + 0 \cdot y = r + 0 \cdot y = r$
. From this observation we find that, upon choosing
$x= \bot $
,
$\bot = r$
holds in all common meadows so that it is derivable from
$E_{\mathsf {ftc-cm}} $
according to the completeness result of [Reference Bergstra and Tucker16]. The case that y occurs in t and x occurs in r is dealt with symmetrically.
(ii) y does not occur in t in which case
$y $
occurs in neither t and r, then choosing
$y = \bot $
we find that
$t = r$
is valid in all common meadows so that it is derivable from
$E_{\mathsf {ftc-cm}} $
according to the completeness result of [Reference Bergstra and Tucker16].
6.2 AVL and conditional equations
As an example of the use of this rule consider the following conditional equation:
$$ \begin{align*}\phi_{2,3,5} \equiv \frac{0}{2} \cdot \frac{0}{3} = \frac{0}{2} \cdot \frac{0}{5} \to \frac{0}{3} = \frac{0}{5}.\end{align*} $$
Lemma 6.1.
$\phi _{2,3,5}$
holds in all common meadows.
Proof. This is a simple case distinction. Note that the conclusion may be written as
$0 \cdot \frac {1}{3} = 0 \cdot \frac {1}{5}$
.
Assuming
$\frac {0}{2} \cdot \frac {0}{3} = \frac {0}{2} \cdot \frac {0}{5} $
and
$\frac {1}{3} = \bot $
we will show that
$\frac {0}{5} = \bot $
, leaving the proof that with
$\frac {1}{5} = \bot $
one may derive
$\frac {1}{3} = \bot $
to the reader. If
$\frac {1}{3} = \bot $
then it is immediate that
$ 0 \cdot 3 = 0 \cdot (1 + 1 + 1) = 0$
, moreover with
$\mathsf {AVL}$
one finds
$0 \cdot 3 = 3$
so that
$3 = 0$
. Then
$ 5 \cdot 2 = 1 + 9 = 1\ \mod 3$
, so that
$2$
is the inverse of
$5$
and conversely. It follows that
$0 \cdot (5 \cdot 2) = 0 \cdot 1 = 0$
and thus
$0 \cdot 5 = 0$
and
$0 \cdot 2 = 0$
so that
$\frac {0}{5} = 0$
and
$\frac {0}{2} = 0$
.
Now the condition
$ \frac {0}{2} \cdot \frac {0}{3} = \frac {0}{2} \cdot \frac {0}{5}$
can be used, and upon substitution of the now known facts this yields:
$0 \cdot \bot = 0 \cdot 0$
and thus
$\bot = 0$
, which suffices to obtain
$\frac {0}{3} = \frac {0}{5}$
.
Proposition 6.5.
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL} \not \vdash \phi _{2,3,5} $
.
Proof. A model of
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL}$
in which
$\phi _{2,3,5} $
fails can be found following the structure theory for GCM’s as set out in [Reference Dias and Dinis21, Reference Dias and Dinis22]. The underlying idea is that all GCM’s M, contain a lattice
$L_M$
made up by elements from
$0 \cdot M$
. Let
$m \in 0 \cdot M$
then m determines the subring of M which consists of multiples of
$1 + m$
.
A common meadow always has 2-element lattice containing
$0$
and
$\bot $
only. The same holds for commutative rings with inverse based common division. Each element
$b \in L_M$
of the lattice serves as the zero for a ring
$R^b$
.
We consider a structure with a three element lattice containing:
$0, c, \bot $
. Here c can be understood as an element which satisfies
$c = 0 \cdot c$
and
$c = c + \frac {0}{p} $
for all primes p.
$R_{0} $
is a copy of
$\mathbb {Z}(\frac {1}{3})$
, that is the ring of integers augmented with a constant for
$\frac {1}{3}$
which satisfies
$3 \cdot \frac {1}{3} = 1$
and
$R^c$
, the substructure generated by c is a common meadow of rational numbers, denoted as
$Q_{\bot }$
.
We assume that the domain of
$R_{0} $
is made up of simplified fracterms with as denominators powers of
$3$
only, while the domain of
$R_{0} $
is made of of all simplified fracterms. The natural isomorphism
$\iota \colon \mathbb {Z}(\frac {1}{3}) \to Q_{\bot }$
(i.e., from
$R_{0} $
to
$R_{c} $
) is needed to describe the operations of M:
$p \star q = p \star _{R_c} q$
, for all pairs
$p,q \in R_c$
,
$\star \in \{+,-, \cdot ,\div \}$
;
$p \star q = \iota (p) \star _{R_c} q$
, for all pairs
$p \in R_0,q \in R_c$
,
$\star \in \{+,-, \cdot ,\div \}$
;
$p \star q = p \star _{R_c} \iota (q)$
, for all pairs
$p \in R_c,q \in R_0$
,
$\star \in \{+,-, \cdot ,\div \}$
;
$p \star q = p \star _{R_0}q$
, for
$p,q \in R_0$
,
$\star \in \{+,-, \cdot \}$
;
$p \div 0 = \bot $
for
$p \in R_0$
;
$p \div q = \iota (p) \div \iota (q)$
for all q with a numerator that is not a power of
$3$
.
It is an elementary check of axioms that M satisfies
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL}$
and indeed
$M\not \models \phi _{2,3,5}$
.
Consider the following conditional equation
$\phi $
:
$$ \begin{align*}\phi \equiv u \cdot x + v \cdot y \cdot z = 1 \wedge \frac{0}{x} \cdot \frac{0}{y} = \frac{0}{x} \cdot \frac{0}{z} \to \frac{0}{y} = \frac{0}{z}.\end{align*} $$
It is easy to see that
$\phi $
is valid in all common meadows and that for all primes p, q and r
$$ \begin{align*}E_{\mathsf{ftc-cm}} \cup \{\phi\} \vdash \frac{0}{p} \cdot \frac{0}{q} = \frac{0}{p} \cdot \frac{0}{r} \to \frac{0}{q} = \frac{0}{r}.\end{align*} $$
Nevertheless, we offer this:
Conjecture 6.1. There is no finite set of conditional equations E, true of all common meadows, such that
$E_{\mathsf {ftc-cm}} \cup E$
provides a complete axiomatisation of the conditional equational theory of common meadows.
7 Customising the logic of common meadows and completeness
We continue the search for an axiomatisation of the conditional theory of common meadows and for this purpose we introduce a proof rule which is sound for all common meadows and in fact more generally, as noted in Proposition 7.1. Using this additional rule, a completeness result is obtained in Theorem 7.2.
7.1 Adding a new proof rule
The following proof rule is sound for common meadows, with E a conjunction of equations:
$$ \begin{align*}\mathsf{R_{cm}}\,\,\frac{\vdash E \wedge t = \bot \to r =\bot, \ \vdash E \wedge r = \bot \to t=\bot} { \vdash E \to 0 \cdot t=0 \cdot r}.\end{align*} $$
We denote derivability in the proof system of conditional equational logic extended with
$\mathsf {R_{cm}}$
by
$\vdash _{\mathsf {R_{cm}}}$
. The following observation is immediate.
Proposition 7.1. The proof system
$\vdash _{\mathsf {R_{cm}}}$
is sound for commutative rings with inverse based common division.
As
$\mathsf {AVL}$
fails in commutative rings with inverse based common division that are not fields (Proposition 4.3), and in view of Proposition 7.1,
$\mathsf {AVL}$
is not derivable with
$\vdash _{\mathsf {R_{cm}}}$
from
$E_{\mathsf {ftc-cm}}$
.
We will write
$\models _{\mathsf {cm}}$
for satisfaction in all common meadows and
$\vdash _{\mathsf {cm/avl}}$
for derivability from
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL}$
.
Lemma 7.1. If
$\models _{\mathsf {cm}} E\to \frac {1}{t} = \bot $
then
$\vdash _{\mathsf {cm/avl}} E \to \frac {1}{t} = \bot $
.
Proof. Suppose
$\not \vdash _{\mathsf {cm/avl}} \frac {1}{t} = \bot $
then for some GCM M which satisfies
$ \mathsf {AVL}$
it is the case that for some substitution
$\vec {c}$
of the free variables of
$E \to \frac {1}{t} = \bot $
it is the case that
$\frac {1}{t(\vec {c})} \neq \bot $
. We have to find a common meadow in which this is also true.
Consider the mapping
$\phi (x) = x + 0 \cdot \frac {1}{t}$
. First of all, we notice that
$\phi (1) \neq \bot $
, as otherwise it would be so that
$1 + 0 \cdot \frac {1}{t} = \bot $
which implies
$\frac {1}{t} = \bot $
. Thus,
$\phi $
is a homomorphism to a GCM, say
$M'$
, where
$$ \begin{align*}t(\vec{\phi(c)})\cdot \frac{1}{t(\vec{\phi(c)})} = 1 + \frac{0}{t(\vec{\phi(c)})} = \phi(1 + \frac{0}{t(\vec{c})}) = \phi(1) = 1\end{align*} $$
which also satisfies
$\mathsf {AVL}$
in view of Lemma 5.1. In
$M'$
,
$E \to \frac {1}{t} = \bot $
is not valid on the substitution
$\vec {\phi (c)}$
. To see the this, notice that the homomorphism
$\phi $
preserves all conditions while
$\frac {1}{t(\vec {\phi (c)})}$
implies
$ 1 = \bot $
against the assumption on M. With Lemma 5.2 we find the existence of a homomorphic
$M"$
image of
$M'$
which is a common meadow and in which the image of
$t({\phi (\vec{c})})$
is invertible so that
$\frac {1}{t(\vec {c})} \neq \bot $
.
Lemma 7.2. If
$\models _{\mathsf {cm}} E\to t = 0 \cdot t$
then
$\vdash _{\mathsf {cm/avl}} t = 0 \cdot t$
.
Proof. Assuming
$\models _{\mathsf {cm}} E\to t = 0 \cdot t$
we have
$\models _{\mathsf {cm}} E\to \frac {1}{t} = \bot $
so that with Lemma 7.1
$\vdash _{\mathsf {cm/avl}} E \to \frac {1}{t} = \bot $
whence with
$\mathsf {AVL}$
$\vdash _{\mathsf {cm/avl}} E \to t = 0 \cdot t = \bot $
.
Theorem 7.1. If
$\models _{\mathsf {cm}} E\to t = \bot $
then
$\vdash _{\mathsf {cm/avl}} E \to t = \bot $
.
Proof. Using fracterm flattening we may write t as
$\frac {p(\vec {x})}{q(\vec {x})}$
where p and q are division free and, moreover, it may be assumed that all variables occurring in p are also present in q. So, we assume that
$\models _{\mathsf {cm}} t = \frac {p(\vec {x})}{q(\vec {x})}$
. Assuming
$\models _{\mathsf {cm}} E \to \frac {p(\vec {x})}{q(\vec {x})} = \bot $
we have that in each common meadow for each substitution either the numerator of
$\frac {p(\vec {x})}{q(\vec {x})}$
equals
$\bot $
or the denominator equals
$0$
or
$\bot $
. Now if the numerator is
$\bot $
then for at least one variable
$\bot $
has been substituted so that the denominator equals
$\bot $
as well. In each of these cases
$q(\vec {x})\cdot 0 = q(\vec {x})$
in the substitution at hand. It follows that
$\models _{\mathsf {cm}} E \to q(\vec {x})\cdot 0 = q(\vec {x})$
so that, with Lemma 7.2,
$\vdash _{\mathsf {cm/avl}} q(\vec {x})\cdot 0 = q(\vec {x})$
from which it follows trivially that
$\vdash _{\mathsf {cm/avl}} t = \bot $
Lemma 7.3. If
$\models _{\mathsf {cm}} E \wedge 0 \cdot t = 0 \cdot r \to t = r$
then
$\vdash _{\mathsf {cm/avl}} E \wedge 0 \cdot t = 0 \cdot r \to t = r$
.
Proof. In the style of the proof of Lemma 7.1 we consider a GCM M that satisfies
$\mathsf {AVL}$
and which refutes
$E \wedge 0 \cdot t = 0 \cdot r \to t = r$
. For some substitution
$\vec {c}$
for the relevant free variables the conditions are true while t and r take different values: in M:
$t(\vec {c}) \neq r(\vec {c})$
. Consider
$s = \frac {1}{t(\vec {c}) - r(\vec {c})}$
in
$M'$
. We claim that
$s \neq \bot $
. Otherwise, with
$\mathsf {AVL}$
,
$t(\vec {c}) - r(\vec {c}) = 0 \cdot (t(\vec {c}) - r(\vec {c}))$
, so that
$t(\vec {c}) - r(\vec {c}) + r(\vec {c})= 0 \cdot (t(\vec {c}) - r(\vec {c})) + r(\vec {c})$
and, with
$x + 0\cdot x = x$
and the condition
$0 \cdot t(\vec {c}) = 0 \cdot r(\vec {c})$
it follows that
$t(\vec {c}) = r(\vec {c})$
in contradiction with the assumptions on
$M'$
. Now we may consider the homomorphism
$\phi (x) = x + 0 \cdot s$
. The image of
$\phi $
is a GCM, that satisfies
$\mathsf {AVL}$
in which
$t(\vec {c}) \neq r(\vec {c})$
differs from
$\bot $
, as otherwise
$1 = t(\vec {c}) \neq r(\vec {c}) \cdot s= \bot $
. Thus
$M'$
refutes
$E \wedge 0 \cdot t = 0 \cdot r \to t = r$
, but now on a substitution
$\vec {\phi (c)}$
which makes
$t-r$
invertible. Using Theorem 5.2 we find a homomorphic image
$M" = \psi (M')$
of
$M'$
which is a common meadow and in which
$E \wedge 0 \cdot t = 0 \cdot r \to t = r$
is refuted on the substitution
$\psi (\phi (\vec {c}))$
.
Completeness can be obtained with the help of the additional rule
$\mathsf {R_{cm}}$
.
Theorem 7.2.
$\models _{\mathsf {cm}} E \to t = r$
if, and only if,
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL} \vdash _{\mathsf {cm}} E \to t = r$
.
Proof. Soundness of the proof system for its purpose is obvious. For completeness, we notice that if
$\models _{\mathsf {cm}} E \to t = r$
also
$\models _{\mathsf {cm}} E \wedge t = \bot \to r = \bot $
with Lemma 7.1 also
$\vdash _{\mathsf {cm/avl}} E \wedge t = \bot \to r = \bot $
. Similarly, symmetrically,
$\vdash _{\mathsf {cm/avl}} E \wedge r = \bot \to t = \bot $
. So, with
$\mathsf {R_{cm}}$
we obtain
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL} \vdash _{\mathsf {cm}} E \to 0 \cdot t=0 \cdot r$
.
Obviously,
$\models _{\mathsf {cm}} E \wedge 0 \cdot t = 0 \cdot r \to 0 \cdot t=0 \cdot r$
, as the additional condition does no harm. With Lemma 7.3, we find
$\vdash _{\mathsf {cm/avl}} \vdash E \wedge 0 \cdot t=0 \cdot r \to t=r$
, and in combination with
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL} \vdash _{\mathsf {cm}} E \to 0 \cdot t=0 \cdot r$
we find
$E_{\mathsf {ftc-cm}}+ \mathsf {AVL} \vdash _{\mathsf {cm}} E \to t = r$
.
We do not know whether or not the use of an additional rule—
$\mathsf {R_{cm}}$
or otherwise—is necessary for a finite and complete axiomatisation of the conditional equational theory of common meadows, although as stated above we expect this to be the case. Nevertheless, a foundational open problem regarding common meadows remains Problem 1.1.
Instead of the rule
$\mathsf {R_{cm}}$
we may also use a less symmetric, and less intuitive, but technically simpler rule
$\mathsf {R_{cm}'}$
$$ \begin{align*}\mathsf{R_{cm}'}\,\,\frac{\vdash E \wedge t = \bot \to r =\bot} { \vdash E \to 0 \cdot r=0 \cdot (t+r)}\end{align*} $$
Using
$\mathsf {R_{cm}'}$
it is easy to obtain
$\mathsf {R_{cm}}$
as a derived rule. The other direction is not obvious, however, and we leave open the question whether or not
$\mathsf {R_{cm}'}$
is stronger than
$\mathsf {R_{cm}}$
.
7.2 Expanding common meadows with a conditional operator
Finally, we extend the signature of common meadows with a conditional operator. In particular, we propose to work with
$x \vartriangleleft y \vartriangleright z$
understood as
$$ \begin{align*}\text{"if } y=0 \text{ then } z \text{ else } x\text{, where } \bot \text{ is returned if } y = \bot\text{"}. \end{align*} $$
The conditional operator is not strict in all arguments, e.g.,
$0 \vartriangleleft 1 \vartriangleright \bot = 0$
. Nevertheless, it is easily shown, from the axioms in Table 3, that for
$a \neq \bot $
,
$\phi _a(x) = x + 0 \cdot a$
is a homomorphism w.r.t. the conditional operator. It follows that the completeness result of Theorem 7.2 can be generalised to the signature of common meadows expanded with the conditional operator.
$E_{\mathsf {Cond-Op}}$
: Axioms for the conditional operator.
8 Integral domains with
$\bot $
8.1 Basics
A integral domain with common division is a commutative ring with common division
$\mathsf {Enl}_\bot (R_{\div })$
that is based on a ring R that is an integral domain, i.e., it has no zero divisors: for all
$a, b \in R$
,
$$ \begin{align*}a \cdot b = 0 \to a = 0 \vee b = 0.\end{align*} $$
Let
$\mathsf {CID}_{\div , \bot }$
be the class of all such algebras. We notice that in personal communication Bruno Dinis suggested a somewhat stronger requirement for integral domains with inverse based common division, the implications of which we have not investigated.
$$ \begin{align*}a \cdot b = 0 \cdot a \cdot b \to 0 \cdot a = a \vee 0 \cdot b = b.\end{align*} $$
Clearly, every common meadow is an integral domain with common division, and each integral domain with common division is a commutative ring with common division, and both inclusions are proper. In symbols,
$$ \begin{align*}\mathsf{CM} \subsetneqq \mathsf{CID}_{\div, \bot} \subsetneqq \mathsf{CR}_{\div, \bot}.\end{align*} $$
Proposition 8.1. Every integral domain with common division can be extended to a common meadow.
Proof. Consider an integral domain with common division
$M= \mathsf {Enl}_\bot (R_{\div })$
where the ring R is an integral domain. Let
$R'$
be a field of fractions for R then
$M' = \mathsf {Enl}_\bot ((R')_{\div })$
is a common meadow which extends M.
Because integral domains with common division are a subclass of commutative rings with common division, the conditional equational theory of integral domains with common division includes the conditional equational theory of commutative rings with common division.
Proposition 8.2. The conditional equational theory of integral domains with common division is a proper extension of the conditional equational theory of commutative rings with common division. In fact, these inclusions are proper:
$$ \begin{align*}ConEqnThy(\mathsf{CR}_{\bot,\div}) \subsetneqq ConEqnThy(\mathsf{CID}_{\bot,\div}) \subsetneqq ConEqnThy(\mathsf{CM}).\end{align*} $$
Proof. For the first proper extension we notice that
$\mathsf {AVL}$
is true in all common meadows but not in the ring of integers enlarged with inverse based common division. For the second proper inclusion we notice that the conditional equation
$\phi \equiv x \cdot x = 0 \to x = 0$
is true in any integral domain with common division, while it fails in a commutative ring with common division based on a ring of dual numbers (we refer to [Reference Bergstra4] for dual numbers in a setting of meadows).
The conditional equation
$\phi \equiv x \cdot x \cdot y = 0 \to x \cdot y = 0$
is true for all integral domains, it is provable from
$E_{\mathsf {ftc-cm}} + \mathsf {AVL}$
but it is stronger than
$x \cdot x = 0 \to x = 0$
as it excludes all rings with non-zero nil-potent elements.
Recall, a quasivariety is a class of algebras definable by conditional equations. Again we have:
Proposition 8.3. The class of integral domains with common division is not a quasivariety.
Proof. Suppose for a contradiction that some conditional equational theory
$E_{ce}$
has precisely the commutative rings with common division as its models. We introduce fresh constants c and d. We consider an initial algebra of
$E' = E_{ce} \cup \{ c\cdot d = 0\}$
. Now, there is a ring with common division
$M_1$
that satisfies
$E'$
by taking
$c= 1$
and
$d = 0$
from which it follows that
$E' \not \vdash c = 0$
. Similarly, there is a model
$M_2$
of
$E'$
in which
$d=0$
and
$c = 1$
so that
$E' \not \vdash d= 0$
. It follows that in an initial algebra of
$E'$
,
$c \cdot d = 0$
while
$c \neq 0$
and
$d\neq 0$
.
However, the latter situation cannot occur in any structure of the form
$\mathsf {Enl}_\bot (R_{\div })$
with R an integral domain, because
$c \cdot d = 0$
implies
$c\neq \bot $
and
$d \neq \bot $
so that
$c \in R$
and
$d \in R$
, whence
$c\cdot d = 0 \in R$
, so that
$c\cdot d = 0 $
in
$\mathsf {Enl}_\bot (R_{\div })$
While the common meadows can be characterised with a single conditional equation as a subclass of the commutative rings with common division (Proposition 4.3), a corresponding characterisation of the integral domains with common division is not so easy to find.
Problem 8.1. Is there a set of conditional equations
$T^{ce}_{idcd} $
true of all integral domains with inverse based common division such that a commutative ring with common division is an integral domain with common division if, and only, if it satisfies
$T^{ce}_{idcd}$
? If so is there a finite set
$T^{ce}_{idcd}$
with the mentioned properties?
The equational theory of integral domains with inverse based common division is the same as the equational theory of common meadows and as the equational theory of commutative rings with inverse based common division. The following issue is left open.
Problem 8.2. Is there a finite axiomatisation with conditional equations of the conditional equational theory of integral domains with inverse based common division?
8.2 A second definition of division for integral domains
Recall our convention where we change notation from
$\div $
to the familiar fraction notations when appropriate. We now introduce a second kind of division (for integral domains) and extend our flexible convention relying on the context. Thus, as long as the divisions are declared, fracterms can continue to have these forms
$$ \begin{align*}p \div q, \ \displaystyle \frac{p}{q}, \ p/q.\end{align*} $$
Here is another definition for division in case the ring R is an integral domain.
Definition 8.1. Let R be an integral domain. Then it has a unique partial division operator
$-/-$
defined by
(i) if
$b \neq 0$
and
$ b\cdot c = a$
(c is unique in this respect) then
$ a / b =_{\mathit {def}} c$
,
(ii) if
$b= 0$
or if for no
$c \in R$
,
$ b \cdot c = a$
then
$a/ b $
is undefined.
Lemma 8.1. Let R be an integral domain. In case (i) of Definition 8.1 above if such c exists then it is unique.
Proof. If such c exists it is unique because of the absence of zero-divisors in R: if also
$ b\cdot c' = a$
then
$a - a = b\cdot c - b\cdot c' = b\cdot (c - c' ) = 0$
, and then, given that
$b \neq 0$
,
$c-c'=0$
, and thus
$c = c'$
.
Extending a ring R with this operator
$/$
creates a ring with partial general division denoted
$R_{/}$
. This general form of division is more familiar in arithmetic.
Example 8.1. In
$\mathbb {Z}$
there are more divisions (in comparison with inverse based division): the equation
$b \cdot x = 1$
(for defining
$\frac {1}{b}$
) has solutions whenever x divides b, e.g.,
$12/1 =12, 12/2 = 6, 12/3 = 4, 12/4 = 3$
, and
$ 12/6 = 2$
all exist and are unique.
The requirement that we work over a ring without zero divisors is needed. For instance in the finite ring
$\mathbb {Z}_{6}$
, the equation
$4 \cdot x = 2 \ mod \ 6$
has solutions
$2/4 = 2$
because
$2 = 2 \cdot 4 \ mod \ 6 = 8 \ mod \ 6 =2$
and
$2/4 = 5$
because
$2 = 5 \cdot 4 \ mod \ 6 = 20 \ mod \ 6 =2$
. So, unless working over an integral domain, divisions are not necessarily unique but may be multivalued. This complication is absent for inverse based division, however.
However,
$\mathsf {Enl}_\bot (R_{/})$
does not satisfy the equations of
$E_{\mathsf {ftc-cm}}$
.
Proposition 8.4.
$\mathsf {Enl}_\bot (R_{/})\not \models E_{\mathsf {ftc-cm}}$
.
Proof. For instance with
$R=\mathbb {Z}$
,
$\mathsf {Enl}_\bot (R_{/}) \models \frac {1}{3} \cdot \frac {3}{1} = \bot \cdot 3 = \bot $
while
$\mathsf {Enl}_\bot (R_{/}) \models \frac {1 \cdot 3}{3 \cdot 1} = \frac {3}{3} = 1$
, which refutes Equation 13 of
$E_{\mathsf {ftc-cm}}$
.
Actually,
$\mathsf {Enl}_\bot (\mathbb {Z}_{/}) $
satisfies the axioms of
$E_{\mathsf {ftc-cm}}$
with the important exceptions of Equations 13, and 14. Given Proposition 8.4, a typical open problem regarding equational logic over these rings with common division is as follows.
Problem 8.3. Does
$\mathsf {Enl}_\bot (\mathbb {Z}_{/})$
allow fracterm flattening?
As far as we can see, there is no straightforward approach to equational reasoning in
$\mathsf {Enl}_\bot (R_{/})$
with standard first order (i.e., Tarski) semantics. Yet, we consider
$\mathsf {Enl}_\bot (R_{/})$
to be a more natural structure than
$\mathsf {Enl}_\bot (R_{\div })$
because direct common division is more often defined (infinitely often in the case of
$R=\mathbb {Z}$
). Defining division with the use of the multiplicative inverse as an intermediate step is fine when working in a field, but doing so is less convincing when working in a ring. However, clearly, the equations for
$\mathsf {Enl}_\bot (R_{/})$
are less attractive than the equations for
$\mathsf {Enl}_\bot (R_{\div })$
.
9 Rings with division and eager equality semantics
9.1 Eager equality
In [Reference Bergstra and Tucker14, Reference Bergstra and Tucker15] we have introduced and investigated in some detail an alternate way of identifying two expressions with partial operations. Called eager equality, and denoted
$\approx $
, its general form is as follows.
Let 
denote the value of term t in a partial algebra A and write
$t \downarrow $
if 
is defined and
$t \uparrow $
if 
is not defined. Naturally, when the expressions are defined in A, eager equality of expressions is the same as equality
$=$
in A:
However, if one or other, or both, of t and
$t'$
are not defined then eager equality
$\approx $
satisfies
$$ \begin{align*}t \uparrow \textrm{or/and} \ t' \uparrow \implies t \approx t'.\end{align*} $$
Thus, eager equality means that if an expression is undefined then all other expressions – defined or not—will be deemed equal to it. This motivates the description ‘eager’. Finally, we note that
$$ \begin{align*}t \not\approx t' \iff t \ \downarrow \textrm{and} \ t' \downarrow \textrm{and} \ t \neq t'.\end{align*} $$
Eager equality is symmetric and reflexive, but it is not transitive. Eager equality satisfies what we call safe transitivity:
$$ \begin{align*}x \approx y \wedge y \approx z \wedge y \not\approx w \to x \approx z.\end{align*} $$
Here transitivity requires that y differs from
$\bot $
, a condition which is guaranteed by the existence of some element w with
$y \not \approx w$
. The relation of eager equality satisfies the congruence property, i.e., operations of A preserve
$\approx $
. Eager equality contrasts with one of the oldest notions of partial equality, that of Kleene equality, which requires both the expressions to be either defined and equal, or both undefined [Reference Kleene25]. As emphasised in our [Reference Bergstra and Tucker14], eager equality is something rather different and unusual.
Let A be be a total or partial algebra and let non-empty
$V \subseteq A$
, then with
$\langle A \rangle _V$
we denote the subalgebra of A with domain limited to V and operations made partial on inputs in V when their values lie outside V or do not exist. We compare the totalisations
$\mathsf {Enl}_\bot (A)$
with
$\mathsf {Enl}_\bot (\langle A \rangle _V)$
. The proof of the following observation is straightforward.
Proposition 9.1. Given a partial algebra A of signature
$\Sigma $
and an equation
$t=r$
over
$\Sigma _\bot $
, then
$\mathsf {Enl}_\bot (A)\models t=r$
implies
$\mathsf {Enl}_\bot (\langle A \rangle _V)\models _{\mathit {eager}} t=r$
.
Proof. The modification that takes place by turning
$\mathsf {Enl}_\bot (A)$
into
$\mathsf {Enl}_\bot (\langle A \rangle _V)$
only introduces more occurrences of
$\bot $
as a function value. Such modifications cannot invalidate an equation w.r.t. to eager equality.
Example 9.1. We are interested in instances of this construction when
$A = F$
is a field and
$V = R \subseteq F$
is a ring. Then, with
$F_\div $
denoting F enriched with a partial division operator, we find that
$\mathsf {Enl}_\bot (\langle F_\div \rangle _{R})$
will satisfy in eager equality semantics all equations—including and especially
$E_{\mathsf {ftc-cm}}$
—which
$F_\div $
satisfies in standard first order semantics. A typical example of this state of affairs is found with
$F = \mathbb {Q}$
and
$R = \mathbb {Z} \subseteq \mathbb {Q}$
.
Example 9.2. Another instance of the construction is where upper and lower bounds are introduced into common meadows, as discussed in [Reference Bergstra, Tucker and Jansen17]. This works as follows: We restrict the domain of
$\mathsf {Enl}_\bot (\mathbb {Q}_\div )$
to an interval
$V = (-b,b)$
for some rational bound
$b>1$
to make
$\mathsf {Enl}_\bot (\langle \mathbb {Q}_\div \rangle _V)$
. We find that bounded meadows thus defined fail to satisfy the equations of
$E_{\mathsf {ftc-cm}}$
in ordinary first order semantics. However, the equations of
$E_{\mathsf {ftc-cm}}$
are satisfied in
$\mathsf {Enl}_\bot (\langle \mathbb {Q}_\div \rangle _V)$
in eager equality semantics.
9.2 Eager equality and the axioms for common division
Now we notice that for an integral domain R,
$\mathsf {Enl}_\bot (R_{/}) $
eager equality validates all of
$E_{\mathsf {ftc-cm}}$
and allows fracterm flattening for that reason.
Proposition 9.2. Let R be an integral domain. Then
$\mathsf {Enl}_\bot (R_{/}) \models _{eager} E_{\mathsf {ftc-cm}}$
.
Proof. Let
$R'$
be a field extending R with
$R^{\prime }_{/}$
as its corresponding partial meadow with general division. Then
$R_{/}$
is a partial algebra coinciding with
$R^{\prime }_{/}$
except for the fact that division in
$R_{/}$
is a subfunction of division in
$R^{\prime }_{/}$
, i.e., the graph of division in
$R_{/}$
is contained in the graph of division in
$R^{\prime }_{/}$
.
It follows that with
$a_1,\ldots ,a_n$
in R, if
$t(a_1,\ldots ,a_n) = r(a_1,\ldots ,a_n)$
follows from
$E_{\mathsf {ftc-cm}}$
it holds in
$\mathsf {Enl}_\bot (R^{\prime }_{/})$
. Now, it must be confirmed that
$t(a_1,\ldots ,a_n) =_{eager} r(a_1,\ldots ,a_n)$
in
$\mathsf {Enl}_\bot (R^{\prime }_{/})$
. If either
$t(a_1,\ldots ,a_n)= \bot $
or
$r(a_1,\ldots ,b_n) = \bot $
in
$\mathsf {Enl}_\bot (R_{/})$
then the equality holds in eager semantics. Otherwise, if both
$t(a_1,\ldots ,a_n)$
and
$r(a_1,\ldots ,a_n)$
are defined in
$\mathsf {Enl}_\bot (R_{/})$
then both terms are defined in
$R_{/}$
and, necessarily, also defined and equal in
$R^{\prime }_{/}$
. Since they cannot differ in
$R^{\prime }_{/}$
they cannot differ in
$\mathsf {Enl}_\bot (R_{/})$
.
We conjecture that Problem 8.3 has a negative answer. Thus, in order to justify fracterm flattening in ring-like structures of the form
$\mathsf {Enl}_\bot (R_{/})$
we find an incentive to contemplate eager equality. Although eager equality has a problematic logic—because it is not transitive—nevertheless we consider eager equality to provide a meaningful semantics for fracterm calculus for this general division over an integral domain. In other words: for plausible structures with division—in particular, for
$\mathsf {Enl}_\bot (R_{/})$
with R an integral domain—the (very plausible!) equational logic of
$E_{\mathsf {ftc-cm}}$
is not sound w.r.t. to Tarski semantics, while it is sound w.r.t. the (less plausible!) eager equality semantics.
Actually, these observations create a good conceptual case for studying and deploying eager equality. They match with the observation in [Reference Bergstra and Tucker15] that working with rewrite rules which are sound for eager equality provides a plausible approach to term rewriting for common meadows.
Notice that
$\mathsf {AVL}$
fails under eager equality in a common meadow of rational numbers, say on
$x=2$
. More technically, consider the conditional equation
$$ \begin{align*}\phi \equiv 0 = \bot \to 0 = 1.\end{align*} $$
We notice that
$\phi $
is valid in all common meadows because the premise never holds. At the same time, however, using eager equality instead of ordinary equality,
$\phi $
is invalid in all common meadows because the premise always holds while the conclusion never holds. We further notice that the conditional equation
$\phi _{2,3,5}$
as introduced in Section 6.2 is valid in all common meadows under eager equality.
10 Concluding remarks
We will reflect on the diversity of algebraic models and logical theories suitable for computer arithmetics, focussing on totality.
10.1 Various forms of total divisions
Given the original motivation to study arithmetical structures as abstract data types suitable for computer specification and computation, the classical algebra of fields is an obvious starting place: field theory provides a comprehensive axiomatic theory of the rational, real and complex numbers, and calculating with polynomials and solving polynomial equations. This theory is widely taken to be the foundation for what many creators and users of mathematics rely on in their work.Footnote 2 However, in computing, as we noted in the Introduction, it is in need of modification to be ‘fit for purpose’ as a tool for the specification of data types.
The modification needed and studied here is to add division and make it total. Elsewhere we have studied several ways of accomplishing this for fields by making different semantic choices for
$\frac {x}{0}$
. Using various semantical values to be found in practical computations—such as
$\mathsf {error}$
,
$\infty $
,
$\mathit {NaN}$
, the last standing for ‘not a number’—we have constructed equational specifications (under initial algebra semantics) for the following data types of meadows of rational numbers:
Involutive meadows, where an element of the meadow’s domain is used for totalisation, in particular
$1/0 = 0$
, [Reference Bergstra and Tucker9, Reference Ono28, Reference Suppes30].
Common meadows, the subject of this paper, where a new external element
$\bot $
that is ‘absorptive’ is used for totalisation
$1/0 = \bot $
, [Reference Bergstra, Ponse, de Nicola and Hennicker8, Reference Bergstra and Tucker13, Reference Bergstra and Tucker16].
Wheels, where one external
$\infty $
is used for totalisation
$1/0 = \infty = -1/0$
, together with an additional external error element
$\bot $
to help control the side effects of infinity, [Reference Bergstra, Tucker and Roggenbach11, Reference Carlström20, Reference Setzer29].
Transrationals, where besides the error element
$\bot $
, two external signed infinities are added, one positive and one negative, so that division is totalised by setting
$1/0 = \infty $
and
$-1/0 = -\infty $
, [Reference Anderson, Völker, Adams, Latecki, Mount and Wu2, Reference Bergstra and Tucker10, Reference dos Reis, Gomide and Anderson23].
Symmetric Transrationals, where to the error element
$\bot $
, and two external signed infinities, are added two infinitesimals along with upper and lower bounds, [Reference Bergstra, Tucker and Jansen17].
In practice, these models are based on data type conventions to be found in theorem provers, common calculators, exact numerical computation and, of course, floating point computation, respectively. For some historical remarks on division by zero, we mention [Reference Anderson and Bergstra1], and for a survey we mention [Reference Bergstra3].
Our results here and elsewhere point to the fact that arithmetical abstract data types with error values are theoretically superior among the many practical conventions we have studied. The other meadows run into fundamental algebraic difficulties that the common meadows do not. For example, a problem for the involutive case is the failure of flattening composed fractional expressions—compare Section 3.3.1. In [Reference Bergstra, Bethke and Ponse6] it is shown that, with the axioms for involutive meadows, terms are provably equal to only finite sums of flat fracterms; and in [Reference Bergstra and Middelburg7], it is shown that arbitrarily large numbers of summands of flat fracterms are needed for that purpose.
Acknowledgments
We thank João Dias, Bruno Dinis and Alban Ponse for several useful comments made by them on two preparatory drafts of the paper. We thank the referee for their comments and suggestions.
Funding
This research programme is supported exclusively by our universities.
