Meadows and the equational specification of division 1 J A Bergstra Informatics Institute, University of Amsterdam, Science Park 403, 1098 SJ Amsterdam, The Netherlands 2 Y Hirshfeld Department of Mathematics, Tel Aviv University, Tel Aviv 69978, Israel 9 3 J V Tucker 0 0 2 Department of Computer Science, Swansea University, n Singleton Park, Swansea, SA2 8PP, United Kingdom a J 7 Abstract ] A The rational, real and complex numbers with their standard operations, including R division, are partial algebras specified by the axiomatic concept of a field. Since the . h class of fieldscannot bedefinedby equations, the theory of equational specifications t a of data types cannot use field theory in applications to number systems based upon m rational, real and complex numbers. We study a new axiomatic concept for number [ systems with division that uses only equations: a meadow is a commutative ring 1 with a total inverse operator satisfying two equations which imply 0−1 = 0. All v fields and products of fields can be viewed as meadows. After reviewing alternate 3 2 axioms for inverse, we start the development of a theory of meadows. We give 8 a general representation theorem for meadows and find, as a corollary, that the 0 conditional equational theory of meadows coincides with the conditional equational . 1 theory of zero totalized fields. We also prove representation results for meadows of 0 9 finite characteristic. 0 : v Keywords. Field, totalized fields, meadow, division-by-zero, total versus partial i functions, representation theorems, initial algebras, equational specifications, von X Neumann regular ring, finite meadows, finite fields. r a 1 Introduction At the heart of the theory of data types are the ideas of specifying the properties of data using equations and conditional equations, performing calculations and reasoning 1 Email: [email protected] 2Email: [email protected] 3Email: [email protected] 1 using term rewriting, and modelling all data representations and implementations using algebras. The theory combines mathematical simplicity, beauty and usefulness, especially when using equations and total operations. Confidence in the scope and explanatory power of the theory was established in its first decade, 1975-85, when it was proved that any computable data type possesses a range of equational specifications with desirable properties, such as having few equations (e.g., [5, 6, 7]), or equations with valuable term rewritingproperties(e.g.,[8]). Sinceeverycomputabledatatypecanbeequationallyspec- ified - and, indeed, there are special specifications that define all and only computable data types - we expect that any data type arising in computing can be specified by equa- tions and studied using the theory. The search for, and study of, equational specifications of particular computational structures is long term activity, contributing to foundational thinking in diverse areas of computer science, such as programming languages, hardware verification, graphics, etc. For the theoretician, it is a challenge to develop and perfect the properties of specifications far beyond those delivered by the general theory. Despite achievements in many areas, one does not have far to look for a truly funda- mental challenge. Algebras of rational, real and complex numbers make use of operations whose primary algebraic properties are captured by the axioms of the concept of field. The field axioms consist of the equations that define commutative rings and, in particular, two axioms that are not equations that define the inverse operator and the distinctness of the two constants. Now, division is a partial operation, because it is undefined at 0, and the class of fields cannot be defined by any set of equations. Thus, the theory of equa- tionalspecifications ofdata types cannot buildonthetheoryof fields; moreover, data type theory has rarely been applied to number systems based upon rational, real and complex numbers. However, we know that, say, the field of rational numbers is a computable data type - arguably, it is the most important data type for measurement and computation. Therefore, thanks to general theory, computable data types of rational, real and complex numbers with division do have equational specifications. This fact leads to two problems: we must search for, and study, 1. equational specifications of particular algebras of rational, reals and complex num- bers with division; and, ideally, 2. equational specifications of classes of number algebras with division that are as elegant and useful as the theory of fields. Having begun to tackle Problem 1 in [9, 10, 1], this paper considers Problem 2 and introduces a new axiomatisation for number systems with division, called the meadow, which uses only equations. A meadow is a commutative ring with unit equipped with a total unary operation x−1, named inverse, that satisfies these additional equations: −1 −1 (x ) = x (1) −1 x·(x·x ) = x. (2) The first equation we call Ref, for reflection, and the second equation Ril, for restricted inverse law. Meadows provide a mathematical analysis of division which is more general than the classical theory of fields. Meadows are total algebras in which, necessarily, 0−1 = 0. We have used algebras with such zero totalized division in developing elementary algebraic 2 specifications for several algebras of numbers in our previous papers [9, 10, 1]. The raison d’ˆetre of meadows is to be a tool that extends our understanding and techniques for making specifications. Clearly, since meadows are commutative rings they also have pure mathematical interest. Let us survey our results. In [9], an equational specification under initial algebra semantics of the zero totalized field of rational numbers was presented, and specifications for other zero totalized fields were developed in [10] and [1]. In [9] meadows were isolated byexploring alternateequationalaxiomsforinverse. Specifically, 12 equationswere found; a set CR of 8 equations for commutative rings was extended by a set SIP of 3 equations for inverse, including Ref, and by Ril. The single sorted finite equational specification CR + SIP + Ril has all zero totalized fields among its models and, in addition, a large class of structures featuring zero divisors. A model of CR + SIP + Ril was baptized a meadow in [9]. Because meadows are defined by equations, finite and infinite products of zero totalized fields are meadows as well. Our first result will be that two of the equations from CR + SIP + Ril can be de- rived from the other ones. This establishes the subset Md, consisting of 10 equations of the 12 equations, including the 8 equations for CR and the equations Ref and Ril men- tioned earlier. Our second result makes an intriguing connection between meadows and commutative von Neumann regular rings. Our main task is to start to make a classification of meadows up to isomorphism. We prove the following general representation theorem: Theorem Up to isomorphism, the non-trivial meadows are precisely the subalgebras of products of zero totalized fields. From this theorem we deduce this corollary: Theorem The equational theory of meadows and the equational theory of fields with zero totalized division are identical. This strengthens a result for closed equations in [9]. Now we prove the following ex- tension: Theorem The conditional equational theory of meadows and the conditional equational theory of fields with zero totalized division are identical. Next, we examine the relationship between fields and meadows of finite characteristic. The characteristic of a meadow is the smallest natural number n ∈ N such that n.1 = 1 + 1 + ... + 1 = 0. A prime meadow is a meadow without a proper submeadow and without a proper non-trivial homomorphic image. Given a positive natural number k, and writing k for the numeral for k, we can define Md for the initial algebra of Md +{k = 0}, i.e., k ∼ Md = I(Σ,Md ∪{k = 0}). k 3 The following results are obtained: Theorem For k a prime number, Md is the zero totalized prime field of characteristic k. k Theorem For k a square free number, Md has cardinality k. k In the matter of Problem 1 above, only recently, Moss found in [20] that there exists an equational specification of the ring of rationals (i.e., without division or inverse) with just one unary hidden function. In [9] we proved that there exists a finite equational specification under initial algebra semantics, without hidden functions, but making use of an inverse operation, of the field of rational numbers. In [10], the specification found for the rational numbers was extended to the complex rationals with conjugation, and in [1] a specification was given of the algebra of rational functions with field and degree operations that are all total. Full details concerning the background of this work can be found in [9]. Weassume thereader isfamiliar withthebasics ofringtheory (e.g., [19,21]), algebraic specifications (e.g., [24]), universal algebra (e.g., [23, 17]) and term rewriting (e.g., [22]). 2 Axioms for fields and meadows We will add to the axioms of a commutative ring various alternative axioms for dealing with inverse and division. The starting point is a signature Σ for commutative rings CR with unit: signature Σ CR sorts ring operations 0: → ring; 1: → ring; +: ring ×ring → ring; −: ring → ring; ·: ring ×ring → ring end To the signature Σ we add an inverse operator −1 to form the primary signature Σ, CR which we will use for both fields and meadows: signature Σ import Σ CR operations −1: ring → ring end 4 2.1 Commutative rings and fields The first set of axioms isthat of acommutative ring with 1, which establishes thestandard properties of +, −, and ·. equations CR (x+y)+z = x+(y +z) (3) x+y = y +x (4) x+0 = x (5) x+(−x) = 0 (6) (x·y)·z = x·(y ·z) (7) x·y = y ·x (8) x·1 = x (9) x·(y +z) = x·y +x·z (10) end These axioms generate a wealth of properties of +,−,· with which we will assume the reader is familiar. We will write x−y as an abbreviation of x+(−y). 2.1.1 Axioms for meadows Having available an axiomatization of commutative rings with unit (such as the one above), we define the equational axiomatization of meadows by Md = (Σ,CR+Ref +Ril). 2.1.2 Axioms for fields On the basis of the axioms CR for commutative rings with unit there are different ways to proceed with the introduction of division. The orthodoxy is to add the following two axioms for fields: let Gil (general inverse law) and Sep (separation axiom) denote denote the following two axioms, respectively: −1 x 6= 0 =⇒ x·x = 1 (11) 0 6= 1 (12) Let (Σ,T ) be the axiomatic specification of fields, where T = CR + Gil + Sep. field field About the status of 0−1 these axioms say nothing. This may mean that the inverse is: (1) a partial function, or (2) a total function with an unspecified value, or (3) omitted as a function symbol but employed pragmatically as a useful notation in some “self-explanatory” cases. 5 Case 3 arises in another approach to axiomatizing fields, taken in many text-books, which is not to have an operator symbol for the inverse at all and to add an axiom Iel (inverse existence law) as follows: x 6= 0 =⇒ ∃y(x·y = 1). Each Σ algebra satisfying T also satisfies Iel. In models of (Σ ,CR+Iel +Sep) field CR the inverse is implicit as a single-valued definable relation, so we call this theory the relational theory of fields RTF. 2.1.3 Totalized division in fields In field theory, if the decision has been made to use a function symbol for inverse the value of 0−1 is either left undefined, or left unspecified. However, in working with elementary specifications, which we prefer, operationsaretotal. This lineof thoughtleads tototalized division. The class Alg(Σ,T ) is the class of all possible total algebras satisfying the axioms field in T . For emphasis, we refer to these algebras as totalized fields. field Now, for all totalized fields A ∈ Alg(Σ,T ) and all x ∈ A, the inverse x−1 is defined. field −1 −1 Let 0 be the zero element in A. In particular, 0 is defined. The actual value 0 = a A A A −1 can be anything but it is convenient to set 0 = 0 (see [9], and compare, e.g., Hodges A A [16], p. 695). Definition 2.1. A field A with 0−1 = 0 is called zero totalized. A A This choice gives us a nice equation to use, the zero inverse law Zil: −1 0 = 0. With ZTF, an extension of T , we specify the class of zero totalized fields: field ZTF = T +Zil = CR +Gil+Sep+Zil. field Let Alg(Σ,ZTF) denote the class of all zero totalized fields. Lemma 2.2. Each Σ algebra satisfying CR+Iel+Sep can be expanded to a Σ algebra CR with a unique inverse operator that satisfies ZTF. Proof. To see this notice that if x·y = 1 and x·z = 1 it follows by subtraction of both equations that x·(y −z) = 0. Now: y −z = 1·(y −z) = (x·y)·(y −z) = x·(y −z)·y = 0·y = 0, which implies that y = z and that the inverse is unique. Let x−1 be the function that produces this unique value (for non-zero arguments). Choose 0−1 to be 0 and a zero totalized field has been built. 6 2.1.4 Equations for zero totalized division Following [9], one may replace the axioms Gil and Sep by other axioms for division, es- pecially, the three equations in a unit called SIP for strong inverse properties. They are considered “strong” because they are equations involving −1 without any guards, such as x 6= 0. These three equations were used already by Harrison in [15]. equations SIP1,SIP2 and SIP3 −1 −1 (−x) = −(x ) (13) −1 −1 −1 (x·y) = x ·y (14) −1 −1 (x ) = x (15) end The following was proven in [9]: Proposition 2.3. CR∪SIP ⊢ 0−1 = 0. 2.2 Meadows and Ril In [9] we add to CR+SIP the equation Ril (restricted inverse law): x·(x·x−1) = x which, using commutativity and associativity, expresses that x·x−1 is 1 in the presence of x. We may write x·x−1 as 1 , in which case we have the following alternative formulations x of Ril, −1 −1 1 ·x = x and 1 ·x = x , x x and also 1x = 1x−1. Following [9] we define: Definition 2.4. A model of CR+SIP +Ril is called a meadow. Shortly, we will demonstrate that this definition is equivalent to the definition of a meadow given in the introduction. A meadow satisfying Sep is called non-trivial. Example All zero totalized fields are clearly non-trivial meadows but not conversely. In particular, the zero totalized prime fields Z of prime characteristic are meadows. p That the initial algebra of CR + SIP + Ril is not a field follows from the fact that (1+1)·(1+1)−1 = 1 cannot be derivable because it fails to hold in the prime field Z2 of characteristic 2 which is a model of these equations as well. Whilst the initial algebra of CR is the ring of integers, we found in [9] that Lemma 2.5. The initial algebra of CR+SIP +Ril is a computable algebra but it is not an integral domain. 7 2.3 Derivable properties of meadows We will now derive some equational facts from the specification Md or relevant subsets of it. Proposition 2.6. CR +Ril ⊢ x·x−1 = 0 ↔ x = 0. Proof. Indeed, we have x·x−1 = 0 =⇒ x·x−1 ·x = 0·x, by multiplication. Thus, x = 0 by applying Ril to the LHS and simplifying the RHS. The other direction is immediate from 0·x = 0. To improve readability we denote x−1 by x and use 1 = x·x−1. Recall that 1 = 1 . x x x Proposition 2.7. Implicit definition of inverse: CR +Ril ⊢ x·y = 1 → x−1 = y Proof. x = 1·x = x·y·x = 1 ·y = (1 +0)·y = (1 +0·x)·y = (1 +(x−x)·x)·y = x x x x (1 +(x·1−x·x·x)·x)·y = (1 +(x·x·y−x·x·x)·x)·y = (1 +x·x·(y−x)·x)·y = x x x (1 +x·(y −x))·y = (1 +x·y −x·x)·y = x·y ·y = 1·y = y x x Proposition 2.8. Derivability of SIP1 and SIP2: 1. Md ⊢ (xy)−1 = x−1y−1 2. Md ⊢ (−x)−1 = −(x−1) Proof. 1. First we show that 1 = 1 ·1 . Indeed we have: 1 ·1 ·1 = x·y·xy·x·x·y·y xy x y xy x y Applying Ril twice we have x · y · x · x · y · y = x · y , and therefore 1 · 1 · 1 = xy x y x · y · xy = 1 . On the other hand applying Ril once we have x · y · xy · x · y = x · y xy and therefore 1 ·1 ·1 = x·y ·x·y = 1 ·1 This proves the auxiliary equation. Now: xy x y x y xy = xy ·1 = xy ·1 ·1 = xy ·x·x·y ·y = 1 ·x·y = 1 ·1 ·x·y = x·y. xy x y xy x y 2. Thefactthat−1 = −1followsbyanapplicationofProposition2.7to(−1)·(−1) = 1 which is a consequence of CR. We now conclude with the help of 1: −x = (−1)·x = (−1)·x = (−1)·x = −x Thanks to Proposition 2.8 we obtain: Corollary 2.9. Md axiomatizes the meadows, i.e. Md is equivalent to CR +SIP +Ril. Proposition 2.10. 1. CR +Ril+SIP2 ⊢ x2 = x → x = x−1 2. Md ⊢ x3 = x → x = x−1, and 3. Md ⊢ x4 = x → x = x−2. Proof. 1. x = x·x·x−1 = x·x−1 = x·(x·x)−1 = x·x−1 ·x−1 = x−1. 2. From the assumption we obtain x3 · x−1 = x · x−1 and then x · x = x · x−1. Thus x·x·x−1 = x·x−1 ·x−1 whence x = ((x·x−1 ·x−1)−1)−1 = (x−1 ·x·x)−1 = x−1. 3. From the assumption we obtain x4 ·x−1 = x·x−1 and then x3 = x·x−1, from which we get x3 ·x−1 = x·x−1 ·x−1 and x2 = x−1. 8 2.4 Meadows and von Neumann regular rings with unit Acommutative von Neumann regular ring (e.g., see [19,13]) is aΣ algebra that satisfies CR CR and which in addition satisfies the following axiom regular ring (RR): ∀x.∃y.(x·y ·x = x). A value y which satisfies x·y ·x = x is called a pseudoinverse of x. Because Ril indicates that x−1 is a pseudoinverse of x, the Σ -reduct of a meadow CR is a commutative von Neumann regular ring and every meadow is an expansion of a von Neumann regular ring. As it turns out a converse is true. We acknowlege Robin Chapman (Exeter UK) for pointing out to us the following observation: Lemma 2.11. Everycommutative regularvonNeumannring canbe expandedto ameadow. Moreover, this expansion is unique. First, we notice a lemma that holds for any commutative ring. Lemma 2.12. Given an x, any y with x·x·y = x and y ·y ·x = y is unique. Proof. Assume that, in addition, x·x·z = x and z ·z ·x = z. By subtracting the first equations of both pairs, we get x·x·(y−z) = 0, which implies x·x·(y−z)·y = 0·y, on multiplying both sides by y. Since x·x·y = x, we deduce that x·(y −z) = 0 and that x·y = x·z. Now, substituting into y·y·x = y, this yields y·z·x = y; and substituting into z ·z ·x = z it yields z ·y ·x = z; taken together, we conclude y = z. Proof. Then we proceed with the proof of Lemma 2.11. Suppose that Σ algebra A CR satsifies RR. First, expand the A to an algebra A′ with an operator i : ring → ring that satisfies x · i(x) · x = x. This function i need not be unique, because i(0) can take any value in A. However, if j(x) is another function on the domain of A such that for all x, x·j(x)·x = x, then for all x, i(x)·x·i(x) = j(x)·x·j(x). To see this, write: p(x) = i(x) · x · i(x) and q(x) = j(x) · x · j(x). Now x · x · p(x) = x·x·i(x)·x·i(x) = x·x·i(x) = x and p(x)·p(x)·x = i(x)·x·i(x)·i(x)·x·i(x)·x = i(x) ·x· i(x) ·i(x) · x = x·i(x) ·i(x) = p(x). An application of Lemma 2.12 establishes that p(x) = q(x) for all x. It follows that p is independent of the choice of i. Then expand A′ to the Σ algebra A′′ by introducing an inverse operator as follows: x−1 = p(x) = i(x)·x·i(x). We will show that bothRil and Ref aresatisfied. ForRil we make use of theequations just derived for p(−) and find: x·x·x−1 = x·x·p(x) = x. Now Ref has to be established for the proposed inverse operator. In order to prove that (u−1)−1 = u, write x = u−1, y = x−1 and z = u. Then, using straightforward calculations, we obtain: x·x·y = x, y·y·x = y, x·x·z = x and z ·z ·x = z. It follows by Lemma 2.12 that y = z, which is the required identity. To see that the expansion is unique suppose that two unary functions p(−) and q(−) both satisfy Ref and Ril. Using Lemma 2.8 both functions satisfy p(x·y) = p(x) ·p(y) 9 and q(x·y) = q(x)·p(y), respectively. Given an arbitrary x we find: x·x·p(x) = x by assumptiononp(−). Applying p(−)onbothsideswefindp(x·x·p(x)) = p(x), whichusing SIP2 implies p(x)·p(x)·p(p(x)) = p(x). Then, using Ref we have p(x)·p(x)·x = p(x). Similarly we find x·x·q(x) = x and q(x)·q(x)·x = q(x). By means of Lemma 2.12 this yields p(x) = q(x). The uniqueness of inverse as an expansion of commutative rings satisfying Ref and Ril indicates that the inverse operation can be implicitly defined on a commutative von Neumann regular ring. The Beth definability theorem implies the existence of an explicit definition for inverse. In this case the application of Beth definability is inessential, however, because from the proof of Lemma 2.11 an explicit definition can be inferred for y = x−1: ∃z.(x·z ·x = x&y = z ·x·z). 3 The embedding theorem Because the theory of meadows is equational we know from universal algebra (see [17, 23]) that: Theorem 3.1. The class of meadows is closed under subalgebras, direct products and homomorphic images. Thus, every subalgebra of a product of zero totalized fields is a meadow. Our main task is to show that every non-trivial meadow is isomorphic to a subalgebra of a product of zero totalized fields. First, we recall some basic properties of commutative rings, which can be found in many textbooks (e.g., [19]). 3.1 Preliminaries on rings Let R be a commutative ring. An ideal in a ring R is a subset I with 0, and such that if x,y ∈ I and z ∈ R, then x+y ∈ I, and z ·x ∈ I. R itself and {0} are the trivial ideals. Any other ideal is a proper ideal. The ideal R·x = {y ·x| y ∈ R } is the principal ideal generated by x. Since R has a unit, the generator x = x·1 is in R·x. This is the smallest ideal that includes x. If I is an ideal then the following relation is a Σ congruence: CR x ≡ y iff x−y ∈ I. The set of classes R/I is a ring. The quotient map maps every element a of R to its equivalence class, which is denoted by a + I or by a/I. The quotient map is a Σ CR homomorphism from R onto R/I (an epimorphism). It is clear what it means that I is a maximal ideal in R. Lemma 3.2. Every ideal is contained in (at least one) maximal ideal. Proof. The union ofa chain ofideals containing I andnot 1 doesnot include 1. Therefore, by Zorn’s lemma there is a maximal such ideal. 10