.Open 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 .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$HardyWright12, $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 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>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$Fermat40 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 $Devlin92 ()|-(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 representations(m) ::= {a:(0..L)^(1..n) || for all i(a(i) in 0..m(i))}, R(m) :=representations(m), represent(m)::=map[x](map[i](x mod m(i))), \rho(m) ::=represent(m). |- 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. .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$Woodcock89 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||ax }, [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)(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::Nat=given,mantissa_length. b::Nat=given,base. e::Nat=given,exponent_length. f::Nat=given,offset. 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 00 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 .Close Numbers .Bibliography (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 .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) .Hole