[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / math_42_Numbers
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Thu Nov 10 09:50:10 PST 2011

# Numbers

## Hoare's Axioms

Tony Hoare published a paper (Hoare69) with an axiomatic system for floating point numbers.

Compare with the various algebras with two operators [ math_41_Two_Operators.html ]

1. HOARE::=
Net{

1. For Numbers::Sets=Positive integers used by the computer.
2. +::infix(Numbers), given.
3. -::infix(Numbers), given.
4. *::infix(Numbers), given.
(Hoare Constants):
5. 0::Numbers, given.
6. 1::Numbers, given.

Use x,y,z to represent these Numbers:

7. For x,y,z:Numbers.

(Hoare Axioms):

8. |- (A1): x+y=y+x.
9. |- (A2): x*y=y*x.
10. |- (A3): x+(y+z)=(x+y)+z.
11. |- (A4): x*(y*z)=(x*y)*z.

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

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

(Hoare types):

17. infinite_arithmetic::@=for no x, all y(y<=x).
18. finite_arithmetic::@=for one max:Numbers, all x (x<=max).

}=::HOARE.

2. FINITE_HOARE::=
Net{

1. |-
2. |-max=the m:Numbers ( for all x (x<=max)).
3. strict_overflow::@=for no x(x=max+1).
4. firm_boundary::@= (max=max+1).
5. modulo_arithmetic::@=(0=max+1).

}=::FINITE_HOARE.

## Classical Number Theory

Source: HardyWright12, Gause

1. Number_Theory::=
Net{
1. Nat::=The natural Numbers: 1,2,3,4.....
2. Natural::=The natural Numbers: 1,2,3,4.....
3. Nat0::=Nat | {0}.
4. Positive::=Nat | {0}.
5. (above)|-Nat0 = Positive.
6. |- (N0): Abelian_group(Nat0, (+), 0, (-)).
7. |- (N1): {1} generates (Nat).
8. |- (N2): Abelian_monoid(Nat, (*) ,1).
9. |- (N3): For all m:Nat0, 0*m=0.
10. |- (N4): (*) distributes (+).
11. (above)|- (N5): for all n,m:Nat0, (n+1)*m=n*m+m.
12. (above)|- (N6): for all m:Nat0, n:Nat (n*m=(n-1)*m+m).
13. (above)|- (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 [ loset in math_21_Order ] as part of the theory of Partially Ordered Sets or Posets.

14. ORDER::= See http://www.csci.csusb.edu/dick/maths/math_21_Order.html.

15. |-
16. (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:

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

18. (woset)|- (induction): for all P:@Nat(INDUCTION(P) ).
19. INDUCTION::=
Net{
1. P::@Nat.
2. basis::= 1 in P.
3. step::=for all k:P (k+1 in P).
4. |- (b): basis.
5. |- (s): step.
6. (b, s)|- (result): P=Nat.

### Proof of result

7. Let{
8. |- (1): P<>Nat.
9. Q::=Nat~P
10. (1, def)|- (2): Q<>{},
11. (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:
12. (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:
13. (3, woset)|- (4): one least Q,
14. (4)|-q:= the least Q,
15. (def)|- (5): q in Q and not q-1 in Q,
16. (5, 3)|- (6): q<>1,
17. (6)|- (7): q-1 in Nat~Q
18. (8): =P,
19. (8, group)|- (9): (q-1)+1 = q in Q
20. (s, 8)|- (10): (q-1)+1 in P
21. (10):|- (11): p in P & Q = {}
22. }

### Proof of 5

23. |- (5.0): q=the least Q
24. |- (5.1): iff q in Q and for no r:Q( r < q ).
25. (def)|- (5.2): q-1<q.
26. (5.1, 5.2, r:=q-1)|- (5.2): q in Q and not (q-1 in Q).

}=::INDUCTION.

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

### Intervals

22. (STANDARD)|-For n,m, n..m={i||n<=i<=m}.
23. n....m::=(n+1)..(m-1),
24. (STANDARD)|-For n, n..*={i||n<=i}
25. (STANDARD)|-For m, *..m={i||i<=m}.

Number theory often needs other specialized intervals:

26. For n,m, n.*k::=n..(n+k-1),
27. For n,m,k, n.(k).m::={l||for some i:Nat0(l=n+i*k<=m)},
28. ...

### Powers

29. For n,m:Nat0, n^m::= *[1..m](n),
30. For n,m:Nat0, powers(n)::={n^m || m:Nat0}.
31. (above)|- (N10): for n:Nat0, n^0=1,
32. (above)|- (N11): n^1=n,
33. (above)|- (N12): n^2=n*n,
34. (above)|- (N13): for n,m:Nat, n^m = n*(n^(m-1)).

### Factorial Function

35. For n:Nat0, n!::Nat0,
36. |-if n>0 then n!=*(1..n)
37. |-if n<=0 then n!= 1.

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

### Binomial Coefficients.

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

43. |- (N14): for n:Nat0, r:0..n, C(n,r)=n!/(r!*(n-r)!)=C(n,n-r).
44. |- (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).
45. |- (N16): for n,m:Nat0, C(n+1,m+1)=+[k:0..n]C(k,m).

### Divisors and Factors

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

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

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

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

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

62. (above)|- (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.

63. ...Euclid's Algorithm...
Net

1. (above)|- (Eu1): hcf(n,n)=n.
2. (above)|- (Eu2): hcf(1,n)=1.
3. (above)|- (Eu3): hcf(0,n)=n.
4. (above)|- (Eu4): hcf(n,m)=hcf(m,n).
5. (above)|- (Eu5): for n>m, hcf(n,m)=hcf(n-m,m).

(End of Net)

For an example of Euclid's algorithm being used in rational numbers see [ rational.plg ] (Prolog).

### Linear Diophantine Equations

Solving an equation like: 10x+12y = 3 depends on the hcf(10,12).
64. (above)|- (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 [PettofrezzoByrkit85] or any other good book of elementary number theory.

### Multiples

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

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

69. (above)|- (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).
70. 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:

71. primes::= Primes~{1}. prime:Nat-->Nat::=primes;/|;>.
72. (above)|-{1,2,3,5,7} are Primes and (2,3,5,7,...)=prime.
73. (above)|- (N26): primes and |prime in Infinite. (primes)::= {p:2..*. for no d:2..p-1(d divides p).

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

74. For n:Nat, π(n)::= | (|prime & 1..n)| ,

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

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

79. (above)|- (Fundamental Theorem of Arithmetic): For n:Nat, one p:#primes(n=*p and <=(p)).
80. (above)|- (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) ).
81. For n:Nat, standard_factorization(n)::= the a:#Nat (n=*[i:dom(a)](prime(i)^a(i) ).
82. (above)|-12= 2^2 * 3^1 and standard_factorization(12)=(2,1)

[click here if you can fill this hole]

### Modular arithmetic

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

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

86. (above)|- (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:

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

88. (above)|- (N32): For p, ≡[p] = (= mod (_ mod p)).

For n,m,p, n ≡[p] m = (n = m wrt (_ mod p)) Use MONOID.

89. (above)|- (N33): for all p:Nat, ≡[p] in congruence(Nat0,+,0) & congruence(Nat,*,1).

90. (above)|- (Fermat's Little Theorem): for all prime p, Nat0 n ( p divides (n^p)-n).

Source: Fermat40

91. Carmichael_numbers::={p:Nat0~prime || for all n (p divides (n^p)-n)}.
92. (above)|- (N34): {561, 1105, 1729, 2465, 2821}==>Carmichael_numbers. [ CarmichaelNumber.html ]

93. (above)|- (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).

94. (above)|- (N35): for abf N, Card(Carmichael_numbers & [1..N)) > n^(2/7)

Source: Devlin92

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

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

### Totient Functions

97. φ::=Euler's totient Function,
98. For m:Nat0, φ(m)::=|{n:1..m || relatively_prime(n,m)}|,
99. (above)|- (N37): φ(1)=φ(2)=1,...
100. (above)|- (N38): For primes p, φ(p)=p-1.
101. (above)|- (N39): For primes p, Nat n, φ(p^n)=p^n-p^(n-1)=p^n*(1-1/p).
102. (above)|- (N40): for a:standard_factorization(n)( φ(n) =*[i:1..|a|](prime(i)^a(i) - prime(i)^(a(i)-1)) =n*[i:1..|a|]((1-1/prime(i)).

103. (above)|- (N41): for all n, +(φ o divisors(n))=n.
104. (above)|- (N42): For all n,m, φ(n*m)=φ(n)*φ(m).
105. (above)|- (Euler's Theorem): for Nat0 n,m, if hcf(m,n)=1 then n^φ(m) ≡[m] 1.
106. (above)|- (N43): For a,m:nat, if hcf(a,m)=1 then { x:nat || a*x ≡[m] b} ={ a^(φ(m)-1)b mod m}

107. (above)|- (N44): For a,b,m, |solutions{ x:0..m-1, a*x ≡[m] b }| =hcf(a,m) iff hcf(a,m) divides b.
108. (above)|- (N45): For a,b,m, |solutions{ x:0..m-1, a*x ≡[m] b }| =0 iff not hcf(a,m) divides b.
109. (above)|- (N46): For a,b,c,some solutions{ x,y:Nat0, a*x+b*y=c }iff hcf(a,b) divides c.
110. (above)|- (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.

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

113. (above)|- (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 ≡[m(i)] a(i))}. So define
114. representations(m)::= {a:(0..L)^(1..n) || for all i(a(i) in 0..m(i))},
115. R(m) :=representations(m),
116. represent(m)::=map[x](map[i](x mod m(i))),
117. \rho(m)::=represent(m).

118. |-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: HardyWright12 and

Source: PettofrezzoByrkit85

}=::Number_Theory.

. . . . . . . . . ( end of section Classical Number Theory) <<Contents | End>>

## Contiguity and Alignment of Integer Intervals

When IBM wanted to upgrade and reimplement its transaction processing system CICS (Customer Information C???? [click here if you can fill this 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: Woodcock89

3. contig::=img(..),
4. For m:Nat0, k:Nat,
5. floor(m,k)::=(m div k)*k,
6. ceiling(m,k)::=for f=floor(m,k){(true,f),(false,f+1)}(m=f),
7. aligned(k)::={S:@Nat||for a:S, f=floor(a,k)(f.*k are S)},
8. (above)|- (CA1): aligned(k) in sub_monoid(@Nat,|,{}).

## Real Numbers

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

2. Nonzero::=Real~{0},
3. 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},
4. a..b::={x:Real||a<=x<=b}. Avoid [a..b] because it is ambiguous.

(a..) ::={x:Real || a<x }, [a..) ::={x:Real || a<=x },

5. 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 },

6. 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]

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

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

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

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

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

12. (def)|-For x:Real,n:Int,
13. floor(x)<n iff x<n
14. and ceiling(x)<=n iff x<=n
15. and n<=floor(x) iff n<=x
16. and n<ceiling(x)iff n<x.

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

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

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

Binomial Theorem

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

... [click here if you can fill this hole]

}=::RealNumbers.

## Number Representations

### Fixed Point

1. FIXED_POINT::=
Net{
1. signed:: @=true if representation allows negative numbers,
2. unsigned::@=true if representation does not handle negative numbers.
3. |- (FP0): unsigned iff not signed.
4. |- (FP1): if normal then unsigned. -- indicates a default value.... assume unsigned if not known.

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

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

16. UNSIGNED_MODEL::=
Net{
1. digits::0..(length-1)->(0..(base-1)),
2. value::= (+[i:|/digits](digits(i)*(base^i)))/(base^scale)

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

}=::SIGNED_MODEL.

18. |-if unsigned then UNSIGNED_MODEL.
19. |-if signed then SIGNED_MODEL.

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

}=::FIXED_POINT.

2. 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.
1. |-
2. |-binary.
3. |-scale=1.
4. digits::0..(length-1)->0..1.
5. value::=(+[i:|/digits](digits(i)*(base^i))) - 2^(length-2)).

}=::TWOS_COMPLEMENT.

### Floating Point

3. FLOATING_POINT::=
Net{
-- always signed
1. m::Nat=given,mantissa_length.
2. b::Nat=given,base.
3. e::Nat=given,exponent_length.
4. f::Nat=given,offset.

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

}=::MODEL.

6. 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

4. 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: [ ncg_math.doc.html ] [ index.html ] and a page that converts decimal numbers into IEEE format [ IEEE-754.html ] from Ian Lasky.

I found pages 197 thru to 201 of the following a simple and comprehensive source of information:

• The Computer Professional's Quick Reference
• MS Vassiliou & JA Orenstein
• McGrawHill 1991
• ISBN 0-07-067211-1(paperback)

A peculiarity of the standard is that it defines two special values:

1. NaN::=Not a Number.
2. INF::=Infinity

Here is an example:

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

The rules get complex

1. |-if e=2047 and M<>0 then value=NaN
2. |-if e=2047 and M=0 then value=sign * INF
3. |-if 0<e<2047 and M=0 then value=sign * 2^(e-1023)*val("1." M)
4. |-if e=0 and M<>0 then value=sign * 2^(-1023)*val("0." M)
5. |-if e=0 and M=0 then value=sign * 0

They make more sense as a table:
Table
eMvalue
20470sign*INF
2047<>0NaN
00sign * 0
0<>0sign*2^(-1023)*val("0."M)
else<>0sign*2^(e-1023)*val("1."M)

(Close Table)

(End of Net)

. . . . . . . . . ( end of section Number Representations) <<Contents | End>>

## 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.

[click here if you can fill this hole]

### Generic Number Fields and Integral Domains.

[ math_45_Three_Operators.html ]

### Complex Numbers

[click here if you can fill this hole]

### Quaternions

[click here if you can fill this hole]

### Octonions and Cayley Numbers

[click here if you can fill this hole]

### Vectors & Matrices

[click here if you can fill this hole]

. . . . . . . . . ( end of section Other Number-like Systems) <<Contents | End>>

. . . . . . . . . ( end of section Numbers) <<Contents | End>>

## References

(Devlin92): Keith Devlin, There are Infinitely Many Carmichael Numbers, MAA Focus V12n4(Sep 1992)pp1,2
(Fermat40): Fermat 1640, Letter from Fermat to Frenicle (18 Oct 1640)
(Gause): Gause [click here if you can fill this hole]
(HardyWright12): Hardy & Wright, Theory of Numbers, 1912
(Hoare69): C A R Hoare, An Axiomatic Basis for Computer Programming, Comm ACM V12n10(Oct 1969)pp576..580+583
(PettofrezzoByrkit85): Anthony J Pettofrezzo & Donald R Byrkit , Elements of Number Theory, Orange 1985, Winter Fork Florida
(Woodcock89): Jim Woodcock, SIGSOFT Software Engineering Notes, ??CICS??, V??n?? (??? 1989) [click here if you can fill this hole]

# Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

# Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

10. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

# Glossary

11. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
12. given::reason="I've been told that...", used to describe a problem.
13. given::variable="I'll be given a value or object like this...", used to describe a problem.
14. goal::theorem="The result I'm trying to prove right now".
15. goal::variable="The value or object I'm trying to find or construct".
16. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
17. hyp::reason="I assumed this in my last Let/Case/Po/...".
18. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
19. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
20. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.