Numbers

introduces: natural , positive-integer , successor _ , 0 .
0 : natural .
successor _ :: natural -> positive-integer (total, injective) . 
(1) natural = 0 | positive-integer (disjoint) .
(2) positive-integer = successor natural .

closed .

Back to the beginning.

1.2 Specifics

introduces:  1 , 2 , 3 , 4 , 5 , 6 , 7 , 8 , 9 , 
	       _0 , _1 , _2 , _3 , _4 , _5 , _6 , _7 , _8 , _9 ,
	       sum _ , product _ , exponent _ , integer-quotient _ , integer-remainder _ . 

includes:   Instant/Total Order ( natural for s , _ is _ , _ is less than _ ) .

needs:	    Tuples/Basics .  natural <= component .
1 , 2 , 3 , 4 , 5 , 6 , 7 , 8 , 9 : natural .
_0 , _1 , _2 , _3 , _4 , _5 , _6 , _7 , _8 , _9 :: natural -> natural (total) .
sum _ :: natural^* -> natural (total, associative, commutative, unit is 0) . 
product _ :: natural^* -> natural (total, associative, commutative, unit is 1). 
exponent _ :: (natural, natural) -> natural (total). 
integer-quotient _ :: (natural, natural) -> natural (partial) . 
integer-remainder _ :: (natural, natural) -> natural (partial) .
(1) 1 = successor 0 ; 2 = successor 1 ; 3 = successor 2 ;4 = successor 3 ; 
	5 = successor 4 ; 6 = successor 5 ; 7 = successor 6 ;8 = successor 7 ;
	9 = successor 8 ; 10 = successor 9 . 
(2) (n:natural)⁰ = product (n, 10) ;
     	(n:natural)¹ = sum (product (n, 10), 1) ;
     	...
     	(n:natural)⁹ = sum (product (n, 10), 9) .
(3) sum _ :: natural^*, positive-integer -> positive-integer ; 
     	sum (n:natural, 1) = successor n .
(4) product _ :: positive-integer^* -> positive-integer ; 
     	product (n:natural, 0) = 0 ;
     	product (m:natural, successor n:natural) = sum (m, product (m, n)) .
(5) exponent (m:natural, 0) = 1 ;
     	exponent (m:natural, successor n:natural) = product (m, exponent (m, n)) .
(6) integer-quotient (n:natural, 0) = nothing ;
     	integer-remainder (n:natural, 0) = nothing .
(7) m is less than p = true ;  m, n : natural ;  p : positive-integer =>
       (1) integer-quotient (sum (product (n, p), m), p) = n ;
       (2) integer-remainder (sum (product (n, p), m), p) = m .
(8) 0 is p:positive-integer = false ;
     	successor m:natural is successor n:natural = m is n .
(9) 0 is less than p:positive-integer = true ;
     	n:natural is less than 0 = false ;
     	successor m:natural is less than successor n:natural = m is less than n .
(10)natural [min m:natural] = m | natural [min successor m] (disjoint) ;
     	natural [max successor m:natural] = natural [max m] | successor m (disjoint) .
(11)natural [min 0] = natural ; natural [max 0] = 0 .

Basics | Specifics

2.1. Basics

introduces:  integer , negative-integer , nonzero-integer , predecessor _ . 
successor _   :: integer -> integer (total, injective) . 
predecessor _ :: integer -> integer (total, injective) . 
(1) integer = 0 | nonzero-integer (disjoint) .
(2) nonzero-integer = positive-integer | negative-integer (disjoint) .
(3) successor _ :: negative-integer -> 0|negative-integer . 
(4) predecessor _ :: 0|negative-integer -> negative-integer, positive-integer -> natural . 
(5) successor predecessor i:integer = i ; predecessor successor i:integer = i .

closed .

Back to the beginning.

2.2. Specifics

introduces: negation _ , absolute _ , difference _ . 

includes:   Instant/Total Order ( integer for s , _ is _ , _ is less than _ ) .

needs:	    Tuples/Basics .   integer <= component .
negation _         :: integer -> integer (total) . 
absolute _         :: integer -> natural (total) . 
sum _              :: integer^* -> integer (total, associative, commutative, unit is 0) . 
difference _       :: (integer, integer) -> integer (total) . 
product _          :: integer^* -> integer (total, associative, commutative, unit is 1) . 
exponent _         :: (integer, natural) -> integer (total) . 
integer-quotient _ :: (integer, integer) -> integer (partial) .
integer-remainder_ :: (integer, integer) -> integer (partial) . 
(1) negation 0 = 0 ;
     	negation successor i:integer = predecessor negation i ;
     	negation negation i:integer = i ;
     	negation positive-integer = negative-integer .
(2) absolute n:natural = n ; absolute negation n:natural = n .
(3) sum (i:integer, 1) = successor i ; 
     	sum (i:integer, negation 1) = predecessor i .
(4) difference (i:integer, j:integer) = sum (i, negation j) .
(5) product (0, i:integer) = 0 ;
     	product (negation i:integer, j:integer) = negation product (i, j) ;
     	product (sum (i:integer, j:integer), k:integer) =
	   	sum (product (i, k), product (j,k)) .
(6) exponent (negation i:integer, product (2, n:natural)) =
 	   	exponent (i, product (2, n)) .
(7) exponent (negation i:integer, successor product (2, n:natural)) =
 	   	negation exponent (i, successor product (2, n)) .
(8) integer-quotient (i:integer, 0) = nothing ;
     	integer-quotient (negation i:integer, j:integer) = 
	   	negation integer-quotient (i, j) ;
     	integer-quotient (i:integer, negation j:integer) = 
	   	negation integer-quotient (i, j) .
(9) integer-remainder (i:integer, 0) = nothing ;
     	integer-remainder (negation i:integer, j:integer) = 
	   	negation integer-remainder (i, j) ;
     	integer-remainder (i:integer, negation j:integer) = integer-remainder (i, j) .
(10)i, j : integer => sum (product (integer-quotient (i, j), j), integer-remainder (i, j)) = i .
(11)m:negative-integer is 0 = false ;
     	negation i:integer is negation j:integer = i is j ;
     	m:negative-integer is p:positive-integer = false ;
     	sum (i:integer, j:integer) is sum (i, k:integer) = j is k .
(12)m:negative-integer is less than 0 = true ;
     	negation i:integer is less than negation j:integer = j is less than i ;
     	sum (i:integer, j:integer) is less than sum (i, k:integer) = j is less than k .
(13)integer [min m:integer] = m | integer [min successor m] (disjoint) ;
     	integer [max successor m:integer] = integer [max m] | successor m (disjoint) .

Basics | Specifics

3.1. Basics

introduces: rational , nonzero-rational , positive-rational , negative-rational , quotient _ .
quotient _ :: integer, nonzero-integer -> rational (total) . 
(1) rational = 0 | nonzero-rational (disjoint) .
(2) nonzero-rational = positive-rational | negative-rational (disjoint).
(3) positive-integer <= positive-rational ; negative-integer <= negative-rational .
(4) quotient _ :: positive-integer, positive-integer ->o positive-rational,
		  negative-integer, positive-integer -> negative-rational, integer, 0 -> nothing . 
(5) quotient (negation i:integer, j:nonzero-integer) = negation quotient (i, j) .
(6) quotient (i:integer, negation j:nonzero-integer) = negation quotient (i, j) .
(7) quotient (product (i:nonzero-integer, j:integer), product (i, k:integer)) = 
	   quotient (j, k) .
(8) quotient (i:integer, 1) = i .  quotient (0, i:nonzero-integer) = 0 .

closed .

Back to the beginning.
3.2. Specifics
introduces: truncation _ , fraction _ . includes: Instant/Total Order ( rational for s , _ is _ , _ is less than _ ) . needs: Tuples/Basics . rational <= component .
quotient _ :: rational, nonzero-rational -> rational (total) .
truncation _ :: rational -> integer (total) .
fraction _ :: rational -> rational (total) .
negation _ :: nonzero-rational -> nonzero-rational (total) .
absolute _ :: nonzero-rational -> positive-rational (total) .
sum _ :: rational^* -> rational (total, associative, commutative, unit is 0) .
difference _ :: (rational, rational) -> rational (total) .
product _ :: rational^* -> rational (total, associative, commutative, unit is 1) .
exponent _ :: (rational, integer) -> rational (partial) .
(1) quotient _ :: positive-rational, positive-rational -> positive-rational, negative-rational, positive-rational -> negative-rational, rational, 0 -> nothing . (2) truncation quotient (i:integer, j:nonzero-integer) = integer-quotient (i, j) . (3) fraction quotient (i:integer, j:nonzero-integer) = quotient (integer-remainder (i, j), j) . (4) negation quotient (r:rational, n:nonzero-rational) = quotient (negation r, n) . (5) absolute p:positive-rational = p ; absolute n:negative-rational = negation n . (6) sum (r:rational, quotient (q:rational, n:nonzero-rational)) = quotient (sum (product (r, n), q), n) . (7) difference (q:rational, r:rational) = sum (q, negation r) . (8) product (r:rational, quotient (q:rational, n:nonzero-rational)) = quotient (product (r, q), n) . (9) exponent (quotient (q:rational, n:nonzero-rational), i:integer) = quotient (exponent (q, i), exponent(n, i)) ; exponent (quotient (q:rational, n:nonzero-rational), negation p:positive-integer) = exponent (quotient (n, q), p) . (10)quotient (r:rational, quotient (q:nonzero-rational, n:nonzero-rational)) = quotient (product (r, n), q) ; quotient (quotient (q:rational, n:nonzero-rational), r:nonzero-rational) = quotient (q, product (n, r)) . (11)product (p:nonzero-rational, q:rational) is product (p, r:rational) = q is r . (12)product (p:positive-rational, q:rational) is less than product (p, r:rational) = q is less than r .

Back to the beginning.
4. Approximations
Generics | Basics
4.1. Generics
introduces: approximation , min-approximation , max-approximation .
approximation <= rational .
min-approximation, max-approximation : approximation .
(1) approximation [min min-approximation] [max max-approximation] = approximation . open .

Back to the beginning.
4.2. Basics
introduces: interval_ , approximately _ .
interval _ :: rational -> rational (strict) .
approximately _ :: rational -> rational (strict, linear) .

The sort interval r is the smallest closed subsort of rational that includes the sort r, whereas approximately r is an interval whose bounds are of sort approximation, or nothing when r is entirely outside the interval from min-approximation to max-approximation.

(1) r <= rational => r <= interval r . (2) s, t : r <= rational => rational [min s] [max t] <= interval r . (3) x : rational => x : approximately x . (4) x : rational => interval approximately x = approximately x . (5) x : approximation => approximately x = x . (6) x : interval y ; y => approximation => approximately x <= interval y . (7) x is greater than max-approximation = true => approximately x:rational = nothing . (8) x is less than min-approximation = true => approximately x:rational = nothing .

Back to the beginning.

WebAni | Ani | RAT | AG | Actions | People | Action Notation | Data Notation

[Created by Jin Jin Yi and Ana Carla Santos. Last modified at 21 Dec 1997 by Jin Jing Yi]

Naturals | Integers | Rationals

Basics | Specifics

Basics | Specifics

Basics | Specifics

Generics | Basics