Search

Division by zero is a controversial theme. Why is division by zero a relevant issue and how can this issue be addressed from different perspectives? Fracterm is used as an abbreviation for fractional expression. Three types of occurrence of the division symbol in a fracterm are distinguished: prospective occurrence, retrospective occurrence, and formal occurrence. Mathematics mostly features retrospective occurrences of division, computer programming gives rise to prospective occurrences, and so does automated proof checking. The use of division in an axiom system may indicate the presence of formal occurrences of division symbols.

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.

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.

We imagine a minimal context where a programmer A serves as the provider of a program X for a user B. A survey is given of plausible promises and accusations in connection with the delivery and deployment of X. When X is used, various problems may arise. The focus of the paper is on the role of accusations which may plausibly arise in various scenarios. We discuss different accusation patterns that may occur outside informatics and see whether such patterns may appear in the context of programming as well.

The formal theory of division in arithmetical algebras reconstructs fractions as syntactic objects called fracterms. Basic to calculation, is the simplification of fracterms to fracterms with one division operator, a process called fracterm attening. We consider the equational axioms of a calculus for calculating with fracterms to determine what is necessary and sufficient for the fracterm calculus to allow fracterm flattening. For computation, arithmetical algebras require operators to be total for which there are several semantical methods. It is shown under what constraints up to isomorphism, the unique total and minimal enlargement of a field Q(\div) of rational numbers equipped with a partial division operator \div has fracterm attening.

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.

Transmathematica archive. Please cite as:J.A.D.W. Anderson & J.A. Bergstra, "Review of Suppes 1957 Proposals for Division by Zero", Transmathematica, ISSN 2632-9212, pp 1-10, 8 June 2021, https://doi.org/10.36285/tm.53

This paper concerns the relation between process algebra and Hoare logic. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning from the equational axioms of the process algebra.

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.

The number of instructions of an instruction sequence is taken for its logical SLOC, and is abbreviated with LLOC. A notion of quantitative expressiveness is based on LLOC and in the special case of operation over a family of single bit registers a collection of elementary properties is established. A dedicated notion of interface is developed and used for stating relevant properties of classes of instruction sequences.

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. Short-circuit evaluation is widely used in programming, with sequential conjunction and disjunction as primitive connectives. We study the question which logical laws axiomatize short-circuit evaluation under the following assumptions: compound statements are evaluated from left to right, each atom (propositional variable) evaluates to either true or false, and atomic evaluations can cause a side effect. The answer to this question depends on the kind of atomic side effects that can occur and leads to different "short-circuit logics". The basic case is FSCL (free short-circuit logic), which characterizes the setting in which each atomic evaluation can cause a side effect. We recall some main results and then relate FSCL to MSCL (memorizing short-circuit logic), where in the evaluation of a compound statement, the first evaluation result of each atom is memorized. MSCL can be seen as a sequential variant of propositional logic: atomic evaluations cannot cause a side effect and the sequential connectives are not commutative. Then we relate MSCL to SSCL (static short-circuit logic), the variant of propositional logic that prescribes short-circuit evaluation with commutative sequential connectives. We present evaluation trees as an intuitive semantics for short-circuit evaluation, and simple equational axiomatizations for the short-circuit logics mentioned that use negation and the sequential connectives only.

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

In process algebras such as ACP, parallel processes are considered to be interleaved in an arbitrary way. In the case of multi-threading as found in contemporary programming languages, parallel processes are actually interleaved according to some interleaving strategy. Interleaving strategies are also known as process-scheduling policies. In many systems, for instance hardware/software systems, we have to do with both parallel processes that may best be considered to be interleaved in an arbitrary way and parallel processes that may best be considered to be interleaved according to some interleaving strategy. Therefore, we extend ACP in this paper with the latter form of interleaving.

The Kolmogorov axioms for probability functions are placedin the context of signed meadows. A completeness theorem is stated andproven for the resulting equational theory of probability calculus. Elementary definitions of probability theory are restated in this framework.

Forensic science advocates the use of inference mechanisms which may be viewed as simple multi-agent protocols. An important protocol of this kind involves an agent FE (forensic expert) who communicates to a second agent TOF (trier of fact) first its value of a certain likelihood ratio with respect to its own belief state which is supposed to be captured by a probability function on FE's proposition space. Subsequently FE communicates its recently acquired confirmation that a certain evidence proposition is true. The inference part of this sort of reasoning, here referred to as likelihood ratio transfer mediated reasoning, involves TOF's revision of its own belief state, and in particular an evaluation of the resulting belief in the hypothesis proposition. Different realizations of likelihood ratio transfer mediated reasoning are distinguished: if the evidence hypothesis is included in the prior proposition space of TOF then a comparison is made between understanding the TOF side of a belief revision step as a composition of two successive steps of single likelihood Adams conditioning followed by a Bayes conditioning step, and as a single step of double likelihood Adams conditioning followed by Bayes conditioning; if, however the evidence hypothesis is initially outside the proposition space of TOF an application of proposition kinetics for the introduction of the evidence proposition precedes Bayesian conditioning, which is followed by Jeffrey conditioning on the hypothesis proposition.

An equational axiomatisation of probability functions for one-dimensional event spaces in the language of signed meadows is expanded with conditional values and configurations. Assuming the presence of a probability function, equational axioms are provided for expectation value, variance, covariance, and correlation squared, each for conditional values, and for expected utility of configurations. 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 higher dimensional setting.

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.

A datatype defining rewrite system (DDRS) is a ground-complete term rewriting system, intended to be used for the specification of datatypes. As a follow-up of an earlier paper we define two concise DDRSes for the ring of integers, each comprising only twelve rewrite rules, and prove their ground-completeness. Then we introduce DDRSes for a concise specification of natural number arithmetic and integer arithmetic in unary view, that is, arithmetic based on unary append (a form of tallying) or on successor function. Finally, we relate one of the DDRSes for the ring of integers to the above-mentioned DDRSes for natural and integer arithmetic in unary view.

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.

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.

Proposition algebra is based on Hoare's conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so-called free valuation congruence: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Free valuation congruence is axiomatized by the four basic equational axioms of proposition algebra that define the conditional connective. Valuation congruences that identify more conditional statements than free valuation congruence are repetition-proof, contractive, memorizing, and static valuation congruence. Each of these valuation congruences is characterized using a transformation on evaluation trees: two conditional statements are C-valuation congruent if, and only if, their C-transformed evaluation trees are equal. These transformations are simple and natural, and only for static valuation congruence a slightly more complex transformation is used. Also, each of these valuation congruences is axiomatized in proposition algebra. A spin-off of our approach is "basic form semantics for proposition algebra": for each valuation congruence C considered, two conditional statements are C-valuation congruent if, and only if, they have equal C-basic forms, where C-basic forms are obtained by a syntactic transformation of conditional statements, which is a form of normalization.

Common meadows are fields expanded with a total multiplicative inverse function. Division by zero produces an additional value denoted with “\({\textup{\textbf{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.

Each Boolean function can be computed by a single-pass instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Auxiliary Boolean registers are not necessary for this. In the current paper, we show that, in the case of the parity functions, shorter instruction sequences are possible with the use of an auxiliary Boolean register in the presence of instructions to complement the content of auxiliary Boolean registers. This result supports, in a setting where programs are instruction sequences acting on Boolean registers, a basic intuition behind the storage of auxiliary data, namely the intuition that this makes possible a reduction of the size of a program.

Multi-threading allows agents to pursue a heterogeneous collection of tasks in an orderly manner. The view of multi-threading that emerges from thread algebra is applied to the case where a single agent, who may be human, maintains a hierarchical multithread as an architecture of its own activities.

In the well-known construction of the field of fractions, 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 (that is, a commutative ring that has no nonzero nilpotent elements) and find that these constitute a "common meadow" (a field equipped with a multiplicative inverse and an additional element "a" that is the inverse of zero and propagates through all operations). We prove that fracpairs over Z constitute a homomorphic pre-image of the common meadow Qa, the field Q of rational numbers expanded with an a-totalized inverse. Moreover, we characterize the initial common meadow as an initial algebra of fracpairs. Next, we define canonical term algebras (and therewith normal forms) for fracpairs over the integers and some related structures that model the rational numbers, and we provide negative results concerning their associated term rewriting properties. Then we define "rational fracpairs" that constitute an initial algebra that is isomorphic to Qa. Finally, we express some negative conjectures concerning alternative specifications for these (concrete) datatypes.