Jan A Bergstra
email: j.a.bergstra@uva.nl

Transrational Numbers as an Abstract Data Type

In an arithmetical structure one can make division a total function by defining 1/0 to be an element of the structure, or by adding a new element, such as an error element also denoted with a new constant symbol, an unsigned infinity or one or both signed infinities, one positive and one negative. We define an enlargement of a field to a transfield, in which division is totalised by setting 1/0 equal to the positive infinite value and -1/0 equal to its opposite, and which also contains an error element to help control their effects. We construct the transrational numbers as a transfield of the field of rational numbers and consider it as an abstract data type. We give it an equational specification under initial algebra semantics.

Introduction

Arithmetical structures are the oldest and most important data types. The rational numbers are particularly fundamental in practical applications: we measure the world with rational numbers and today's computers calculate only with rational numbers. However, as a data type completely central to computer science, the rationals are only slowly being analysed and understood as an abstract data type. The theory of algebraic specifications for abstract data types, with its wealth of concepts, results and tools, have only lately been applied to the rationals. Classical mathematics has viewed the rationals as a field, i.e., a commutative ring in which each non-zero element has a unique multiplicative inverse; this leads to inverse x -1 not being a total operator on 0. The need c Jan A. [START_REF] Bergstra | The wheel of rational numbers as an abstract data type[END_REF] Licence CC BY-SA 4.0 to rule out zero means that a field cannot be axiomatised by total operations satisfying equations or conditional equations, the core specification methods for the theory.

In arithmetical structures, the most important partial operator is 1/x when x = 0. Among the approaches to making division or inverse total are structures in which:

1. 1/0 behaves as one of the elements in the structure, e.g., 0 or 1; 2. 1/0 behaves as an error element ⊥ additional to the structure; 3. 1/0 behaves as an infinite element ∞, additional to the structure; 4. 1/0 and -1/0 behaves as infinite elements ∞ and -∞, respectively, and additional to the structure.

There are plenty of examples of these approaches in theory and practice, often to solve a technical issue in an ad hoc way. All four approaches deliver workable and interesting ways of removing partiality. In the case of (ii), basic properties such as the absorption laws ⊥ + x =⊥, ⊥ . x =⊥ are expected to hold. In the case of (iii) and (iv) basic properties such as

∞ + x = ∞, ∞.x = ∞, ∞ + ∞ = ∞, ∞.∞ = ∞, ∞.(-∞) = -∞
are expected and begin to shape intuitions about the semantics. However, adding elements to structures commonly cause complications, because the new elements must operate sensibly with all the algebraic constants and operations of the structure. For example, in the case of adding infinity, we can easily find possible identities that are unattractive and against some arithmetic intuitions, such as:

0.∞ = ∞ or ∞ -∞ = 0.
Thus a next step, in the case of infinity ∞, is to also add an error element ⊥ so that some unwanted or suspect results can be controlled. For instance: 0.∞ =⊥, and, indeed, ∞ -∞ =⊥.

If 1/0 is defined then the rationals can be axiomatised by equations: an initial algebra specification of the rationals was accomplished in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF] by taking approach [START_REF] Anderson | Perspex Machine VIII: axioms of transreal arithmetic[END_REF]. Furthermore, approach (1), especially 1/0 = 0, was examined in some generality through a theory of meadows, which are an axiomatically defined class of arithmetical algebras first studied in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF][START_REF] Bergstra | Meadows and the equational specification of division[END_REF]. Earlier, meadows, with a focus on first order axiomatisations thereof, had been studied in significant detail and depth under the name of pseudofields in [START_REF] Ono | Equational theories and universal theories of fields[END_REF].

Later, meadows with an error element, approach (2), were extensively developed in [START_REF] Bergstra | Division by zero in common meadows[END_REF]; and the infinity element, approaches (3) and (4), were discussed in [START_REF] Bergstra | Division by zero: A survey of options[END_REF].

The idea of adding infinity and an error element is not new -such elements are mentioned in informal specifications of floating point arithmetic [START_REF] Patterson | Computer Organisation and Design: The Hardware/Software Interface[END_REF]. A theoretical analysis motivated by theorem proving is based upon algebraic structures called wheels, which are an axiomatically defined class of algebras first studied in [START_REF] Setzer | [END_REF][START_REF] Carlstrom | Wheels: on division by zero[END_REF]. Wheels contain the elements positive infinity and error. Along with the key ideas of a wheel -namely, 1 0 = ∞ and 1 ∞ = 0 -come the subtle controlling properties that 0.∞ =⊥ and ∞ + ∞ =⊥.

The viability or fitness for purpose of any method of totalising division depends upon the axioms for the structures and, subsequently, on their application to a computational problem. Both axiomatisations of meadows and wheels start with familiar axioms for commutative ring-like structures to which axioms for inverse -1 are added. Central to both meadows, wheels and other approaches to totalisation is the field of rational numbers and the problem of totalising division; see [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF] and for several other options for division by zero [START_REF] Bergstra | Division by zero: A survey of options[END_REF].

In the case of meadows, the development uses the theory of algebraic specifications of abstract data types, in which a central concept is axiomatisation by a finite set E of equations over a signature Σ, whose initial algebra defines the data type up to isomorphism. Thus, in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF], a finite equational specification is given, of the rationals up to isomorphism with 1/0 = 0, which in other words defines the abstract data type Q 0 of the meadow of rational numbers. Interestingly, an equational specification for the rational numbers was open until [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF].

In this paper we examine the basic structure of rational number arithmetic augmented by the infinite elements ∞ and -∞ and ⊥. We call this structure the algebra of transrationals, which we adopt from a semantic model called transreal arithmetic in [START_REF] Anderson | Perspex Machine VIII: axioms of transreal arithmetic[END_REF][START_REF] Reis | Construction of the transreal numbers and algebraic transfields[END_REF]. The transrationals are a minimal subalgebra of the transreals.

We will extend and adapt the techniques from meadows [START_REF] Bergstra | Meadows and the equational specification of division[END_REF] to give an equational specification for the transfield Q tr of rational numbers as abstract data type: we give a set of equations E tr over the signature Σ tr such that

I(Σ tr , E tr ) ≡ Q tr .
The structure of the paper is as follows. In section 2 we recall some basic semantics of floating point arithmetic, which provides some additional motivation for our interest. In section 3 we list some basic concepts and principles of our general approach, including the methodology of abstract data type theory and the focus of our interest, namely arithmetical structures. In section 4 we introduce a construction of the transfield of an ordered field and apply it to a construction of the field of rationals. in section 5 we give it its initial algebra specification. Section 6 makes some concluding remarks on equational axiomatisations, floating point and other approaches.

We assume that the reader is familiar with the basic algebraic concepts used to model data types: signature, algebra, expansion, reduct, congruence, term, homomorphism, equational theory, first order theory, etc. These basics can be found in several inroductions to algebraic methods and abstract data type theory [START_REF] Meinke | Universal algebra[END_REF][START_REF] Wechler | Universal Algebra for Computer Scientists[END_REF][START_REF] Ehrig | Fundamentals of Algebraic Specification 1: Equations und Initial Semantics[END_REF][START_REF] Loeckx | Specification of abstract data types[END_REF]. We have chosen to keep our algebraic techniques very simple to focus attention on a topic for theoretical investigation, namely arithmetic data type theory.

Transrationals and floating point arithmetic

As is evident from the Introduction, our point of departure is the analysis of arithmetical structures of computational interest using the theory of abstract data types. The transrationals are a particularly interesting arithmetical structure not least for the light they shine on computer arithmetics such as floating point arithmetic. Many reasons for developing the transreals, and implicitly the transrationals, have been elaborated in the works of James Anderson and his co-workers including [START_REF] Anderson | Perspex Machine VIII: axioms of transreal arithmetic[END_REF][START_REF] Reis | Construction of the transreal numbers and algebraic transfields[END_REF]. Here we will focus on their relevance to floating point arithmetic.

Viewed as a data type, floating point arithmetic is an arithmetical data type for a finite subset of the rational numbers. Its actual design strives for an approximation of rational number arithmetic that is "best possible" according to certain working criteria. The design is a finite data type that can be implemented in computer hardware and involves complications such as the following:

1. Every number must be represented in a bit pattern of fixed length (e.g., 2 n bits).

2. Except for zero 0, which is represented with a dummy exponent, each finite number is coded by a pair containing a decimal number 1 ≤ d ≤ 10 of fixed length l and a power e ∈ [-k, k] of 10. A finite set of rationals can be represented in this way.

3. Arithmetical operations on floating point numbers cannot always be carried out exactly and rounding will occur.

4. Partial arithmetical operations are avoided by using the special values ∞ (infinity) and -∞ (minus infinity) to represent 1 0 and -1 0 , respectively, and an error value to represent 0 0 . 5. Partial operations also use error values that enable them to terminate on certain data, e.g, a "not a number" value, quiet NaN or qNaN ).

6. Partial operations may lead to exceptions and interrupts that are modelled by special error values signalling, e.g, a "not a number " value, signalling NaN or sNaN).

7. Due to the presence of error values there is no total ordering of the domain of floating point arithmetic.

8. In some models of floating point arithmetic 1 ∞ = 0 and 1 -∞ = -0 with -0 different from 0.

The arithmetical data type of transrationals adapts the data type of rational numbers by including ∞ and -∞ and a single quiet NaN, which is here called ⊥. We notice that Anderson denotes this object by Φ and calls it nullity, thereby emphasising that its role may be more significant than simply representing an error. It sets 1 ∞ = 1 -∞ = 0. Seen from the point of view of the rationals, the transrationals are a semantic model of some key features to be found in floating point arithmetic. They are idealisations, of course, that 'correct' issues with floating point: the transrationals enjoy associativity, are infinite and dense in the reals, etc.

Preliminaries on ADTs

The Approach of ADTs

The theory of abstract data types is based upon the following principle:

Principle. In programming, data is characterised by the operations and tests we can use on the data. All the data can be constructed and accessed by applying the operations to given constants. An interface to the data type is a syntactic declaration of these constant, operator and test names. What is known to the programmer about the implementation of the data type is only a set of properties of the constants, operators and tests. The interface and set of properties is called a specification of an abstract data type.

These ideas about programming are faithfully modelled by the algebraic and logical theories of general algebras and relational structures. In particular, the interface is modelled by a signature Σ and the properties modelled by an axiomatic theory T .

Principle. An abstract data type is an isomorphism class of algebras of common signature. Each algebra is a possible representation or construction or implementation of the abstract data type. The algebras for which all the data can be constructed from the constants by the operations of the abstract data type are the minimal algebras.

Thus, to specify an abstract data type is to specify an isomorphism class of algebras. In the case of the field of rational numbers, the standard notation Q will stand for the the isomorphism type and Q will stand for a particular representative or construction or implementation of the rational isomorphism type.

In general, conditions are added to this idea of an abstract data type, of which finite, computable, semicomputable abstract data types are common; notice such properties must be isomorphism invariants of algebras. Computable algebras have important roles in modelling data [START_REF] Stoltenberg-Hansen | Effective algebras[END_REF], and especially in classical field theory [START_REF] Stoltenberg-Hansen | Computable rings and fields[END_REF]. Of course, the rationals are a computable data type.

Let us expand on the ideas introduced above. The interface is a signature Σ and, typically, the properties form a set T of first order axioms about the constants, operations and tests in Σ. A Σalgebra is Σ-minimal if all the elements of A can be constructed by applying the operations to the constants of A. The pair (Σ, T ) is an axiomatic specification and Alg(Σ, T ) is the class of all Σ-structures that satisfy the axioms of T . Of particular importance is the case when the axiomatisations consist of a set E of equations only. Such an equational specification (Σ, E) has an initial algebra I(Σ, E) in the class Alg(Σ, E) that is unique up to isomorphism. The initial algebra has an important representative structure. Let T (Σ) be the set of all closed terms over the signature Σ. Define a congruence on T (Σ) for any t 1 , t 2 ∈ T (Σ),

t 1 ≡ t 2 ⇐⇒ E t 1 = t 2
Then we have the factor algebra

I(Σ, E) ∼ = T (Σ)/ ≡.

Thus the

Specification Problem.

Given an algebra A representing an implementation of an abstract data type, can we find an equational specification (Σ, E)

such that I(Σ, E) ∼ = T (Σ)/ ∼ = A.
Algebras can be extended by adding new elements to their domain; and they can be expanded by adding new constants and operations to their signature. Often both extensions and expansions are performed, especially to add auxiliary operators in order to find or simplify equations in specifications. These actions of extension and expansion and their combination are what we call enlargements of the algebra. Obviously, the transrationals are an enlargement of the rationals.

The general specification problem for computable, semicomputable and cosemicomputable abstract data types has been studied in depth [START_REF] Bergstra | The completeness of the algebraic specification methods for computable data types[END_REF][START_REF] Bergstra | Algebraic specifications of computable and semicomputable data types[END_REF][START_REF] Bergstra | Initial and final algebra semantics for data type specifications: Two characterization theorems[END_REF]. In general, auxiliary operators and even auxiliary sorts may be needed. For example, small equational specifications exist for all computable data types, provided some auxiliary operations may appear in the specification; indeed, general theory shows that the rational number data types studied here are computable and, therefore, can all be specified with 6 auxiliary functions and 4 equations only [START_REF] Bergstra | The completeness of the algebraic specification methods for computable data types[END_REF]! However, these general theoretical results use advanced methods from computability theory and do not yield recognisable and useable axiomatisations.

Here the equational specifications are close to the algebra and do not use auxiliary operators.

Arithmetic structures

Consider the following signature Σ tr for transfields which simply adds two characteristic constants, ∞ for infinity and ⊥, to the signature Σ m for meadows:

signature Σ tr sorts num constants 0 :→ num 1 :→ num ∞ :→ num ⊥:→ num operations + : num × num → num . : num × num → num -: num → num -1 : num → num / : num × num → num end
We have not added -∞ for negative infinity as we can use the term -(∞). Note that the signature for meadows is richer than those commonly used for working with fields and skew structures; often inverse -1 is not an explicit operation having an axiomatisation, and binary divison / seems to be rarely used. (In some cases of interest to us it is convenient to add other binary operations such as subtraction -: v × v → v.) Definition 3.1. Σ is an arithmetic signature if it extends the meadow signature, i.e., Σ m ⊂ Σ.

Clearly, a transfield signature is an arithmetic signature in this sense. [START_REF] Bergstra | Division by zero: A survey of options[END_REF] The transrationals

The transfield of a field

A field F is a commutative ring with 1 = 0 and in which, for all x ∈ F , if x = 0 then there exists a unique y ∈ F such that x.y = 1. Let (F, ≤) be an ordered field. We propose to enlarge F by extending with new elements e, i p and i n representing error, positive infinity and negative infinity, respectively; and expanding with the inverse operation -1 .

We also expand the signature with constant names ⊥, ∞ for e, i p -note we will not need a name for i n . This new structure F tr we call the transfield of F . This is a special case of a more general concept of transfield in [START_REF] Reis | Construction of the transreal numbers and algebraic transfields[END_REF].

The new elements and operations are defined on the domain F tr = F ∪ {e, i p , i n } as follows. First, we make the extension of the ring operations:

Additive inverse -e = e -i p = i n -i n = i p Addition e + x = e
for all x ∈ F tr x + e = e for all x ∈ F tr

i p + x = i p for all x ∈ F i n + x = i n for all x ∈ F i p + i p = i p i p + i n = e i n + i p = e i n + i n = i n Multiplication e.
x = e for all x ∈ F tr

x.e = e for all x ∈ F tr i p .0 = e 0.i p = e i n .0 = e 0.i n = e i p .x = i p for all x ∈ F, x > 0

x.i p = i p for all x ∈ F, x > 0 i p .x = i n for all x ∈ F, x < 0 x.i p = i n for all x ∈ F, x < 0 i n .x = i p for all x ∈ F, x < 0 x.i n = i p for all x ∈ F, x < 0 i p .i p = i p i p .i n = i n i n .i p = i n i n .i n = i p Inverse e -1 = e i -1 p = 0 i -1 n = 0 0 -1 = i p x -1 = (unique y)[x.y = 1] for all x ∈ F, x = 0
Note that the ordering on F is essential for the construction of F tr but is not a relation in the signature of either F or F tr .

A concrete representation of the rationals

We start with a ring Q of rational numbers with unit. This is an algebra that is not minimal.

We begin the construction of the rationals from the integers Z as follows: let SF P = {(n, m) : n, m ∈ Z, m > 0, and gcd(n, m) = 1}. SF P stands for simplified fracpairs. For further information on fracpairs see [START_REF] Bergstra | Fracpairs and fractions over a reduced commutative ring[END_REF]. Note we seek to avoid equivalence classes in this construction.

The additive identity is uniquely defined by (0, 1); note that elements such as (0, 2) are not in SF P . The multiplicative unit is [START_REF] Anderson | Perspex Machine VIII: axioms of transreal arithmetic[END_REF][START_REF] Anderson | Perspex Machine VIII: axioms of transreal arithmetic[END_REF].

We define the operations in stages starting with addition:

A concrete representation of the transrationals

To build an algebra Q tr of transrational numbers we need to add elements that behave like ± infinity and error. We apply to Q the construction of the transfield of an ordered field given in section 4.1. However, instead of extending Q by adding the elements e, i p and i n of the general construction to Q we add the following. The element (1, 0) will represent infinity ∞, the element (-1, 0) will represent the opposite of infinity -∞ and the element (0, 0) will represent error ⊥.

The elements (1, 0), (-1, 0) and (0, 0) are not in the set SF P , which requires the second coordinate m > 0, and so we define SF P tr = SF P ∪ {(1, 0), (-1, 0), (0, 0)}.

Thus the structure Q is extended to the algebra Q[(1, 1), (0, 0)] = (SF P tr | (0, 1), (1, 1), +, -, .)

The new elements are not named constants.

At this point we expand the algebra Q[(1, 1), (0, 0)] with inverse operation -1 again defined by the construction in section 4.1:

This extended structure Q tr = (SF P tr | (0, 1), (1, 1), (1, 0), (0, 0), +, -, ., -1 ) is an algebra of transrational numbers.

Lemma 4.1. The algebra Q tr is a Σ tr -minimal algebra.

Definition 4.1. The abstract data type Q tr of the algebra of transrational numbers is the isomorphism class of the Σ tr -minimal algebra Q tr .

5 Initial algebra specification of transrationals

Axioms

The complete set of equational axioms is given in Table 1.

Notice that axioms 33 and 34 introduce two auxiliary operators (division and square) to make other axioms and arguments more familiar and easier to read; they can be removed.

To get the feel of these axioms we prove carefully some identities that will be needed in proofs later on. As with all axiomatisations of algebraic structures, the lemmas are needed to build up a stock of basic properties, some of which could have been chosen as axioms. We start with the following observation:

x + y = y + x (1) (x + y) + z = x + (y + z) (2)
x + 0 = x

x + (-x) = 0.x (4)

x.y = y.x

x.(y.z) = (x.y).z

x.1 = x (7)

(x.y) -1 + 0.(x -1 + y -1 ) = x -1 .y -1 + 0.(x -1 + y -1 ) (8) (x -1 ) -1 + (0.x) = x + (0.x) (9) (-x) -1 + (0.x -1 ) = -(x -1 ) + (0.x -1 ) (10)
(x + y).z + (0.z) = (x.z + y.z) + (0.z) [START_REF] Bergstra | Probability functions in the context of signed involutive meadows (extended abstract)[END_REF] 0.0 = 0 (12)

0 -1 = ∞ (13)
∞ -1 = 0 (14) (-∞) -1 = 0 (15) ∞ + 1 = ∞ (16) ∞ -1 = ∞ (17) ∞.∞ = ∞ (18) ∞ + ∞ = ∞ (19)
∞ + (-∞) =⊥ ( 20)

-(x + y) = (-x) + (-y) (21)
(-x).y = -(x.y)

-(-x) = x (23) 0.∞ =⊥ (22)
-⊥ =⊥ (25)

⊥ -1 =⊥ (26) ⊥ + ⊥ =⊥ (27) 1 + ⊥ =⊥ (28) ∞ + ⊥ =⊥ (29) (x.y) + ⊥ = x + (y+ ⊥) (30)
x

-1 + ⊥ = x+ ⊥ (31) (-x) + ⊥ = x+ ⊥ (32) x y = x.y -1 (33)
x 2 = x.x (34)

1 + 0.((x + y) + (z + u)) = ((x 2 + y 2 ) + (z 2 + u 2 )) + 1 ((x 2 + y 2 ) + (z 2 + u 2 )) + 1 (35) ∞ + 0.((x + y) + (z + u)) = ((x 2 + y 2 ) + (z 2 + u 2 )) + 1 0 + 0.((x + y) + (z + u)) (36)
Table 1: E tr : An initial algebra specification of the abstract datatype of transrationals In further proofs we will use associativity and commutativity without reference to the respective axioms. The lemma prompts to note that the absorption law x + ⊥=⊥ is not provable from the equations of E tr . This is because all our equations in E tr have exactly the same variables on both sides of the equality sign, which is a property preserved by equational deduction. (A rationale for choosing this type of equation is given in section 6.2.) Next, recall the properties of numerals. Let n = 1 + 1 + . . . + 1 (n-times). Then the following is easy to check: Proof. Applying Lagrange's Theorem to m -1, let m = p 2 + q 2 + r 2 + s 2 + 1.

Then: denominator evaluates to (1,0) and their division to (0,0), as previously. On the LHS the sum of the variable is immediately (0,0) and so evaluates to (0,0) and LHS = RHS. With these illustrative cases we conclude the argument for the lemma.

m m = p 2 + q 2 + r 2 + s 2 + 1 p 2 + q 2 + r 2 + s 2 + 1 = 1 + 0.(p + q + r +
T (Σ tr , E tr ) is the initial algebra of the class of models of (Σ tr , E tr ). By the lemma Q tr is such a model and so by intitiality, there exists a unique surjective homomorphism φ : T (Σ tr , E tr ) -→ Q tr . We have to show that φ is an isomorphism. We do this by proving by induction the following lemma: Lemma 5.15. Every term t ∈ T (Σ tr ) reduces to an element t 0 of the transversal Tr, i.e., (Σ tr , E tr ) t = t 0 .

We deal with the constants in the base case and the operator symbols in the induction step. There are several case distinctions and the argument uses the 36 equations in various subtle ways.

Basis Case: The Constants. Clearly, the transversal contains the constants ⊥, ∞. We will show that the constant 0 is 0.1 -1 using axioms of x.1 = x (axiom 7) and associativity:

0 = 0.1 = 0.(1.1 -1 ) = (0.1).1 -1 = 0.1 -1 .
Last we show the constant 1 is 1.1 -1 using the four squares axiom:

1 1 = 0 2 + 0 2 + 0 2 + 0 2 + 1 0 2 + 0 2 + 0 2 + 0 2 + 1 = 1 + 0.(0 + 0 + 0 + 0) = 1.
Both are in the transversal.

Induction

Step. There are four operators -, -1 , +, . to consider.

Additive inverse. Consider the leading operator symbol -and term t = -s. By induction, the subterm s reduces to one of four cases: s = ∞, s = -∞, s =⊥ and s = n.m -1 in the transversal Tr. From the axioms, the first two cases of -s are immediate as -∞, -(-∞) = ∞ (axiom 23) and -⊥=⊥ (axiom 25) are in the transversal. Finally, Suppose t = -(n.m -1 ). Then, by axiom 22, t = (-n.m -1 ), which is in the transversal.

Multiplicative inverse. Consider the leading operator symbol -1 and term t = s -1 . By induction, the subterm s reduces to one of five cases: Multiplication. Consider the leading operator symbol . and term t = r.s. By induction, the subterms r, s reduce to one of nine cases as in the table for addition above; each case will need an argument. which is in the transversal. This concludes the proof of the theorem.

s = ∞, s = -∞, s

Q tr as a final algebra

We will prove that Q tr is also final among the minimal algebras satisfying the equations in E tr . To do this it is convenient to have a few further lemmas.

Lemma 5.16. If x ∈ Q and x = 0 then x.x -1 = 1.

Proof. By inspection.

Lemma 5.17.

If x ∈ Q and x > 0 then x.∞ = ∞. If x ∈ Q and x < 0 then x.∞ = -∞.
Proof. By inspection.

Theorem 5.2. Let A be any Σ tr algebra and φ : Q tr -→ A be any Σ tr homomorphism that is surjective. Then φ is either an isomorphism, and A is isomorphic to Q tr , or φ is the trivial homomorphism and A is the unit algebra.

Proof. Assume that φ is an epimorphism that is not an isomorphism. Then there are x and y such that x = y and φ(x) = φ(y) in A. We will show that A is the unit algebra and φ is trivial. At first sight there are 13 cases to consider depending upon x and y being rationals, ∞, -∞, or ⊥. By symmetry of equality, and dealing with each case in a certain order these can be reduced to 7 cases:

x ⊥ ⊥ ⊥ ∞ ∞ -∞ r y ∞ -∞ r -∞ r r r Case 1: x =⊥ and y = ∞ and φ(⊥) = φ(∞) in A. φ(0) = φ( 1 ∞ ) by axiom 13 = φ(1) φ(∞) φ is a homomorphism = φ(1) φ(⊥) by case assumption = φ( 1
⊥ ) φ is a homomorphism = φ(⊥) by axiom 26
Thus, φ(0) = φ(⊥) implies 0 A =⊥ A since φ is a homomorphism. Now the identity x + 0 = x holds in Q tr and so it holds in the homomorphic image A.

In particular, for all z ∈ A,

z = z + 0 A = z + ⊥ A =⊥ A
Thus A is the unit algebra.

= φ(s) φ(s) φ is a homomorphism = φ(0) φ(0) φ is a homomorphism = φ(0).φ( 1 0 ) φ is a homomorphism = φ(0).φ(∞) by axiom 13 = φ(0.∞) φ is a homomorphism = φ(⊥) by axiom 24
Thus, a rational and ⊥ maps to the same value, which is Case 3. Finally, we complete this case: suppose φ(r) = φ(s). Then φ(r) -φ(r) = φ(s) -φ(r) and φ(0) = φ(s -r) in A This is the case above.

The following is immediate.

Corollary 5.1. Algebra Q tr is both initial and final in the class Alg min (Σ tr , E tr ) of minimal algebras satisfying the axioms of E tr .

6 Concluding Remarks

Expansion with a sign function

It is central to the idea of transrationals and transreals that the infinite elements admit an ordering, leaving only ⊥ as an unordered element. Following [START_REF] Bergstra | Cancellation meadows: A generic basis theorem and some applications[END_REF], a practical way to deal with the ordering of a meadow is to introduce a sign function s(-). This is possible in the context of transrationals as well. Equations for the sign function can be chosen as follows:

s(0) = 0 (37) s(⊥) =⊥ (38) s(∞) = 1 (39) s(-x) = -s(x) (40)
s(

x 2 + y 2 + z 2 + u 2 + 1 a 2 + b 2 + c 2 + d 2 + 1 ) + 0.(x+y + z + u + a + b + c + d) = 1 + 0.(x + y + z + u + a + b + c + d) (41)
Adding these equations to the equations of E tr enriches the initial algebra with a sign function.

Reflections on floating point

Floating point numbers constitute a subset of the rational numbers and here we have shown how to enlarge the field of rationals to model more closely some semantic aspects of floating point arithmetic. The introduction of ∞ and -∞ was perhaps the first step to ensure the division operations were total. We also introduced the error element ⊥ that we viewed as a quiet "not a number" qNaN. We can step closer to floating point behaviour by introducing a fourth new element to model a signalling "not a number" or sNaN. Suppose we add ⊥ s for the purpose of signalling the need for an interrupt. We can expect the interrupt to take precedence and satisfy the simple axioms:

-⊥ s =⊥ s (42) ⊥ -1 s =⊥ s (43) x+ ⊥ s =⊥ s (44) x. ⊥ s =⊥ s (45) s(⊥ s ) =⊥ s (46)
Clearly, combing these two basic forms of error ⊥ and ⊥ s are a complication but one that can be managed by our equations. In fact these four axioms can be simply added to the axioms of E tr to give an initial algebra specification of an enlarged structure for the transrationals having the stronger error element ⊥ s .

The simple addition of the signalling axioms is an attractive property but does require special features in the design of E tr . The specification E tr is designed to be "weak" in order to cope with such developments. The large number of very simple axioms and the absence of general axioms like x + ⊥=⊥ is one consequence; and the painstaking recovery of properties in lemmas and deductions is another. The equations are designed to have the same variables on both sides of the equality sign to cope smoothly with error propagation.

On approaches to total division

Using a general conceptual framework for analysing numerical data types with total operations, we have given a general mathematical model of the transrational numbers.

The concept of a meadow emerged when we were making an algebraic specification of the rational numbers in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF]; we studied the axiomatic class of meadows in [START_REF] Bergstra | Meadows and the equational specification of division[END_REF]. A substantial series of papers has built an algebraic theory of meadows, e.g., [START_REF] Bergstra | Division safe calculation in totalised fields[END_REF][START_REF] Bergstra | Inversive meadows and divisive meadows[END_REF][START_REF] Bergstra | Probability functions in the context of signed involutive meadows (extended abstract)[END_REF][START_REF] Bergstra | Transformation of fractions into simple fractions in divisive meadows[END_REF].

The concept of a wheel was introduced by Anton Setzer in unpublished notes [START_REF] Setzer | [END_REF]. It was motivated by Jens Blanck's lectures on exact real number computations, based on domains, and Per Martin Löf's suggestion to allow 0 in denominators of elements of quotient fields. Later wheels were studied in greater generality and published by Jesper Carlström [START_REF] Carlstrom | Wheels: on division by zero[END_REF]. Carlström generalised the constructions to semirings, developed equations and identities, and considered the class of wheels. In [START_REF] Bergstra | The wheel of rational numbers as an abstract data type[END_REF] we have provided an equational specification of the wheel of rationals as an abstract data type. An alternative initial algebra specification of the wheel of rationals can be obtained from E tr by replacing ∞ + ∞ = ∞ by ∞ = -∞.

The concept of a transfield and of the transrationals we have taken from [START_REF] Reis | Construction of the transreal numbers and algebraic transfields[END_REF], wherein the focus of the models are the transreals which are intended to support Analysis for computers [START_REF] Anderson | Perspex Machine VIII: axioms of transreal arithmetic[END_REF]. There has been considerable criticism, voiced by experts in the field, of the introduction of transreals by James Anderson et. al. for instance in [START_REF] Anon | British computer scientist's new "nullity" idea provokes reaction from mathematicians[END_REF]. Now some comments can be made on three of these critical remarks: (i) as far as we know the transrationals and transreals were novel structures around 1998, and the suggestion (made in [START_REF] Anon | British computer scientist's new "nullity" idea provokes reaction from mathematicians[END_REF]) that these structures were well-known in mathematics or logic or computer science (e.g., ring theory, model theory, domain theory, abstract data type theory) lacks confirmation, in particular the precise relation between positive infinity, negative infinity, and nullity was a novel design choice; (ii) the suggestion that studying error propagation in infinite data types is "totally meaningless" is in contrast with the extensive literature on infinite data types with error handling; (iii) considering the transrationals and transreals to be merely a rediscovery of IEEE floating point NaN (or qNaN) misses the point that there is a definite lack of theoretical clarity to the design of the floating point number system when it comes to the additional values such as infinity, NaN, qNaN, sNaN, and negative infinity. From the perspective of abstract data type theory, and the design of software specification languages which makes use of abstract data types, Anderson's approach was and still is entirely natural.

  (n, m) + (p, q) = (a, b) where a = nq + mp gcd(nq + mp, mq) and b = mq gcd(nq + mp, mq) Secondly, we define multiplication: (n, m).(p, q) = (a, b) , mq) Thirdly, we define additive inverse: -(n, m) = (-n, m). Let Q = (SF P | (0, 1), (1, 1), +, -, .)

Lemma 5 . 1 .

 51 (Σ tr , E tr ) ⊥ . ⊥=⊥.

Lemma 5 . 2 . 25 =For

 5225 For all closed Σ tr terms t, (Σ tr , E tr ) t + ⊥=⊥ and (Σ tr , E tr ) t . ⊥=⊥ Proof. Consider the first statement using induction on the structure of t. The basis cases of t + ⊥ are as follows. If t ≡ 0 apply axiom 3. If t ≡ 1 use axiom 28. If t ≡ ∞ use axiom 29. For t ≡ -∞ write -∞+ ⊥ = -∞-⊥ by axiom t ≡⊥ use axiom 27. The induction steps follow by applying axiom 31, axiom 29, and axiom 30, and Lemma 5.1.

Lemma 5 . 3 . 5 =Lemma 5 . 5 .

 53555 (Σ tr , E tr ) n + m = n + m and (Σ tr , E tr ) n.m = n.m. Lemma 5.4. (Σ tr , E tr ) 0.n = 0.Proof. We do this by induction on n. As basis note that if n = 0 or n = 1 then the lemma is true by the axioms 7 and 12. Suppose the lemma is true for n = k and consider n = k + 1. Using the axioms we deduce that 0.k + 1 = k + 1.0 by commutativity, axiom (Σ tr , E tr ) m.m -1 = 1 for m > 0.

1 Lemma 5 . 6 . 4 =Lemma 5 . 7 .

 156457 (Σ tr , E tr ) 0.m -1 = 0 for m > 0. Proof. 0.m -1 = (0.m).m -1 by Lemma 5.(Σ tr , E tr ) 0.(n.m -1 ) = 0 for m > 0.

23 = 22 =

 2322 =⊥, s = 0.m -1 and s = n.m -1 with n = 0 in the transversal Tr. If s = ∞ then s -1 = 0 by axiom 14 which is in the transversal. If s = -∞ then s -1 = 0 by axiom 15 which is in the transversal. If s =⊥ then axiom 26 yields s -1 =⊥ which is in the transversal. If s = 0.m -1 then -∞ + a.b -1 = -∞ + -(-(a.b -1 )) by axiom -∞ + -((-a).b -1 ) by axiom -(∞ + a.b -1 ) by axiom 21 = -∞ by the previous case Consider the last case: a.b -1 + c.d -1 = a.b -1 .1 + c.d -1 .1 by axiom 7 = a.b -1 .d.d -1 + c.d -1 .b.b -1 by Lemma 5.5 = a.d.b -1 .d -1 + c.b.d -1 .b -1 by axiom 5 = (a.d.b -1 .d -1 + c.b.d -1 .b -1 ) + 0.b -1 .d -1 by axiom 3 and Lemma 5.6 = (a.d + c.b).b -1 .d -1 + 0.b -1 .d -1 deduction: let p = gcd(a.d + c.b, bd). Choose p , p such that p.p = a.d + c.b and p.p = b.d. Then a.d+c.b bd = p.p p.p = p p , which is in the transversal.

⊥ 24 = 24 a 1 by axioms 5 and 8 = 8 = 5 =

 24241885 . ⊥ = (∞.0).(∞.0) by axiom the transversal. The next case is straightforward: .b -1 .c.d -1 = (a.c).(b.d) -(p.p ).(p.p ) -1 by substitution = (p.p ).(p -1 .p -1 ) by axiom (p.p -1 ).(p p -1 ) by axiom

Case 2 : 23 = 26 Thus, 1 A

 223261 x =⊥ and y = -∞ and φ(⊥) = φ(-∞) in A. φ(∞) = φ(-(-∞)) by axiom -φ(-∞) φ is a homomorphism = -φ(⊥) by case assumption = φ(-⊥) φ is a homomorphism = φ(⊥) by axiom 25Since φ(∞) = φ(⊥) we are in Case 1, and A is the unit algebra.Case 3: x =⊥ and y = r for r = 0 and φ(⊥) = φ(r) in A. ⊥) by ⊥ . ⊥=⊥ as derived in the proof of Lemma 5.1 and axiom =⊥ A . Now the identity x = 1.x holds in Q tr and so it holds in the homomorphic image A. In particular, for all z ∈ A, z = z. ⊥ A =⊥ A Turning to subcase r = 0 and s = 0 in Q tr ,

Acknowledgement We thank Alban Ponse, University of Amsterdam, for pointing out an inconsistency in a previous version of the specification with the help of Prover9-Mace4, which led to the current form of axiom 10.

Proof. First, with Lemma 5.4, we find 0.m = 0 so that with axiom 9 we deduce (m -1 ) -1 = m.

Now axiom 8 yields

(n.(m -1 ) -1 ) + (0.(n -1 + (m -1 ) -1 )) = (n -1 .(m -1 ) -1 ) + (0.(n -1 + (m -1 ) -1 )).

And with 0.m = 0 we have (n.(m -1 ) -1 ) + (0.(n -1 + m)) = (n -1 .(m -1 ) -1 ) + (0.(n -1 + m)).

Taking z = 0 from axiom 11 we find (x + y).0 = x.0 + y.0 whence with commutativity:

(n.(m -1 ) -1 ) + ((0.n -1 ) + (0.m)) = (n -1 .(m -1 ) -1 ) + ((0.n -1 ) + (0.m)).

Combining this with Lemmas 5.4 and 5.6, we can obtain the required result.

Turning to ∞ we have these basic properties:. And with a similar proof one obtains:

Proof. Consider the first statement. Applying Lagrange's Theorem, let m =

Theorem

Theorem 5.1. The initial algebra I(Σ tr , E tr ) of the equations in E tr is isomorphic to the algebra Q tr of transrationals.

Proof. We will take the standard term representation T (Σ tr , E tr ) of initial algebra I(Σ tr , E tr ) and show that T (Σ tr , E tr ) ∼ = Q tr . Recall (3.1) that T (Σ tr , E tr ) = T (Σ tr )/ ≡ Etr and that for t 1 , t 2 ∈ T (Σ tr ),

To work with the congruence we define a transversal Tr of unique representatives of the equivalence classes of ≡ Etr . Let

Proof. To prove soundness we inspect each axiom and show its validity in Q tr . This involves 32 equations, often with many case distinctions each. We give some examples to illustrate the pattern of reasoning.

First, consider if any one of the variables is the error element (0, 0). Note that all equations have the property that the variables that appear on the left side of the equality sign also appear on the right, and vice versa. The definition of the operations in the error case of section 4.3 shows that (0, 0) propagates. Thus, all equations are valid if one of the variables is (0, 0). Thus we need only consider the equations when their variables have values that are rationals or infinities. Note that the infinities do not always propagate, which can lead to many case distinctions in the equations having several variables. 1. Consider associativity: x + (y + z) = (x + y) + z. If all variables are rationals then the equation is easily seen to be valid. There are 26 cases involving the rationals and infinities (1, 0) and (-1, 0). For example, suppose x = (1, 0), y = (1, 0) and z = (-1, 0). Then the LHS is (1, 0) + ((1, 0) + (-1, 0)) = (1, 0) + (0, 0) = (0, 0) and the RHS is ((1, 0) + (1, 0)) + (-1, 0) = (1, 0) + (-1, 0) = (0, 0). -1 ) -1 + 0.x = x + 0.x. If x ∈ Q then the axiom is satisfied immediately when x = 0 and almost immediately when x = 0. Consider the guard term 0.x which appears on both sides. If x = (1, 0) then (0, 1).(1, 0) = (0, 0). By definition, anything added to (0, 0) results in (0, 0). Thus, LHS=RHS. Similarly, If x = (-1, 0) then (0, 1).(-1, 0) = (0, 0) and again LHS=RHS.

Consider (x

3. Consider the four squares equation 35. If all the x, y, z, u are assigned rational numbers then it is easy to see that the equation holds. There are 3 4 -1 = 80 cases remaining in which at least one variable is not assigned a rational value. Consider two cases.

If x = (1, 0) and y, z, u are rationals then the numerator and the denominator of the fracterm is (1,0). Thus the RHS is (1, 0).(1, 0) -1 = (1, 0).(0, 1) = (0, 0). On the LHS the sum of the variables is (1,0). Thus the LHS is (1,1) + (0,1).(1,0) = (1,1) + (0,0) = (0,0). So LHS = RHS.

Let x = (1, 0), x = (-1, 0) and z, u be rationals. Note that the variables on the RHS are squared and so (-1, 0).(-1, 0) = (1, 0) and we have numerator and Addition. Consider the leading operator symbol + and term t = r + s. For notational ease, we write a for n and b for m. By induction, the subterms r, s reduce to one of ten cases in the table below:

The first four cases where r =⊥ follow from the axiom x + ⊥=⊥ and commutativity. The next case ∞ + ∞ = ∞ is axiom 19. The case ∞ + (-∞) =⊥ is axiom 20. There are three cases left. Now

Thus, φ(0) = φ(⊥) and a rational and ⊥ maps to the same value, which is Case 3. Thus, a rational and -∞ maps to the same value, we are in Case 6.