A common meadow is an enrichment of a field with a partial division operation that is made total by assuming that division by zero takes the a default value, a special element adjoined to the field. To a common meadow of real numbers we add a binary logarithm log_2(-), which we also assume to be total with log_2(p) = for p ≤ 0. With these and other auxiliary operations, such as a sign function, we form algebras over which entropy and cross entropy can be defined for probability mass functions on a finite sample space by algebraic formulae that are simple terms built from the operations of the algebras and without case distinctions or conventions to avoid partiality. The discuss the advantages of algebras based on common meadows, whose theory is established, and alternate methods to define entropy and other information measures completely for all arguments using single terms.

We introduce approximations to arithmetical data types called arithmetics by proxy or proxy arithmetics. Focusing on the common meadow of rational numbers, we examine the effect of imposing bounds on the numbers and finiteness on algebras that approximate the rationals. Starting with an established set of equations for common meadows, we explore sets of equational axioms for these approximating algebras. Then we give a new general algebraic construction that may serve as a way of making proxies for arbitrary data types. We apply the construction to the arithmetical case. Finally, we return to the sets of equations using notions of equality that are different from standard first order equality.

Both two-valued and three-valued conditional logic (CL), defined by Guzm\'an and Squier (1990) and based on McCarthy's non-commutative connectives, axiomatise a short-circuit logic (SCL) that defines more identities than MSCL (Memorising SCL), which also has a two- and a three-valued variant. This follows from the fact that the definable connective that prescribes full left-sequential conjunction is commutative in CL. We show that in CL, the full left-sequential connectives and negation define Bochvar's three-valued strict logic. In two-valued CL, the full left-sequential connectives and negation define a commutative logic that is weaker than propositional logic because the absorption laws do not hold. Next, we show that the original, equational axiomatisation of CL is not independent and give several alternative, independent axiomatisations.

Partial algebras and datatypes are discussed with the use of signatures that allow partial functions, and a three-valued short-circuit (sequential) first order logic with a Tarski semantics. The propositional part of this logic is also known as McCarthy calculus and has been studied extensively. Axioms for the fracterm calculus of partial meadows are given. The case is made that in this way a rather natural formalisation of fields with division operator is obtained. It is noticed that the logic thus obtained cannot express that division by zero must be undefined. An interpretation of the three-valued sequential logic into -enlargements of partial algebras is given, for which it is concluded that the consequence relation of the former logic is semi-computable, and that the -enlargement of a partial meadow is a common meadow.

We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value \(\bot\) whose main purpose is to always return a value for division. To rings and fields, we add a division operator \(x/y\) and study a class of algebras called common meadows wherein \(x/0=\bot\) . The set of equations true in all common meadows is named the equational theory of common meadows . We give a finite equational axiomatisation of the equational theory of common meadows and prove that it is complete and that the equational theory is decidable.

Classic formulae for entropy and cross-entropy contain operations x0 and log2x that are not defined on all inputs. This can lead to calculations with problematic subexpressions such as 0log20 and uncertainties in large scale calculations; partiality also introduces complications in logical analysis. Instead of adding conventions or splitting formulae into cases, we create a new algebra of real numbers with two symbols ±∞ for signed infinite values and a symbol named ⊥ for the undefined. In this resulting arithmetic, entropy, cross-entropy, Kullback–Leibler divergence, and Shannon divergence can be expressed without concerning any further conventions. The algebra may form a basis for probability theory more generally.

Arithmetical texts involving division are governed by conventions that avoid the risk of problems to do with division by zero (DbZ). A model for elementary arithmetic texts is given, and with the help of many examples and counter examples a partial description of what may be called traditional conventions on DbZ is explored. We introduce the informal notions of legal and illegal texts to analyse these conventions. First, we show that the legality of a text is algorithmically undecidable. As a consequence, we know that there is no simple sound and complete set of guidelines to determine unambiguously how DbZ is to be avoided. We argue that these observations call for further explorations of mathematical conventions. We propose a method using logics to progress the analysis of legality versus illegality: arithmetical texts in a model can be transformed into logical formulae over special total algebras that are able to approximate partiality but in a total world. The algebras we use are called common meadows. Our dive into informal mathematical practice using formal methods opens up questions about DbZ which we address in conclusion.

We examine the consequences of having a total division operation $\frac {x}{y}$ on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the other defined directly as a general operation; each are made total by setting $1/0$ equal to an error value $\bot $ , which is added to the ring. Such totalised divisions we call common divisions. In a field the two forms are equivalent and we have a finite equational axiomatisation E that is complete for the equational theory of fields equipped with common division, which are called common meadows. These equational axioms E turn out to be true of commutative rings with common division but only when defined via inverses. We explore these axioms E and their role in seeking a completeness theorem for the conditional equational theory of common meadows. We prove they are complete for the conditional equational theory of commutative rings with inverse based common division. By adding a new proof rule, we can prove a completeness theorem for the conditional equational theory of common meadows. Although, the equational axioms E fail with common division defined directly, we observe that the direct division does satisfy the equations in E under a new congruence for partial terms called eager equality.

A common meadow is an enrichment of a field with a division operator and an error value to make division total. A signed common meadow enriches a common meadow with a sign function that can be equationally axiomatised; the sign function can simulate an ordering on the underlying field but is not limited to orderings. In particular, of mathematical interest are the weakly signed common meadows. The prime example of a weakly signed common meadow is an expansion of a common meadow of complex numbers with a weak sign function. We show that all common meadows may be enlarged to a weakly signed common meadow. A special case is the 4-signed common meadows, which are precisely the enlargements of ordered fields. To illustrate the equational calculus for signed common meadows, we use it as a foundation for building a probability calculus and derive some classical formulae.

Previously, in [Bergstra and Tucker 2023], we provided a systematic description of elementary arithmetic concerning addition, multiplication, subtraction and division as it is practiced. Called the naive fracterm calculus, it captured a consensus on what ideas and options were widely accepted, rejected or varied according to taste. We contrasted this state of the practical art with a plurality of its formal algebraic and logical axiomatisations, some of which were motivated by computer arithmetic. We identified a significant gap between the wide embrace of the naive fracterm calculus and the narrow precisely defined formalisations. In this paper, we introduce a new intermediate and informal axiomatisation of elementary arithmetic to bridge that gap; it is called the synthetic fracterm calculus. Compared with naive fracterm calculus, the synthetic fracterm calculus is more systematic, resolves several ambiguities and prepares for reasoning underpinned by logic; indeed, it admits direct formalisations, which the naive fracterm calculus does not. The methods of these papers may have wider application, wherever formalisations are needed to analyse and standardise practices.

We introduce the concept of arithmetic by proxy and study its role in arithmetical computation. A proxarithmetic is a model of a classical arithmetic that features some (though not necessarily all) of the algebraic properties that separate computer arithmetics from classical arithmetics. Typical features of proxarithmtics are: partial operations, finiteness, overflows, underflows, degrees of precision, approximation, etc. We focus on the case of the classical rational numbers Q and examine nine types of proxarithmetics for Q. We compare computation by imperative programs on Q and on, and between, the proxarithmetics; and we classify several semantic consequences of computing by proxy. Our analysis leads to a new tenth proxarithmetic with good invariance properties for Q.

Eager equality is a novel semantics for equality in the presence of partial operations. We consider term rewriting for eager equality for arithmetic in which division is a partial operator. We use common meadows which are essentially fields that contain an absorptive element $\bot $. The idea is that term rewriting is supposed to be semantics preserving for non-$\bot $ terms only. We show soundness and adequacy results for eager term rewriting w.r.t. the class of all common meadows. However, we show that an eager term rewrite system which is complete for common meadows of rational numbers is not easy to obtain, if it exists at all.

Eager equality for algebraic expressions over partial algebras distinguishes or separates terms only if both have defined values and they are different. We consider arithmetical algebras with division as a partial operator, called meadows, and focus on algebras of rational numbers. To study eager equality, we use common meadows, which are totalisations of partial meadows by means of absorptive elements. An axiomatisation of common meadows is the basis of an axiomatisation of eager equality as a predicate on a common meadow. Applied to the rational numbers, we prove completeness and decidability of the equational theory of eager equality. To situate eager equality theoretically, we consider two other partial equalities of increasing strictness: Kleene equality, which is equivalent to the native equality of common meadows, and one we call cautious equality. Our methods of analysis for eager equality are quite general, and so we apply them to these two other partial equalities; and, in addition to common meadows, we use three other kinds of algebra designed to totalise division. In summary, we are able to compare 13 forms of equality for the partial meadow of rational numbers. We focus on the decidability of the equational theories of these equalities. We show that for the four total algebras, eager and cautious equality are decidable. We also show that for others the Diophantine Problem over the rationals is one-one computably reducible to their equational theories. The Diophantine Problem for rationals is a longstanding open problem. Thus, eager equality has substantially less complex semantics.

An outline is provided of a new perspective on elementary arithmetic, based on addition, multiplication, subtraction and division, which is informal and unique and may be considered naive when contrasted with a plurality of algebraic and logical, axiomatic formalisations of elementary arithmetic.

We will examine totalising a partial operation in a general algebra by using an absorbtive element ⊥, such as an error flag. We then focus on the simplest example of a partial operation, namely subtraction on the natural numbers: n − m is undefined whenever n < m. We examine the use of ⊥ in algebraic structures for the natural numbers, especially semigroups and semirings. We axiomatise this totalisation process and introduce the algebraic concept of a team, being an additive cancellative semigroup with totalised subtraction. Also, with the natural numbers in mind, we introduce the property of being generated by an iterative function, which we call a splinter. We prove a number of theorems about the algebraic specification of datatypes of natural numbers. © J.A. Bergstra, J.V. Tucker Licence CC BY-SA 4.0

A new definition of algorithms is given, where algorithms are understood as cognitive 'entities', the definition of which is done in tandem with so-called algorhymes, which are entities serving as documentation of algorithms. Based on this definition the notions of fault and defect are reconsidered in relation to instruction sequences, programs and algorithms. Programs as well as algorithms are considered capable of containing moral defects, the notion of a moral defect is developed in some detail. The notion of a moral fault is considered implausible.

Upon adding division to the operations of a field we obtain a meadow. It is conventional to view division in a field as a partial function, which complicates considerably its algebra and logic. But partiality is one out of a plurality of possible design decisions regarding division. Upon adding a partial division function ÷ to a field Q of rational numbers we obtain a partial meadow Q(÷) of rational numbers that qualifies as a data type. Partial data types bring problems for specifying and programming that have led to complicated algebraic and logical theories – unlike total data types. We discuss four different ways of providing an algebraic specification of this important arithmetical partial data type Q(÷) via the algebraic specification of a closely related total data type. We argue that the specification method that uses a common meadow of rational numbers as the total algebra is the most attractive and useful among these four options. We then analyse the problem of equality between expressions in partial data types by examining seven notions of equality that arise from our methods alone. Finally, based on the laws of common meadows, we present an equational calculus for working with fracterms that is of general interest outside programming theory.

Thread algebra is a domain-specific process algebra which may be used for semantic work on sequential systems, including systems based on deterministically scheduled multi-threading. Thread algebra is used in this capacity with the forecasting phenomenon for programs and machines as a domain of interest. Several new informal notions are proposed: prospecting services, foresight patterns for systems, and lookahead conditions as a mechanism for the specification of services. Some new prospecting services are proposed which facilitate the realisation of certain foresight patterns. Several negative results about the non-realisability of certain foresight patterns are provided.

We introduce and investigate an arithmetical data type designed for computation with rational numbers. Called the symmetric transrationals, this data type comes about as a more algebraically symmetric modification of the arithmetical data type of transrational numbers [9], which was inspired by the transreals of Anderson et.al. [1]. We also define a bounded version of the symmetric transrationals thereby modelling some further key semantic properties of floating point arithmetic. We prove that the bounded symmetric transrationals constitute a data type. Next, we consider the equational theory and prove that deciding the validity of equations over the symmetric transrationals is 1-1 algorithmically equivalent with deciding unsolvability of Diophantine equations over the rational numbers, which is a longstanding open problem. The algorithmic degree of the bounded case remains open.

Using the conceptual analysis of instruction sequence faults, failures, and defects as developed by the author in [10] and [12], a survey of testing is developed as an extension of a theory of instruction sequences. An attempt is made to develop a consistent terminology regarding instruction sequence testing while taking into account the literature on software testing at large.