Wheels

Anton Setzer^{∗}

December 7, 1997

Abstract

The following is not very well checked yet, i.e. there might be some typoi and mistakes.

Definition 1 (Quotientwheel of an integral domain) Let R := (|R|, 0, 1, +, ·, −) be an integral domain (integral domain always with 0 ≠ 1). We write R for |R|.

(a) Define ∼ on R^{2} by (a, b) ∼ (a′, b′) ⇔ ∃r, r′ ∈ R.r ≠ 0 ∧ r′ ≠ 0 ∧ (a · r, b · r) = (a′ · r′, b′ · r′).

(b) Let \frac{a}{b} be the equivalence class of (a, b) modulo ∼.

(c) Let R_{⊥}^{∞} := (|R_{⊥}^{∞}|, 0′, 1′, +′, ·′, −′, (\frac{1}{·})′, ∞, ⊥), the quotient wheel of R (name preliminary), be defined by: |R_{⊥}^{∞}| = \{\frac{a}{b} | a, b ∈ R\}. \frac{a}{b} +′ \frac{a′}{b′} := \frac{a·b′+a′·b}{b·b′}. \frac{a}{b} ·′ \frac{a′}{b′} := \frac{a·b}{a′·b′}. −′ \frac{a}{b} := \frac{−a}{b}.

( \frac{1}{\frac{a}{b}})′ := \frac{b}{a}. ∞ := \frac{1}{0}. ⊥:= \frac{0}{0}.

∗This article was insprired by disussions during Jens Blanck’s lectures [Bla97] on [Pot97]. The idea to extend the quotient field by allowing fractions with denominator 0 is due to P. Martin-Löf.

(d) We write R_{⊥}^{∞} instead of |R_{⊥}^{∞}|. Let ι : R → R_{⊥}^{∞}, ι(a) := \frac{a}{1}. We identify a with ι(a), R with ι[R], and omit ′ and sometimes ·. (Note 0′ = \frac{0}{1} = ι(0), 1′ = ι(1)).

Lemma 2 (a) \frac{a}{b} = ι(a) · (\frac{1}{·})′(ι(b)).

(b) R_{⊥}^{∞} = Quot(R) is the quotient field of R, then R_{⊥}^{∞} = Quot(R)∪{∞, ⊥}.

(c) Let a, b ∈ Quot(R). Then the following “multiplication tables” hold in R_{⊥}^{∞}:

\begin{matrix}+ & a & ∞ & ⊥ \\ b & a + b & ∞ & ⊥ \\ ∞ & ∞ & ⊥ & ⊥ \\ ⊥ & ⊥ & ⊥ & ⊥ \end{matrix}

\begin{matrix}· & a ≠ 0 & 0 & ∞ & ⊥ \\ b ≠ 0 & ab & 0 & ∞ & ⊥ \\ 0 & 0 & 0 & ⊥ & ⊥ \\ ∞ & ∞ & ⊥ & ∞ & ⊥ \\ ⊥ & ⊥ & ⊥ & ⊥ & ⊥ \end{matrix}

\frac{1}{x} −x
a ≠ 0 \frac{1}{a} −a
0 ∞ 0
∞ 0 ∞
⊥ ⊥ ⊥

Proof:

(a) a · (\frac{1}{·})′(b) = \frac{a}{1} · \frac{1}{b} = \frac{a}{b}.

(b) Only ⊂: If b ≠ 0, then \frac{a}{b} = \frac{a· \frac{1}{b}}{b· \frac{1}{b}} = ι(a · \frac{1}{b}).

\frac{a}{0} = \frac{1}{0} = ∞ if a ≠ 0. \frac{0}{0} =⊥. (c): Verify.

Definition 3 (a) A wheel is an n-tupel

R_{⊥}^{∞} = (|R_{⊥}^{∞}|, 0, 1, +, ·, −, \frac{1}{·}, ∞, ⊥) ,

where |R_{⊥}^{∞}| is a set (written as R_{⊥}^{∞}), 0, 1, ∞, ⊥∈ R_{⊥}^{∞}, −, \frac{1}{·} are unary functions on R_{⊥}^{∞}, and +, · are binary functions on R_{⊥}^{∞}, written in the usual way, such that for all x, y, z ∈ R_{⊥}^{∞} the following axioms hold:

Commutativity  x + y = y + x.

x · y = y · x.

Associativity  (x + y) + z = x + (y + z).

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

Distributivity  z ≠ ∞ → (x + y) · z = x · z + y · z,
Neutral Elements x + 0 = x

x · 1 = x.

Inverse Elements x ∉ {∞, ⊥} → x + (−x) = 0.

x ∉ \{0, ∞, ⊥\} → x · \frac{1}{x} = 1.

Definition of ∞, ⊥ ∞ = \frac{1}{0}.

⊥= 0 · ∞

Strictness  x· ⊥=⊥

x+ ⊥=⊥. − ⊥=⊥. \frac{1}{⊥} =⊥.

Laws for ∞  x ∉ {∞, ⊥} → x + ∞ = ∞.

∞ + ∞ =⊥. x ∉ {0, ⊥} → x · ∞ = ∞. −∞ = ∞. \frac{1}{∞} = 0.

Non-triviality  0 ≠ 1.

(b) \frac{x}{y} = x · \frac{1}{y}, x − y := x + (−y). The usual conventions like omitting of ·, omitting parentheses (where · binds more than +) apply.

Remark 4 The following axioms

Strictness x· ⊥=⊥
x+ ⊥=⊥.
− ⊥=⊥.
\frac{1}{⊥} =⊥.
Laws for ∞ x ∉ {∞, ⊥} → x + ∞ = ∞.
∞ + ∞ =⊥.
x ∉ {0, ⊥} → x · ∞ = ∞.
−∞ = ∞.
\frac{1}{∞} = 0.

can be replaced by the following axioms:

Laws of \frac{1}{·}  \frac{1}{\frac{1}{x}} = x
\frac{1}{xy} = \frac{1}{x} \frac{1}{y}.
y ≠ ∞ → \frac{x}{y} + z = \frac{x+zy}{y}.
Laws for − (−x)y = −(xy).
(−\frac{1}{x}) = \frac{1}{−x}.
Non triviality ∞ ≠ 0.

or even the special cases:

Laws of \frac{1}{·}  \frac{1}{∞} = 0
\frac{1}{0·y} = ∞ · \frac{1}{y}.
\frac{x}{0} + z = \frac{x+z·0}{0}.
Axioms of − − ⊥=⊥.
−∞ = ∞.

Lemma 5 If R is an integral domain, its quotient wheel is a wheel. Proof: \frac{a}{b} + \frac{a′}{b′} = \frac{ab′+a′b}{a′b′} = \frac{a′}{b′} + \frac{a}{b}. \frac{a}{b} · \frac{a′}{b′} = \frac{aa′}{bb′} = \frac{a}{b} + \frac{a′}{b′}. (\frac{a}{b} + \frac{c}{d}) + \frac{e}{f} = \frac{ad+bc}{bd} + \frac{e}{f} = \frac{adf+bcf+bde}{bdf} = \frac{a}{b} + \frac{cf+de}{df} = \frac{a}{b} + (\frac{c}{d} + \frac{e}{f}). If \frac{a}{b} ≠ ∞, i.e. f ≠ 0 ∨ e = 0, then (\frac{a}{b} + \frac{c}{d}) · \frac{e}{f} = \frac{ad+bc}{bd} · \frac{e}{f} = \frac{ade+bce}{bdf} = \frac{adef+bcef}{bdff} = \frac{ae}{bf} + \frac{ce}{df} = \frac{a}{b} · \frac{e}{f} + \frac{c}{d} · \frac{e}{f}. The other laws are even more straight forward. Task 6 Minimize the number of axioms. (More precisely, the number of symbols for writing a complete axiomatization). The proofs for the following lemmata are not optimized yet.

Lemma 7 Assume R_{⊥}^{∞} is a wheel as above. For x, y ∈ R_{⊥}^{∞} we have (a) 0, 1, ∞, ⊥ are distinct.

(b) R_{⊥}^{∞} \ \{⊥, ∞\} is a field (note that \frac{1}{·} is then partial).

(c) If x + y = x, x ∉ {∞, ⊥}, then y = 0.

(d) If x · y = x, x ∉ {0, ∞, ⊥} then y = 1.

(e) If x + y = 0, then y = −x.

(f) x · 0 = 0, if x ∉ {∞, ⊥}.

(g) If x · y = 1, then y = \frac{1}{x}.

(h) −0 = 0.

(i) \frac{1}{1} = 1.

(j) x + y =⊥ ⟺ x =⊥ ∨y =⊥ ∨x = y = ∞.

(k) If x + y ∈ {0, ⊥} then (x + y) · ∞ = x · ∞ + y · ∞. Otherwise (x + y) · ∞ = ∞ ≠⊥= x · ∞ + y · ∞.

(l) (−x)y = −(xy) = x(−y)

(m) −(−x) = x.

(n) − is injective.

(o) \frac{1}{·} is injective.

(p) \frac{1}{x} · \frac{1}{y} = \frac{1}{xy}.

(q) \frac{1}{\frac{1}{x}} = x.

(r) \frac{1}{−x} = −\frac{1}{x}.

(s) y ≠ ∞ → \frac{x}{y} + w = \frac{x+wy}{y}

(t) y, y′ ∉ \{∞, ⊥\} → \frac{x}{y} + \frac{x′}{y′} = \frac{xy′+x′y}{yy′} Proof:

(a) If ⊥= 1, then ∀x.x = x · 1 = x· ⊥=⊥, 0 = 1, contradiction. If ⊥= 0, then ∀x.x = x + 0 = x+ ⊥=⊥, 0 = 1, contradiction. If ⊥= ∞, then 0 = \frac{1}{∞} = \frac{1}{⊥} =⊥, contradiction. If ∞ = 0, then 1 = 1 + 0 = 1 + ∞ = ∞ = 0, contradiction. If ∞ = 1, then ⊥= 0 · ∞ = 0 · 1 = 0, contradiction. 0 ≠ 1.

(b) by (a). The remaining assertions follow now from (b). But let’s do it from scratch:

(c) y = x + y − x = x − x = 0.

(d) y = \frac{1}{x}xy = \frac{1}{x}x = 1.

(e) If x ∉ {∞, ⊥}, then y = −x + x + y = −x + x = 0. If x =⊥, x + y =⊥≠ 0. If x = ∞, x + y ∈ {∞, ⊥}, x + y ≠ 0.

(f) x · 0 + x = x · 0 + x · 1 = x · (0 + 1) = x · 1 = x, x · 0 = 0.

(g) If x ∉ \{0, ∞, ⊥\}, then y = \frac{1}{x}xy = \frac{1}{x}x = 1. If x = 0, xy ∈ {0, ⊥}, xy ≠ 1. If x =⊥, x · y =⊥≠ 0. If x = ∞, x · y ∈ {∞, ⊥}, x · y ≠ 0. (h): 0 + −0 = 0, −0 = 0. (i): \frac{1}{1} · 1 = 1, 1 = \frac{1}{1}. (j): “←” trivial. “→”: Assume right side is false, left side holds. If x = ∞, then x + y = ∞ ≠⊥. Otherwise y = −x + (x + y) = −x+ ⊥=⊥, contradicting the falsity of the right side. (k): Case x + y = 0. Then x ≠⊥, (x + y) · ∞ = 0 · ∞ =⊥. Subcase x = y = 0: x · ∞ + y · ∞ =⊥. Otherwise x, y ∉ {0, ∞, ⊥}, x = −y, x · ∞ + y · ∞ = ∞ + ∞ =⊥. Case x + y =⊥. Again (x + y) · z =⊥. Case x =⊥ ∨y =⊥. Right side is ⊥. Otherwise follows x = y = ∞, right side is ⊥. Case x + y ∉ {0, ⊥}. Then (x + y) · ∞ = ∞. x ≠⊥, y ≠⊥. If x = 0, then x · ∞ + y · ∞ =⊥. If y = 0, the assertion follows again. Otherwise x · ∞ + z · ∞ = ∞ + ∞ =⊥.

(l) If x ∉ {∞, ⊥}, then (−x)y + xy = (−x + x)y = 0 · y = 0, −(xy) = (−x)y. If x = ∞, ⊥, the assertion is an axiom.

(m) x = ∞, ⊥: by the axioms. Otherwise: x + (−x) = 0, therefore x = −(−x).

(n) Assume −x = −y. Case x =⊥. y ≠ ∞. If y ≠⊥, then 0 = y + −y = y+ ⊥=⊥, contradiction. Case x = ∞: y ≠⊥. If y ≠ ∞, then 0 = y + −y = ∞, contradiction. Case y =⊥, y = ∞: similar. Otherwise x = x + −y + y = x + −x + y = y. (o) Assume \frac{1}{x} = \frac{1}{y}. If x =⊥, then \frac{1}{y} =⊥, y ∉ \{0, ∞\}. If y ≠⊥, 1 = y · \frac{1}{y} =⊥, contradiction. If x = 0, then y ∉ \{⊥, ∞\}. If y ≠ 0, then 1 = y · \frac{1}{y} = ∞, contradiction. If y =⊥, 0, follows again the assertion. Otherwise x = x\frac{1}{y}y = x\frac{1}{x}y = y. (p) x, y ∉ \{0, ∞, ⊥\}: xy \frac{1}{x} \frac{1}{y} = 1. x =⊥: \frac{1}{x} · \frac{1}{y} =⊥= \frac{1}{xy}. y =⊥ similarly. Assume x, y ≠⊥. Case x = 0, y ≠ ∞: \frac{1}{y} ∉ \{0, ⊥\}. \frac{1}{xy} = \frac{1}{0} = ∞, \frac{1}{x} \frac{1}{y} = ∞\frac{1}{y} = ∞. Case x = 0, y = ∞: both sides are ⊥. Case x = ∞, y = 0: similarly. Case x = ∞, y ≠ 0: \frac{1}{xy} = 0 = \frac{1}{x} \frac{1}{y}. Case y = ∞: similarly. (q): x = 0, ∞, ⊥: trivial. Otherwise \frac{1}{x} · x = 1, \frac{1}{\frac{1}{x}} = x. (r): The cases x = 0, ∞, ⊥ can be easily verified. Otherwise we have (−x) · (−\frac{1}{x}) = −(−(x · \frac{1}{x})) = x, and the assertion. (s): If x =⊥ or y =⊥ or w =⊥, both sides are ⊥. Assume x, y, w ≠⊥. Case x = y = 0: wy ∈ \{0, ⊥\}, left side is ⊥, right side is \frac{0}{0} or \frac{⊥}{0}, therefore ⊥. Case y = 0, w = ∞: both sides ⊥. Case y = 0, w ≠ ∞: both sides are ⊥, if x = 0 and ∞ otherwise. Otherwise: y ≠ 0, ∞, ⊥, \frac{x}{y} + w = \frac{1}{y} · y · (\frac{x}{y} + w) = \frac{1}{y} · (x + wy). (t): By (s)

Lemma 8 Let a, b, c, d, e, f, r, s ∈ R_{⊥}^{∞} \ {∞, ⊥} (as well with indices and accents), R_{⊥}^{∞} be a wheel.

(a) Every element of R_{⊥}^{∞} can be written as \frac{x}{y} with x, y ≠⊥, ∞.

(b) \frac{a}{b} = \frac{a′}{b′} ⟺ ∃r ∉ \{0, ∞, ⊥\}.(ar, br) = (a′r′, b′r′).

(c) \frac{a}{b} + \frac{a′}{b′} = \frac{ab′+a′b}{bb′}.

(d) −\frac{a}{b} = \frac{−a}{b}.

(e) \frac{a}{b} \frac{c}{d} = \frac{ac}{bd}.

(f) \frac{1}{\frac{a}{b}} = \frac{b}{a}.

Proof:

(a) ∞ = \frac{1}{0}, ⊥= \frac{0}{0}. Otherwise x = \frac{x}{1}.

(b) Assume \frac{a}{b} = \frac{a′}{b′}. Case b, b′ ≠ 0: ab′ = \frac{a}{b}bb′ = \frac{a′}{b′} = a′b, choose r = b′, r′ = b. If b = 0 ∨ b′ = 0, then \frac{a′}{b′} = \frac{a}{b} ∈ \{∞, ⊥\}, b = b′ = 0. Further a = 0 ⟺ \frac{a}{b} =⊥ ⟺ a′ = 0. Choose, if a = 0, r, r′ = 1 otherwise r := a′, r′ := a. In the other direction it suffices to show \frac{a}{b} = \frac{ar}{br} if a, b, r ∉ \{∞, ⊥\}, r ≠ 0. If b = 0, br = 0, further a = 0 ⟺ ar = 0 (multiplb with \frac{1}{r}), \frac{a}{b} = \frac{ar}{br}. Otherwise \frac{ar}{br}b = \frac{1}{r}rb\frac{ar}{br} = ar\frac{1}{r} = a(r\frac{1}{r}) = a, \frac{a}{b} = a\frac{1}{b} = \frac{ar}{br}. (c), (d), (e), (f): Immediate by the properties proved before.

References

[Bla97] J. Blanck. One possible approach to efficient implementation of exact real arithmetic (I – III). Lectures given in the Logic seminar Uppsala-Stockholm, 1997.

[Pot97] P. J. Potts. Efficient on-line computation of real functions using exact floating point. Manuscript, Dept. of Computing, Imperial College, London, 1997.