Showing 1–26 of 26 results for author: Bergstra, J A

Sumterms, Summands, Sumtuples, and Sums and the Meta-arithmetic of Summation

Authors: Jan A. Bergstra

Abstract: Sumterms are introduced as syntactic entities, and sumtuples are introduced as semantic entities. Equipped with these concepts a new description is obtained of the notion of a sum as (the name for) a role which can be played by a number. Sumterm splitting operators are introduced and it is argued that without further precautions the presence of these operators gives rise to instance of the so-call… ▽ More Sumterms are introduced as syntactic entities, and sumtuples are introduced as semantic entities. Equipped with these concepts a new description is obtained of the notion of a sum as (the name for) a role which can be played by a number. Sumterm splitting operators are introduced and it is argued that without further precautions the presence of these operators gives rise to instance of the so-called sum splitting paradox. A survey of solutions to the sum splitting paradox is given. △ Less

Submitted 18 September, 2020; originally announced September 2020.

Universality of Univariate Mixed Fractions in Divisive Meadows

Authors: Jan A. Bergstra, Inge Bethke, Dimitri Hendriks

Abstract: Univariate fractions can be transformed to mixed fractions in the equational theory of meadows of characteristic zero. Univariate fractions can be transformed to mixed fractions in the equational theory of meadows of characteristic zero. △ Less

Submitted 3 July, 2017; originally announced July 2017.

Comments: 12 pages

Equational Axioms for Expected Value Operators

Authors: Jan A. Bergstra

Abstract: An equational axiomatisation of probability functions for one-dimensional event spaces in the language of signed meadows is expanded with conditional values. Conditional values constitute a so-called signed vector meadow. In the presence of a probability function, equational axioms are provided for expected value, variance, covariance, and correlation squared, each defined for conditional values.… ▽ More An equational axiomatisation of probability functions for one-dimensional event spaces in the language of signed meadows is expanded with conditional values. Conditional values constitute a so-called signed vector meadow. In the presence of a probability function, equational axioms are provided for expected value, variance, covariance, and correlation squared, each defined for conditional values. Finite support summation is introduced as a binding operator on meadows which simplifies formulating requirements on probability mass functions with finite support. Conditional values are related to probability mass functions and to random variables. The definitions are reconsidered in a finite dimensional setting. △ Less

Submitted 25 May, 2019; v1 submitted 9 September, 2016; originally announced September 2016.

Comments: The notation has been somewhat simplified with reference to the notions of assimilation and dis-assimilation as have been put forward by Nicaud et. al. in 2001. Some typographical improvements were performed. An open problem statement has been removed

Transformation of fractions into simple fractions in divisive meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Meadows are alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Divisive meadows are meadows with the multiplicative inverse operation replaced by a division operation. Viewing a fraction as a term over the signature of divisive mead… ▽ More Meadows are alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Divisive meadows are meadows with the multiplicative inverse operation replaced by a division operation. Viewing a fraction as a term over the signature of divisive meadows that is of the form p / q, we investigate which divisive meadows admit transformation of fractions into simple fractions, i.e. fractions without proper subterms that are fractions. △ Less

Submitted 25 February, 2016; v1 submitted 21 October, 2015; originally announced October 2015.

Comments: 23 pages; one theorem and two corollaries of it added at end of Sect. 5; some minor errors corrected

MSC Class: 12E12; 12L12; 68Q65

Journal ref: Journal of Applied Logic, 16:92--110, 2016

Subvarieties of the variety of meadows

Authors: Jan A. Bergstra, Inge Bethke

Abstract: Meadows - commutative rings equipped with a total inversion operation - can be axiomatized by purely equational means. We study subvarieties of the variety of meadows obtained by extending the equational theory and expanding the signature. Meadows - commutative rings equipped with a total inversion operation - can be axiomatized by purely equational means. We study subvarieties of the variety of meadows obtained by extending the equational theory and expanding the signature. △ Less

Submitted 19 April, 2016; v1 submitted 14 October, 2015; originally announced October 2015.

Comments: 11 pages

Meadow based Fracterm Theory

Authors: Jan A. Bergstra

Abstract: Fracterms are introduced as a proxy for fractions. A precise definition of fracterms is formulated and on that basis reasonably precise definitions of various classes of fracterms are given. In the context of the meadow of rational numbers viewing fractions as fracterms provides an adequate theory of fractions. A very different view on fractions is that fractions are values, i.e. rational numbers.… ▽ More Fracterms are introduced as a proxy for fractions. A precise definition of fracterms is formulated and on that basis reasonably precise definitions of various classes of fracterms are given. In the context of the meadow of rational numbers viewing fractions as fracterms provides an adequate theory of fractions. A very different view on fractions is that fractions are values, i.e. rational numbers. Fracterms are used to provide a range of intermediate definitions between these two definitions of fractions △ Less

Submitted 6 June, 2019; v1 submitted 6 August, 2015; originally announced August 2015.

Comments: The paper has been completely rewritten. Now 48 pages, additional references from educational literature are included. The title has been adapted in order to highlight the central position of fracterms, of which the definition of fractions is now considered an application

A negative result on algebraic specifications of the meadow of rational numbers

Authors: Jan A. Bergstra, Inge Bethke

Abstract: $\mathbb{Q}_0$ - the involutive meadow of the rational numbers - is the field of the rational numbers where the multiplicative inverse operation is made total by imposing $0^{-1}=0$. In this note, we prove that $\mathbb{Q}_0$ cannot be specified by the usual axioms for meadows augmented by a finite set of axioms of the form $(1+ \cdots +1+x^2)\cdot (1+ \cdots +1 +x^2)^{-1}=1$. $\mathbb{Q}_0$ - the involutive meadow of the rational numbers - is the field of the rational numbers where the multiplicative inverse operation is made total by imposing $0^{-1}=0$. In this note, we prove that $\mathbb{Q}_0$ cannot be specified by the usual axioms for meadows augmented by a finite set of axioms of the form $(1+ \cdots +1+x^2)\cdot (1+ \cdots +1 +x^2)^{-1}=1$. △ Less

Submitted 22 January, 2016; v1 submitted 2 July, 2015; originally announced July 2015.

Comments: 5 pages, 2 tables

MSC Class: 12D15

Poly-infix operators and operator families

Authors: Jan A. Bergstra, Alban Ponse

Abstract: Poly-infix operators and operator families are introduced as an alternative for working modulo associativity and the corresponding bracket deletion convention. Poly-infix operators represent the basic intuition of repetitively connecting an ordered sequence of entities with the same connecting primitive. Poly-infix operators and operator families are introduced as an alternative for working modulo associativity and the corresponding bracket deletion convention. Poly-infix operators represent the basic intuition of repetitively connecting an ordered sequence of entities with the same connecting primitive. △ Less

Submitted 5 May, 2015; originally announced May 2015.

Comments: 8 pages

MSC Class: 97B50; 97D30 ACM Class: I.1.1

Fracpairs and fractions over a reduced commutative ring

Authors: Jan A. Bergstra, Alban Ponse

Abstract: In the well-known construction of the field of fractions of an integral domain, division by zero is excluded. We introduce "fracpairs" as pairs subject to laws consistent with the use of the pair as a fraction, but do not exclude denominators to be zero. We investigate fracpairs over a reduced commutative ring (a commutative ring that has no nonzero nilpotent elements) and provide these with natur… ▽ More In the well-known construction of the field of fractions of an integral domain, division by zero is excluded. We introduce "fracpairs" as pairs subject to laws consistent with the use of the pair as a fraction, but do not exclude denominators to be zero. We investigate fracpairs over a reduced commutative ring (a commutative ring that has no nonzero nilpotent elements) and provide these with natural definitions for addition, multiplication, and additive and multiplicative inverse. We find that modulo a simple congruence these fracpairs constitute a "common meadow", which is a commutative monoid both for addition and multiplication, extended with a weak additive inverse, a multiplicative inverse except for zero, and an additional element "a" that is the image of the multiplicative inverse on zero and that propagates through all operations. Considering "a" as an error-value supports the intuition. The equivalence classes of fracpairs thus obtained are called common cancellation fractions (cc-fractions), and cc-fractions over the integers constitute a homomorphic pre-image of the common meadow Qa, the field Q of rational numbers expanded with an a-totalized inverse. Moreover, the initial common meadow is isomorphic to the initial algebra of cc-fractions over the integer numbers. Next, we define canonical term algebras for cc-fractions over the integers and some meadows that model the rational numbers expanded with a totalized inverse, and provide some negative results concerning their associated term rewriting properties. Then we consider reduced commutative rings in which the sum of two squares plus one cannot be a zero divisor: by extending the equivalence relation on fracpairs we obtain an initial algebra that is isomorphic to Qa. Finally, we express negative conjectures concerning alternative specifications for these (concrete) datatypes. △ Less

Submitted 22 January, 2016; v1 submitted 17 November, 2014; originally announced November 2014.

Comments: 25 pages, 8 tables

MSC Class: 13B30; 16S85 ACM Class: B.2.0; F.4.1

Journal ref: Indagationes Mathematicae, 27(3):727-748, 2016

Note on paraconsistency and reasoning about fractions

Authors: Jan A. Bergstra, Inge Bethke

Abstract: We apply a paraconsistent logic to reason about fractions. We apply a paraconsistent logic to reason about fractions. △ Less

Submitted 6 March, 2015; v1 submitted 31 October, 2014; originally announced October 2014.

Comments: 6 pages

Report number: report TCS1413, October 2014 ACM Class: F.4.1

Division by zero in common meadows

Authors: Jan A. Bergstra, Alban Ponse

Abstract: Common meadows are fields expanded with a total inverse function. Division by zero produces an additional value denoted with "a" that propagates through all operations of the meadow signature (this additional value can be interpreted as an error element). We provide a basis theorem for so-called common cancellation meadows of characteristic zero, that is, common meadows of characteristic zero that… ▽ More Common meadows are fields expanded with a total inverse function. Division by zero produces an additional value denoted with "a" that propagates through all operations of the meadow signature (this additional value can be interpreted as an error element). We provide a basis theorem for so-called common cancellation meadows of characteristic zero, that is, common meadows of characteristic zero that admit a certain cancellation law. △ Less

Submitted 22 March, 2021; v1 submitted 26 June, 2014; originally announced June 2014.

Comments: 17 pages, 4 tables; differences with v3: axiom (14) of Mda (Table 2) has been replaced by the stronger axiom (12), this appears to be necessary for the proof of Theorem 3.2.1

MSC Class: 12F99; 12L12; 68Q65 ACM Class: F.4.1

Division by zero in non-involutive meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Meadows have been proposed as alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Thus, the multiplicative inverse operation of a meadow is an involution. In this paper, we study `non-involutive meadows', i.e.\ variants of meadows in… ▽ More Meadows have been proposed as alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Thus, the multiplicative inverse operation of a meadow is an involution. In this paper, we study `non-involutive meadows', i.e.\ variants of meadows in which the multiplicative inverse of zero is not zero, and pay special attention to non-involutive meadows in which the multiplicative inverse of zero is one. △ Less

Submitted 9 June, 2014; originally announced June 2014.

Comments: 14 pages

MSC Class: 12E12; 12L12; 68Q65

Journal ref: Journal of Applied Logic, 13(1):1--12, 2015

Equations for formally real meadows

Authors: Jan A. Bergstra, Inge Bethke, Alban Ponse

Abstract: We consider the signatures $Σ_m=(0,1,-,+, \cdot, \ ^{-1})$ of meadows and $(Σ_m, {\mathbf s})$ of signed meadows. We give two complete axiomatizations of the equational theories of the real numbers with respect to these signatures. In the first case, we extend the axiomatization of zero-totalized fields by a single axiom scheme expressing formal realness; the second axiomatization presupposes an o… ▽ More We consider the signatures $Σ_m=(0,1,-,+, \cdot, \ ^{-1})$ of meadows and $(Σ_m, {\mathbf s})$ of signed meadows. We give two complete axiomatizations of the equational theories of the real numbers with respect to these signatures. In the first case, we extend the axiomatization of zero-totalized fields by a single axiom scheme expressing formal realness; the second axiomatization presupposes an ordering. We apply these completeness results in order to obtain complete axiomatizations of the complex numbers. △ Less

Submitted 13 January, 2015; v1 submitted 18 October, 2013; originally announced October 2013.

Comments: 24 pages, 14 tables, revised, new Theorem 3.7

MSC Class: 12D15

Probability functions in the context of signed involutive meadows

Authors: Jan A. Bergstra, Alban Ponse

Abstract: The Kolmogorov axioms for probability functions are placed in the context of signed meadows. A completeness theorem is stated and proven for the resulting equational theory of probability calculus. Elementary definitions of probability theory are restated in this framework. The Kolmogorov axioms for probability functions are placed in the context of signed meadows. A completeness theorem is stated and proven for the resulting equational theory of probability calculus. Elementary definitions of probability theory are restated in this framework. △ Less

Submitted 22 December, 2016; v1 submitted 19 July, 2013; originally announced July 2013.

Comments: 20 pages, 6 tables, some minor errors are corrected

MSC Class: 62F15 ACM Class: F.4.1; F.1.2

On Hoare-McCarthy algebras

Authors: Jan A. Bergstra, Alban Ponse

Abstract: We discuss an algebraic approach to propositional logic with side effects. To this end, we use Hoare's conditional [1985], which is a ternary connective comparable to if-then-else. Starting from McCarthy's notion of sequential evaluation [1963] we discuss a number of valuation congruences and we introduce Hoare-McCarthy algebras as the structures that characterize these congruences. We discuss an algebraic approach to propositional logic with side effects. To this end, we use Hoare's conditional [1985], which is a ternary connective comparable to if-then-else. Starting from McCarthy's notion of sequential evaluation [1963] we discuss a number of valuation congruences and we introduce Hoare-McCarthy algebras as the structures that characterize these congruences. △ Less

Submitted 22 December, 2010; originally announced December 2010.

Comments: 29 pages, 1 table

ACM Class: F.3.2

Short-circuit logic

Authors: Jan A. Bergstra, A. Ponse, D. J. C. Staudt

Abstract: Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with sequential conjunction and disjunction as primitive connectives. A short-circuit logic is a variant of propositional logic (PL) that… ▽ More Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with sequential conjunction and disjunction as primitive connectives. A short-circuit logic is a variant of propositional logic (PL) that can be defined with help of Hoare's conditional, a ternary connective comparable to if-then-else, and that implies all identities that follow from four basic axioms for the conditional and can be expressed in PL (e.g., axioms for associativity of conjunction and double negation shift). In the absence of side effects, short-circuit evaluation characterizes PL. However, short-circuit evaluation admits the possibility to model side effects and gives rise to various different short-circuit logics. The first extreme case is FSCL (free short-circuit logic), which characterizes the setting in which evaluation of each atom (propositional variable) can yield a side effect. The other extreme case is MSCL (memorizing short-circuit logic), the most identifying variant we distinguish below PL. In MSCL, only a very restricted type of side effects can be modelled, while sequential conjunction is non-commutative. We provide axiomatizations for FSCL and MSCL. Extending MSCL with one simple axiom yields SSCL (static short-circuit logic, or sequential PL), for which we also provide a completeness result. We briefly discuss two variants in between FSCL and MSCL, among which a logic that admits contraction of atoms and of their negations. △ Less

Submitted 12 March, 2013; v1 submitted 18 October, 2010; originally announced October 2010.

Comments: 59 pages, 7 tables, 3 figures; Daan Staudt is added as an extra author; normal forms for FSCL are defined and completeness of its axiomatization is proved

ACM Class: F.3.2

Partial Komori fields and imperative Komori fields

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: This paper is concerned with the status of 1/0 and ways to deal with it. These matters are treated in the setting of Komori fields, also known as non-trivial cancellation meadows. Different viewpoints on the status of 1/0 exist in mathematics and theoretical computer science. We give a simple account of how mathematicians deal with 1/0 in which a customary convention among mathematicians plays a… ▽ More This paper is concerned with the status of 1/0 and ways to deal with it. These matters are treated in the setting of Komori fields, also known as non-trivial cancellation meadows. Different viewpoints on the status of 1/0 exist in mathematics and theoretical computer science. We give a simple account of how mathematicians deal with 1/0 in which a customary convention among mathematicians plays a prominent part, and we make plausible that a convincing account, starting from the popular computer science viewpoint that 1/0 is undefined, by means of some logic of partial functions is not attainable. △ Less

Submitted 29 September, 2009; originally announced September 2009.

Comments: 10 pages

Report number: PRG0911 MSC Class: 12E99; 12L99

Arithmetical meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: An inversive meadow is a commutative ring with identity equipped with a multiplicative inverse operation made total by choosing 0 as its value at 0. Previously, inversive meadows were shortly called meadows. A divisive meadow is an inversive meadows with the multiplicative inverse operation replaced by a division operation. In the spirit of Peacock's arithmetical algebra, we introduce variants of… ▽ More An inversive meadow is a commutative ring with identity equipped with a multiplicative inverse operation made total by choosing 0 as its value at 0. Previously, inversive meadows were shortly called meadows. A divisive meadow is an inversive meadows with the multiplicative inverse operation replaced by a division operation. In the spirit of Peacock's arithmetical algebra, we introduce variants of inversive and divisive meadows without an additive identity element and an additive inverse operation. We give equational axiomatizations of several classes of such variants of inversive and divisive meadows as well as of several instances of them. △ Less

Submitted 2 November, 2010; v1 submitted 11 September, 2009; originally announced September 2009.

Comments: 14 pages; sections 4 and 5 permuted

Report number: PRG0909 MSC Class: 12E12; 12E30; 12L05

Inversive Meadows and Divisive Meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Inversive meadows are commutative rings with a multiplicative identity element and a total multiplicative inverse operation whose value at 0 is 0. Divisive meadows are inversive meadows with the multiplicative inverse operation replaced by a division operation. We give finite equational specifications of the class of all inversive meadows and the class of all divisive meadows. It depends on the an… ▽ More Inversive meadows are commutative rings with a multiplicative identity element and a total multiplicative inverse operation whose value at 0 is 0. Divisive meadows are inversive meadows with the multiplicative inverse operation replaced by a division operation. We give finite equational specifications of the class of all inversive meadows and the class of all divisive meadows. It depends on the angle from which they are viewed whether inversive meadows or divisive meadows must be considered more basic. We show that inversive and divisive meadows of rational numbers can be obtained as initial algebras of finite equational specifications. In the spirit of Peacock's arithmetical algebra, we study variants of inversive and divisive meadows without an additive identity element and/or an additive inverse operation. We propose simple constructions of variants of inversive and divisive meadows with a partial multiplicative inverse or division operation from inversive and divisive meadows. Divisive meadows are more basic if these variants are considered as well. We give a simple account of how mathematicians deal with 1 / 0, in which meadows and a customary convention among mathematicians play prominent parts, and we make plausible that a convincing account, starting from the popular computer science viewpoint that 1 / 0 is undefined, by means of some logic of partial functions is not attainable. △ Less

Submitted 2 November, 2010; v1 submitted 3 July, 2009; originally announced July 2009.

Comments: 18 pages; error corrected; 29 pages, combined with arXiv:0909.2088 [math.RA] and arXiv:0909.5271 [math.RA]

MSC Class: 12E12; 12L05; 12L12; 16E50; 68Q65

Journal ref: Journal of Applied Logic, 9(3):203--220, 2011

A process calculus with finitary comprehended terms

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: We introduce the notion of an ACP process algebra and the notion of a meadow enriched ACP process algebra. The former notion originates from the models of the axiom system ACP. The latter notion is a simple generalization of the former notion to processes in which data are involved, the mathematical structure of data being a meadow. Moreover, for all associative operators from the signature of mea… ▽ More We introduce the notion of an ACP process algebra and the notion of a meadow enriched ACP process algebra. The former notion originates from the models of the axiom system ACP. The latter notion is a simple generalization of the former notion to processes in which data are involved, the mathematical structure of data being a meadow. Moreover, for all associative operators from the signature of meadow enriched ACP process algebras that are not of an auxiliary nature, we introduce variable-binding operators as generalizations. These variable-binding operators, which give rise to comprehended terms, have the property that they can always be eliminated. Thus, we obtain a process calculus whose terms can be interpreted in all meadow enriched ACP process algebras. Use of the variable-binding operators can have a major impact on the size of terms. △ Less

Submitted 28 March, 2013; v1 submitted 17 March, 2009; originally announced March 2009.

Comments: 25 pages, combined with arXiv:0901.3012 [math.RA]; presentation improved, mistakes in Table 5 corrected

ACM Class: D.1.3; F.1.2; F.4.1

Journal ref: Theory of Computing Systems, 53(4):645--668, 2013

An Instruction Sequence Semigroup with Involutive Anti-Automorphisms

Authors: Jan A. Bergstra, Alban Ponse

Abstract: We introduce an algebra of instruction sequences by presenting a semigroup C in which programs can be represented without directional bias: in terms of the next instruction to be executed, C has both forward and backward instructions and a C-expression can be interpreted starting from any instruction. We provide equations for thread extraction, i.e., C's program semantics. Then we consider threa… ▽ More We introduce an algebra of instruction sequences by presenting a semigroup C in which programs can be represented without directional bias: in terms of the next instruction to be executed, C has both forward and backward instructions and a C-expression can be interpreted starting from any instruction. We provide equations for thread extraction, i.e., C's program semantics. Then we consider thread extraction compatible (anti-)homomorphisms and (anti-)automorphisms. Finally we discuss some expressiveness results. △ Less

Submitted 7 November, 2009; v1 submitted 7 March, 2009; originally announced March 2009.

Comments: 36 pages, 1 table

ACM Class: D.3.1; F.3.2; I.1.1

Journal ref: Scientific Annals of Computer Science, 19:57-92, 2009

Meadow enriched ACP process algebras

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: We introduce the notion of an ACP process algebra. The models of the axiom system ACP are the origin of this notion. ACP process algebras have to do with processes in which no data are involved. We also introduce the notion of a meadow enriched ACP process algebra, which is a simple generalization of the notion of an ACP process algebra to processes in which data are involved. In meadow enriched… ▽ More We introduce the notion of an ACP process algebra. The models of the axiom system ACP are the origin of this notion. ACP process algebras have to do with processes in which no data are involved. We also introduce the notion of a meadow enriched ACP process algebra, which is a simple generalization of the notion of an ACP process algebra to processes in which data are involved. In meadow enriched ACP process algebras, the mathematical structure for data is a meadow. △ Less

Submitted 4 February, 2009; v1 submitted 20 January, 2009; originally announced January 2009.

Comments: 8 pages; correction in Table 3

Report number: PRG0902

Meadows and the equational specification of division

Authors: J. A. Bergstra, Y. Hirshfeld, J. V. Tucker

Abstract: The rational, real and complex numbers with their standard operations, including division, are partial algebras specified by the axiomatic concept of a field. Since the class of fields cannot be defined by equations, the theory of equational specifications of data types cannot use field theory in applications to number systems based upon rational, real and complex numbers. We study a new axiomat… ▽ More The rational, real and complex numbers with their standard operations, including division, are partial algebras specified by the axiomatic concept of a field. Since the class of fields cannot be defined by equations, the theory of equational specifications of data types cannot use field theory in applications to number systems based upon 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 with a total inverse operator satisfying two equations which imply that the inverse of zero is zero. All fields and products of fields can be viewed as meadows. After reviewing alternate axioms for inverse, we start the development of a theory of meadows. We give a general representation theorem for meadows and find, as a corollary, that the conditional equational theory of meadows coincides with the conditional equational theory of zero totalized fields. We also prove representation results for meadows of finite characteristic. △ Less

Submitted 7 January, 2009; originally announced January 2009.

Skew Meadows

Authors: J. A. Bergstra, Y. Hirshfeld, J. V. Tucker

Abstract: A skew meadow is a non-commutative ring with an inverse operator satisfying two special equations and in which the inverse of zero is zero. All skew fields and products of skew fields can be viewed as skew meadows. Conversely, we give an embedding of non-trivial skew meadows into products of skew fields, from which a completeness result for the equational logic of skew fields is derived. The rel… ▽ More A skew meadow is a non-commutative ring with an inverse operator satisfying two special equations and in which the inverse of zero is zero. All skew fields and products of skew fields can be viewed as skew meadows. Conversely, we give an embedding of non-trivial skew meadows into products of skew fields, from which a completeness result for the equational logic of skew fields is derived. The relationship between regularity conditions on rings and skew meadows is investigated. △ Less

Submitted 7 January, 2009; originally announced January 2009.

Differential Meadows

Authors: Jan A. Bergstra, Alban Ponse

Abstract: A meadow is a zero totalised field (0^{-1}=0), and a cancellation meadow is a meadow without proper zero divisors. In this paper we consider differential meadows, i.e., meadows equipped with differentiation operators. We give an equational axiomatization of these operators and thus obtain a finite basis for differential cancellation meadows. Using the Zariski topology we prove the existence of a… ▽ More A meadow is a zero totalised field (0^{-1}=0), and a cancellation meadow is a meadow without proper zero divisors. In this paper we consider differential meadows, i.e., meadows equipped with differentiation operators. We give an equational axiomatization of these operators and thus obtain a finite basis for differential cancellation meadows. Using the Zariski topology we prove the existence of a differential cancellation meadow. △ Less

Submitted 21 April, 2008; originally announced April 2008.

Comments: 8 pages, 2 tables

MSC Class: AC; RA

Cancellation Meadows: a Generic Basis Theorem and Some Applications

Authors: Jan A. Bergstra, Inge Bethke, Alban Ponse

Abstract: Let Q_0 denote the rational numbers expanded to a "meadow", that is, after taking its zero-totalized form (0^{-1}=0) as the preferred interpretation. In this paper we consider "cancellation meadows", i.e., meadows without proper zero divisors, such as $Q_0$ and prove a generic completeness result. We apply this result to cancellation meadows expanded with differentiation operators, the sign functi… ▽ More Let Q_0 denote the rational numbers expanded to a "meadow", that is, after taking its zero-totalized form (0^{-1}=0) as the preferred interpretation. In this paper we consider "cancellation meadows", i.e., meadows without proper zero divisors, such as $Q_0$ and prove a generic completeness result. We apply this result to cancellation meadows expanded with differentiation operators, the sign function, and with floor, ceiling and a signed variant of the square root, respectively. We give an equational axiomatization of these operators and thus obtain a finite basis for various expanded cancellation meadows. △ Less

Submitted 22 May, 2013; v1 submitted 27 March, 2008; originally announced March 2008.

Comments: 24 pages, 6 tables; Inge Bethke is added as an extra author; new title (previous title: A Generic Basis Theorem for Cancellation Meadows)

MSC Class: AC; RA

Journal ref: The Computer Journal 56(1): 3-14, 2013