.Open Numbers
. Hoare's Axioms
Tony Hoare published a paper with an axiomatic system for floating point numbers.
.Open Hoare69
 C A R Hoare
 An Axiomatic Basis for Computer Programming
 Comm ACM V12n10(Oct 69)pp576..580+583
.Close

Compare with the various algebras with two operators
.See http://www/dick/maths/math_41_Two_Operators.html

HOARE::=Net{

	For Numbers::Sets=`Positive integers used by the computer`.

(Hoare Operations):
	+ ::infix(Numbers), given.
	- ::infix(Numbers), given.
	* ::infix(Numbers), given.
(Hoare Constants):
	0::Numbers, given.
	1::Numbers, given.

Use x,y,z to represent these Numbers:
 For x,y,z:Numbers.

(Hoare Axioms):
	|- (A1):	x+y=y+x.
	|- (A2):	x*y=y*x.
	|- (A3):	x+(y+z)=(x+y)+z.
	|- (A4):	x*(y*z)=(x*y)*z.

	|- (A5):	x*(y+z)=x*z + x*z.

	|- (A6):	if y<=x then (x-y)+y = x.
	|- (A7): 	x+0 =x.
	|- (A8):	x*0=0.
	|- (A9):	x*1=x.

(Hoare types):
	infinite_arithmetic::@=for no x, all y(y<=x).
	finite_arithmetic::@=for one max:Numbers, all x (x<=max).
}=::HOARE.

FINITE_HOARE::=Net{
	|- $HOARE and $finite_arithmetic.
	|- max=the  m:Numbers ( for all x (x<=max)).
	strict_overflow::@=for no x(x=max+1).
	firm_boundary::@= (max=max+1).
	modulo_arithmetic::@=(0=max+1).

}=::FINITE_HOARE.

.Open Classical Number Theory
.Source Hardy & Wright, Gause, ...
Number_Theory::=Net{
        Nat::=`The natural Numbers: 1,2,3,4....`.
        Natural::=`The natural Numbers: 1,2,3,4....`.
        Nat0::=Nat | {0}.
        Positive::=Nat | {0}.
	()|- Nat0 = Positive.
       |- (N0): Abelian_group(Nat0, (+), 0, (-)).
       |- (N1): {1} generates (Nat).
       |- (N2): Abelian_monoid(Nat, (*) ,1).
	|- (N3):For all m:Nat0, 0*m=0.
        |- (N4):(*) distributes (+).
	()|-(N5): for all n,m:Nat0, (n+1)*m=n*m+m.
        ()|-(N6): for all m:Nat0, n:Nat (n*m=(n-1)*m+m).
        ()|-(N7): for all n (2*n=n+n).
       |- (N8): For n,m:Nat0, n<=m::=for some l:Nat(n+l=m).

The numbers are a Linearly ordered Sets I define in
.See http://www.csci.csusb.edu/dick/maths/math_21_Order.html#loset
as part of the theory of Partially Ordered Sets or Posets.
ORDER::=http://www.csci.csusb.edu/dick/maths/math_21_Order.html.

	|- $ORDER.
        (ORDER)|-(N9): loset (Nat0,<).

The above also imports the definitions for intervals like n..m,
n..*, and *..m. See $Intervals below.

The critical disinction between the natural numbers and other
number-like logics is that they are well-ordered:

|- (woset): < in Left_limited(Nat0).

(woset)|-(induction): for all P:@Nat($INDUCTION(P) ).
INDUCTION::=Net{ 
  P::@Nat.
   basis::= 1 in P.
   step::=for all k:P (k+1 in P).
	|- (b): basis. 
	|- (s): step.
	 (b,s)|-(result): P=Nat.
. Proof of result
	Let{
	|- (1):  P<>Nat. 
	Q::=Nat~P
	(1,def)|-(2): Q<>{},
	(2,def)|-(3): some Q.
We now think about the question: "Which Nat could be in Q?".  First, 1 can not be an element in Q because:
	   (b)|-(3): not 1 in Q.
So any element of Q must be > 1.
But if there are any then there will be a smallest one:
	 (3,woset)|-(4):    one least Q,
	       (4) |-    q:= the least Q,
	       (def) |-(5): q in Q and not q-1 in Q,
	     (5,3)|-(6):   q<>1,
	  (6) |-(7):    q-1 in Nat~Q
		(8):	=P,
	   (8,group)|- (9): (q-1)+1 = q in Q
	    (s,8)|-(10):    (q-1)+1 in P  
	     (10):   |-(11):    p in P & Q = {}
	}  
. Proof of 5
|-(5.0): q=the least Q
|-(5.1):	iff  q in Q and for no r:Q( r < q ).
(def)|-(5.2):	q-1<q.
(5.1, 5.2, r:=q-1)	|-(5.2): q in Q and not (q-1 in Q).

}=::INDUCTION.


|-(induction1): for all P:@Nat, if 1 in P and for all k:P(k+1 in P) then P=Nat.
|-(induction2):	for all P:@Nat, if 1 in P and (_+1)(P) ==> P then P=Nat.


. Intervals
(STANDARD)|- For n,m, n..m={i||n<=i<=m}.
	n....m::=(n+1)..(m-1),
(STANDARD)|- For n, n..*={i||n<=i}
(STANDARD)|- For m, *..m={i||i<=m}.

Number theory often needs other specialized intervals:
 For n,m, n.*k::=n..(n+k-1),
 For n,m,k, n.(k).m::={l||for some i:Nat0(l=n+i*k<=m)},
        ...

. Powers
 For n,m:Nat0, n^m::= *[1..m](n), 
 For n,m:Nat0, powers(n) ::={n^m || m:Nat0}.
	()|-(N10): for n:Nat0, n^0=1, 
	()|-(N11): n^1=n,
	()|-(N12): n^2=n*n, 
	()|-(N13): for n,m:Nat, n^m = n*(n^(m-1)).

. Factorial Function
 For n:Nat0, n!::Nat0,
	|- if n>0 then n!=*(1..n)
	|- if n<=0 then n!= 1.

	()|- for n>0, n! = n* (n-1)!.

. Binomial Coefficients.
C::=$binomial_coefficient,  C(n,r) is the number of combinations of n things taken r at a time.
binomial_coefficient::=(Nat0><Int)->Nat0,
 For n:Nat0, r:0..n, C(n,r) ::= *(r+1..n)/r!,
 For n:Nat0, r:Int~0..n, C(n,r) ::=0.

|-(N14): for n:Nat0, r:0..n, C(n,r)=n!/(r!*(n-r)!)=C(n,n-r).
|-(N15): for n:Nat0, r:Int, C(n,r)=n*C(n-1,r-1)/r and	C(n,r)=C(n-1,r)+C(n-1,r-1) and	C(n+r+1,n)=+[k:0..n]C(r+k,k).
|-(N16): for n,m:Nat0, C(n+1,m+1)=+[k:0..n]C(k,m).

. Divisors and Factors
	divides::@(Int, Int), in number theoretic texts this written (|).
|- (N17): For n:Nat,m:Nat0, n divides m = for some q:Nat0(n*q=m).
	()|- 3 divides 12.
()|-(N18): (Nat0, divides) in poset, (partially ordered set).
For n:Nat0, divisors(n) ::={m:Nat||m divides n},
Note: we do not allow 0 to be a divisor/factor.
 factors ::= divisors.
	()|- divisors(12) = {1,2,3,4,6,12}.

()|-(N19): for all n:Nat, {1,n}==>divisors(n)==>1..n.
Each number is divisible by 1 and by itself.

()|-(N20): (Nat, divides) in poset(bottom=1).

	common_factors::=map[N:@Nat] &(divisors(N), intersection of sets of divisors.

 For n,m, hcf(n,m) ::= max (divisors(n) & divisors(m)), highest common factor,
or greatest common divisor (gcd).
	|- (N21): SERIAL(hcf). 
	(N21)|-(N22): hcf(l,m,n)=l hcf m hcf n=hcf(l, hcf(m,n)).
	()|- 10 hcf 12 = 2.
	()|-(N23): semilattice(Nat, hcf).
 For n,m, relatively_prime(n,m) ::= (hcf(n,m)=1).

()|-(N24): hcf(a,b)= smallest{n:Nat || for some x,y:Int(n=x*a+y*b)}.
Note that x and y include negative numbers so we want the smallest
element in a set that includes a-b, b-a, a-2b, 3a-4b, and so on.

  ...Euclid's Algorithm...
.Net
	()|-(Eu1): hcf(n,n)=n.
	()|-(Eu2): hcf(1,n)=1.
	()|-(Eu3): hcf(0,n)=n.
	()|-(Eu4): hcf(n,m)=hcf(m,n).
	()|-(Eu5): for n>m, hcf(n,m)=hcf(n-m,m).
.Close.Net
For an example of Euclid's algorithm being used in rational numbers see
.See http://www/dick/cs320/prolog/rational.plg
(Prolog).

. Linear Diophantine Equations
Solving an equation like: 10x+12y = 3 depends on the hcf(10,12).
()|-(N25): for all a,b,c:Int, some x,y:Int(a*x+b*y=c) iff hcf(a,b) divides c.

If x0, y0 is a solution of a*x+b*y = c and h = hcf(a,b) then each solution has
the form x=x0+t*b/h and y=y0-t*a/h where t:Int.

See pages 46..49 of
.See [PettofrezzoByrkit85]
or any other good book of elementary number theory.


. Multiples
	is_a_multiple ::= /divides, inverse or converse of divisor.
	()|- n is_a_multiple m = m divides n.
	multiples::=map[n]{m|| n divides m}.

	lcm::= map[n,m] min( multiples(n) & multiples(m) ), Least common multiple.

	()|-(NM): lcm(n) * hcf(n) = *(n).


. Primes
Define the set of all prime numbers ($Primes)and the sequence of all primes in increasing order ($prime).
Primes ::= {p:Nat0 || divisors(n)={n,1}}, I like letting 1 be a prime
number... even if it makes a number of theorems a little harder to
state. 

However by defining a sequence `prime` that list all the primes but
omits 1, we can have our cake and also eat it...  

We just use `primes= |(prime)` for mathematical work:
primes::= Primes~{1}.
prime:Nat-->Nat::=primes;/|;>.
	()|- {1,2,3,5,7} are Primes and (2,3,5,7,...)=prime.
	()|-(N26): primes and |prime in Infinite.
	(primes)::= {p:2..*. for no d:2..p-1(d divides p).

I posted some elementary results
.See ../samples/primes.html
about the numbers close to prime number in November of 2005.

 For n:Nat, \pi(n) ::= | (|prime & 1..n)| , 

()|- (Prime Number Theorem): lim [n+>oo] (\pi(n)*(log[e]n)/n))=1.

()|-(N27): For n,m,p:Nat, if p in primes and p divides n*m then (p divides n or p divides m).
()|-(N28): For primes p, n:Nat, a:Nat^n, if p divides *a then for some i:1..n(p divides a(i)).
()|-(N29): For primes p, n:Nat, a:prime^n, if 1 <> p divides *a then for some i:1..n(p = a(i)).

()|- (Fundamental Theorem of Arithmetic): For n:Nat, one p:#primes(n=*p and <=(p)).
()|- (Fundamental Theorem of Arithmetic 2): For n:Nat,  one f:Nat, p:1..f-->prime, a:1..f->Nat(n= *[i](p(i)^a(i)) and <=(p) ).
 For n:Nat, standard_factorization(n) ::=  the a:#Nat (n=*[i:dom(a)](prime(i)^a(i) ).
	()|- 12= 2^2 * 3^1 and standard_factorization(12)=(2,1)



.Hole
. Modular arithmetic
 For n:Nat0,m:Nat, n mod m ::= the[r:0..n-1](for some q:Nat0(n=q*m+r)).
 For n:Nat0,m:Nat, n div m ::= the[q:Nat0](for some r:0..n-1(n=q*m+r)).

	()|-(N30): (n div m) * m + n mod m = n

	()|-(N31): for n, divisors(n)={m:Nat||n mod m = 0}

Gause developed the idea of using equivalence modulo a number as a 'kind of
equality' - what evolved into the concept of an equivalence relation.  The
common term in number theory was 'congruence'.  This term is now a general
monoid theoretic concept.  Here is a piece of the special theory for numbers:

 For p:Nat, \equiv[p] ::= rel[n,m:Nat0](n mod p = m mod p).

	()|-(N32): For p, \equiv[p] = (= mod (_ mod p)).

For n,m,p, n \equiv[p] m = (n = m wrt (_ mod p))
Use MONOID.
	()|-(N33): for all p:Nat, \equiv[p] in congruence(Nat0,+,0) & congruence(Nat,*,1).

()|-(Fermat's Little Theorem): for all prime p, Nat0 n ( p divides (n^p)-n).
.Source Fermat 1640, Letter from Fermat to Frenicle 18th October 1640

Carmichael_numbers::={p:Nat0~prime || for all n (p divides (n^p)-n)}.
	()|-(N34): {561, 1105, 1729, 2465, 2821}==>Carmichael_numbers.
.See http://mathworld.wolfram.com/CarmichaelNumber.html

	()|-(Korselt's Criteria): for Nat0 n, n in Carmichael_numbers iff for all prime p(if p divides n then p-1 divides n-1) and for no p(p^2 divide n).

	()|-(N35):for abf N, Card(Carmichael_numbers & [1..N)) > n^(2/7)
.Source Devlin 92, Kieth Devlin, There are Infinitely Many Carmichael Numbers, MAA Focus V12n4(Sep 92)pp1,2

()|-(Fermats Theorem): for all prime p, Nat0 n, if hcf(p,n)=1 then n^(p-1) \equiv[p] 1.

()|-(N36): a^p \equiv[m] a^q iff p \equiv[t] q where t = the smallest {k:1..m || a^k \equiv[m] 1 }.


. Totient Functions
\phi::=`Euler's totient Function`,
	For m:Nat0, \phi(m) ::=|{n:1..m || relatively_prime(n,m)}|,
	()|-(N37): \phi(1)=\phi(2)=1,...
	()|-(N38): For primes p, \phi(p)=p-1.
	()|-(N39): For primes p, Nat n, \phi(p^n)=p^n-p^(n-1)=p^n*(1-1/p).
	()|-(N40): for a:standard_factorization(n)( \phi(n)	=*[i:1..|a|](prime(i)^a(i) - prime(i)^(a(i)-1)) =n*[i:1..|a|]((1-1/prime(i)).

	()|-(N41): for all n, +(\phi o divisors(n))=n.
	()|-(N42): For all n,m, \phi(n*m)=\phi(n)*\phi(m).
()|-(Euler's Theorem): for  Nat0 n,m, if hcf(m,n)=1 then n^\phi(m) \equiv[m] 1.
()|-(N43): For a,m:nat, if hcf(a,m)=1 then { x:nat || a*x \equiv[m] b} ={ a^(\phi(m)-1)b mod m}

()|-(N44): For a,b,m,	|solutions{ x:0..m-1, a*x \equiv[m] b }| =hcf(a,m)  iff hcf(a,m) divides b.
()|-(N45): For a,b,m,	|solutions{ x:0..m-1, a*x \equiv[m] b }| =0  iff not hcf(a,m) divides b.
()|-(N46): For a,b,c,some solutions{ x,y:Nat0, a*x+b*y=c }iff hcf(a,b) divides c.
()|-(N47): For a,b,c,d,some solutions{ x,y:Nat0, a*x+b*y+c*z=d }iff hcf(a,b,c) divides d.

()|-(Wilson's Theorem):  p in prime iff (p-1)!+1 \equiv[p] 0.
()|-(N48): For a,b,c,m, some solutions{ x,y:0..m-1, a*x+b*y \equiv[m]c }iff hcf(a,b,m) divides c.

()|-(Chinese Remainder Theorem):  For n:Nat, m:Nat^(1..n), M:=*m, L:=max(m),   if for all i,j:1..n( if i<>j then hcf(m(i), m(j))=1 )   then for all a:(0..L)^(1..n),  one solutions{ x:0..M , for all i:1..n(x \equiv[m(i)] a(i))}.
So
define
	R(m) ::=representations(m) ::= {a:(0..L)^(1..n) || for all i(a(i) in 0..m(i))},
and
	\rho(m) ::=represent(m)::=map[x](map[i](x mod m(i))).

|- if for all i,j:1..n( if i<>j then hcf(m(i), m(j))=1 )  then \rho(m) in 1..*m---R(m)

.Source Hardy & Wright 1912
and
.Source Pettofrezzo & Byrkit 1985

}=::Number_Theory.
.Close Classical Number Theory

. Contiguity and  Alignment of Integer Intervals
When IBM wanted to upgrade and reimplement its transaction processing
system CICS (Customer Information C????
.Hole
System) they invited Jim
Woodcock of the "formal methods" community in Europe
to try out formal
specification techniques and in particular the Z ("zed") language.

He published some results..... the most interesting was that he
had to spend a lot of time establishing elementary results
in number theory before he could get to grips with the actual
operating system itself.

From Jim Woodcock's study of the Z model of CICS
.Source Woodcock 89
        contig::=img(`..`),
        For m:Nat0, k:Nat,
          floor(m,k) ::=(m div k)*k,
          ceiling(m,k) ::=for f=floor(m,k){(true,f),(false,f+1)}(m=f),
          aligned(k) ::={S:@Nat||for a:S, f=floor(a,k)(f.*k are S)},
          ()|-(CA1): aligned(k) in sub_monoid(@Nat,|,{}).

. Real Numbers
Real_Numbers::=Net{
Uses Integers.
|- FIELD(Real,(+),0,(-),(*),1,(/), Archimedian, not finite, ordered, absolute_value=>abs).

Nonzero::=Real~{0},
Realoo::=Real|{oo,-oo}.

. Intervals
(a..b) ::={x:Real||a<x<b},
[a..b) ::={x:Real||a<=x<b},
(a..b]::={x:Real||a<x<=b},
a..b::={x:Real||a<=x<=b}. Avoid [a..b] because it is ambiguous.

(a..) ::={x:Real || a<x },
[a..) ::={x:Real || a<=x },
Positive::=[0..),
(a..]::={x:Realoo || a<x or x=oo},
[a..]::={x:Realoo || a<=x or x=oo},

(..a) ::={x:Real || a>x },
[a..) ::={x:Real || a>=x },
Negative::=(..0],
(..a]::={x:Realoo || a>x or x=-oo},
[..a]::={x:Realoo || a>=x or x=-oo},

. Mapping reals into the integers 
[Knuth 69, section1.2.4]

floor::=[x:Real]greatest{i:Int||i<=x}

ceiling::=[x:Real]least{i:Int||i>=x}

mod::=[x,y:Real](x-y*floor(x/y))

fractional_part::=[x:Real](x mod 1.0)

(def)|-For n:Int, floor(n)=n=ceiling(n).

(def)|-For x:Real,n:Int,
	floor(x)<n iff x<n
  and	ceiling(x)<=n iff x<=n
  and	n<=floor(x) iff n<=x
  and	n<ceiling(x)iff n<x.

(def)|-For all x:Real, floor(-x)= -ceiling(x).

(def)|-for x:Real,	x-1 < floor(n) <= x <= ceiling(n) < x+1.
(def)|-for x:Real, floor(x)=the [n:Int](x-1<n<=x)=the [n](n<=x<n+1).
(def)|-for x:Real, ceiling(x)=the [n:Int](x<=n<x+1)=the [n](n-1<x<=n).


(def)|- For x:Real, m:Int, n:Nat, floor((x+m)/n)=floor((floor(x)+m)/n)

Binomial Theorem
(def)|-(binomial theorem): for x,y:Real, n:Int, (x+y)^n=+[r:Int]C(n,r)*x^r*y^(n-r).

...
.Hole

}=::RealNumbers.
.Open Number Representations
. Fixed Point
FIXED_POINT::=Net{ 
	signed:: @=`true if representation allows negative numbers`,
	unsigned::@=`true if representation does not handle negative numbers`.  
	|- (FP0): unsigned iff not signed.
	|- (FP1): if normal then unsigned.  -- indicates a default value.... assume unsigned if not known.

	base::Nat=`A $given positive Base for the number system`.
Common bases are: 2, 8, 10, and 16.
	binary::@=`Computer arithmetic and Liebnitz`. 
	|- (FP2):binary iff base=2.
	octal::@=`Older English and DEC computers`. 
	|- (FP3): octal iff base=8.
	decimal::@=`Number of fingers(digits) on two human hands`. 
	|- (FP3): decimal iff base=10.
	hexadecimal::@=`Most post 1980's computers use 8 bit bytes`. 
	|- (FP3): hexadecimal iff base=16.

	length::Nat=`number of digits`, 
	scale::Nat=`Normally 0, scale can be used to represent fractions`.


	UNSIGNED_MODEL::=Net{
		digits::0..(length-1)->(0..(base-1)), 
		value::= (+[i:|/digits](digits(i)*(base^i)))/(base^scale)
	}=::UNSIGNED_MODEL.
	SIGNED_MODEL::=Net{
		sign::Bit, 
		digits::0..(length-2)->(0..(base-1)), 
		unsigned_value::= (+[i:|/digits](digits(i)*(base^i)))/(base^scale)
		value::=  if(sign=1, -1, 1) * unsigned_value.
	}=::SIGNED_MODEL.
	|- if $unsigned then $UNSIGNED_MODEL.
	|- if $signed then $SIGNED_MODEL.

	if scale=0 then fixed::@Nat0= 0..(base^length)-1.
	if scale<>0 then fixed::@Rational= (0..(base^length)-1)/(base^scale).
	if signed and scale=0 then fixed::@Nat0=  (0..(base^length)-1)-floor(base^(length-1)/2).
	if signed and scale<>0 then fixed::@Rational=  (((0..(base^length)-1))-floor(base^(length-1)/2))/(base^scale).
	
}=::FIXED_POINT.

TWOS_COMPLEMENT::=Net{
A notation that is very convenient for electrons.  Adding
a negative number is done precisely the same way as adding
a positive one.
	|- $FIXED_POINT.
	|-binary.
	|-scale=1.
	digits::0..(length-1)->0..1.
	value::=(+[i:|/digits](digits(i)*(base^i))) - 2^(length-2)).
}=::TWOS_COMPLEMENT.

. Floating Point
FLOATING_POINT::=Net{ -- always signed
	m::=mantissa_length::Nat.
	b::=base::Nat.
	e::=exponent_length::Nat.
	f::=offset::Nat.

	MODEL::=Net{
		mantissa::$ $FIXED_POINT(base=>b, length=>m-1, scale=>1, signed),
		exponent::$ $FIXED_POINT(base=>b, length=>e-1, scale=>1, signed),
		value::=mantissa.value * b^( exponent.value -  f)

	}=::MODEL.

	float:: $FIXED_POINT(base=>b, length=>m-1, scale=>1, signed).fixed * b^( $FIXED_POINT(base=>b, length=>e-1, scale=>1, signed).fixed -  f).

}=::FLOATING_POINT.

. IEEE Standard Floating Point
IEEE::=Net{ --standard floating point forms.

The Institute of Electrical and Electronic Engineers (IEEE) has defined
a standard format for binary floating point numbers.  This has a number
of pragmatic features added to the theoretical format.  As a result all
computers in the 21st century have some IEEE standard floating point
on them.

Two pointers from Dr. Yasha Karant:
.See http://www.sns.ias.edu/Main/computing/compilers_html/common-tools/numerical_comp_guide/ncg_math.doc.html
.See http://www.sns.ias.edu/Main/computing/compilers_html/common-tools/numerical_comp_guide/index.html
and a page that converts decimal numbers into IEEE format
.See http://babbage.cs.qc.edu/courses/cs341/IEEE-754.html
from Ian Lasky.

I found pages 197 thru to 201 of the following a simple and comprehensive
source of information:
.Set
 The Computer Professional's Quick Reference
 MS Vassiliou & JA Orenstein
 McGrawHill 1991
 ISBN 0-07-067211-1(paperback)
.Close.Set

A peculiarity of the standard is that it defines two special values:
NaN::=Not a Number.
INF::=Infinity

Here is an example:
IEEE_64BIT::=following,
.Net
The 64 double length IEEE Standard.
 s::Bit, 1 bit sign,
 e::$ $FIXED_POINT(binary, unsigned, length=11, scale=>1), 11 bit exponent,
 M::$ $FIXED_POINT(binary, unsigned, length=52, scale=1), 52 bit mantissa.
 value::Rational=goal.
 sign::{-1,1}=goal,
|- sign= if s then -1 else 1.
 For b:#Bit, val(b) ::= $FIXED_POINT(binary, unsigned, digits=>b).value.

The rules get complex
.Box
 |- if e=2047 and M<>0 then value=$NaN
 |- if e=2047 and M=0 then value=sign * $INF
 |- if 0<e<2047 and M=0 then value=sign * 2^(e-1023)*$val("1." M)
 |- if e=0 and M<>0 then value=sign * 2^(-1023)*$val("0." M)
 |- if e=0 and M=0 then value=sign * 0
.Close.Box
They make more sense as a table:
.Table e	M	value
.Row 2047	0	sign*INF
.Row 2047	<>0	NaN
.Row 0	0	sign * 0
.Row 0	<>0	sign*2^(-1023)*val("0."M)
.Row else	<>0	sign*2^(e-1023)*val("1."M)
.Close.Table
.Close.Net
.Close Number Representations

.Open Other Number-like Systems
. Interval Arithmetic
It is possible to construct an arithmetic of intervals or ranges.
The result has several applications in computer science but less
interest by mathematicians. 

.Hole
. Generic Number Fields and Integral Domains.
.See ./math_45_Three_Operators.html
. Complex Numbers
.Hole
. Quaternions
.Hole
. Octonions and Cayley Numbers
.Hole
. Vectors & Matrices

See 
.See ./math_45_Three_Operators.html#Vector Spaces

.Hole
.Close Other Number-like Systems


. Glossary
given::=indicates the declaration of a variable that is a parameter of the network of definitions etc.
goal::=indicates the declaration of a variable that is defined in terms of the given parameters.
Net::=network of variables+assumptions+results+definitions.
.Close Numbers