[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng Dept] / [R J Botting] / [ MATHS ] / math_42_Numbers
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Thu Feb 21 14:47:25 PST 2008

Opening Microsoft files (winzip, word, excel, powerpoint) on this page may require you to download a special viewer. Or you can download and save the files and use your preferred office applications to view and edit them.

Contents

    Numbers

      Hoare's Axioms

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

      Hoare69

      1. C A R Hoare
      2. An Axiomatic Basis for Computer Programming
      3. Comm ACM V12n10(Oct 69)pp576..580+583

      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.


        (Hoare Operations):

      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. |-HOARE and finite_arithmetic.
      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

        Hardy & Wright, 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. |-ORDER.
        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 [socket symbol] 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). Fermat 1640, Letter from Fermat to Frenicle 18th October 1640

        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) Devlin 92, Kieth Devlin, There are Infinitely Many Carmichael Numbers, MAA Focus V12n4(Sep 92)pp1,2


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


        116. |-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)

          Hardy & Wright 1912 and Pettofrezzo & Byrkit 1985


        }=::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 [socket symbol] 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 Woodcock 89

    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 [socket symbol] 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. |-FIXED_POINT.
        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::=mantissa_length::Nat.
        2. b::=base::Nat.
        3. e::=exponent_length::Nat.
        4. f::=offset::Nat.

        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:
            eMvalue
            20470sign*INF
            2047<>0NaN
            00sign * 0
            0<>0sign*2^(-1023)*val("0."M)
            else<>0sign*2^(e-1023)*val("1."M)

          (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 [socket symbol] if you can fill this hole]

          Generic Number Fields and Integral Domains.

          [ math_45_Three_Operators.html ]

          Complex Numbers

           [click here [socket symbol] if you can fill this hole]

          Quaternions

           [click here [socket symbol] if you can fill this hole]

          Octonions and Cayley Numbers

           [click here [socket symbol] if you can fill this hole]

          Vectors & Matrices

          See [ math_45_Three_Operators.html#Vector Spaces ]

          [click here [socket symbol] if you can fill this hole]

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

        Glossary

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

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

      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 = Net{radius:Positive Real, center:Point}.

      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.

    End