Real

This structure provides access to floating point numbers (traditionally called "reals"). The possible range of floating point numbers or the precision depend on the underlying system. If you must know exactly, consult the hand-coded implementation and get hold of a local C library guru.

Signature of Real

List of Import References :
See BOOL
See DENOTATION

SIGNATURE Real

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

The sort real

SORT real

Constants

Constants are not built-ins of the language. The most often occurring numbers are made available by the following definitions:

• Numbers from zero through thirtytwo

  FUN 0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 
        17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32: real
  
  

• Powers of two from the zeroth to the tenth power

  FUN 1 2 4 8 16 32 64 128 256 512 1024: real
  
  

• Powers of ten from the zeroth to the sixth power

  FUN 1 10 100 1000 10000 100000 1000000: real
  
  

• The smallest and biggest positive real number

  FUN min max: real
  
  

• The smallest value that makes 1+eps differ from 1

  FUN eps: real
  
  

• The constants pi (3.14...) and e (2.71...)

  FUN pi e            : real                  -- pi/e
  
  

All other numbers may be written down with the help of the function !. The denotation must match the regexp [+|-](0|1|..|9)*[.(0|1|..|9)*][e[+|-](0|1|..|9)+], otherwise the function is undefined.

FUN !               : denotation->real

Calculating with floating points

The basic operations

FUN + - * /         : real ** real -> real

Minimum and amximum of two numbers

FUN min max         : real ** real -> real

Negation (monadic minus)

FUN -     : real -> real

Absolute value

FUN abs  : real -> real

pow(x,y) yields the yth power of x

FUN pow  ^          : real ** real -> real
-- DFD x pow y <=> (x > 0) OR (x = 0 AND y > 0) OR (x < 0 AND y integer?)

Square root function

FUN sqrt         : real->real  --   DFD sqrt(x) <=> x >= 0

Exponential, natural and decimal logarithm

FUN exp      : real -> real
FUN ln log       : real -> real
-- DFD ln(x) <=> x > 0     DFD log(x) <=> x > 0

The next bigger resp. smaller real integer number

FUN ceil floor: real -> real
                      -- ceil(x)  == min{n in Int|n >=x}
                      -- floor(x) == max{n in Int|n <=x}

The sign function: -1 for negative values, +1 for positive, 0 for zero

FUN sign: real -> real

Trigonometric functions

Basic trigonometric functions (input in radian)

FUN sin cos tan 

Arcus functions (input in radian)

    arcsin                    
    arccos 
    arctan          : real->real
    arctan2     : real**real->real

convert radians to degrees

FUN deg: real -> real

convert degrees to radians

FUN rad: real -> real

-- DFD arcsin(x) <=> x >= -(1) AND x <= 1
-- DFD arccos(x) <=> x >= -(1) AND x <= 1
                      
-- DFD arcsin(x) => (arcsin(x) = y <=> 
--                   sin(y) = x AND y >= -(pi/2) AND y <= pi/2)
-- DFD arccos(x) => (arccos(x) = y <=> 
--                   cos(y) = x AND y >= 0 AND y <= pi
-- arctan(x) = y <=> tan(y) = x AND y >= -(pi/2) AND y <= pi/2)
-- arctan(y,x) = z <=> tan(y/x) = z AND z >= -(pi) AND z <= pi
    

Hyperbolic trigonometric functions

FUN sinh cosh tanh  : real->real

Tests on real numbers

positive / negative / zero number ?

FUN pos? neg? zero? : real->bool

comparisons

FUN <= = >= < > |=  : real**real->bool

Bracketings

/$ BRACKET RIGHT [+,-  : real ** real -> real] [*,/] $/
/$ BRACKET LEFT [*,/] [+,-  : real ** real -> real] $/
/$ BRACKET LEFT [+,-  : real ** real -> real] [+,-  : real ** real -> real] $/
/$ BRACKET LEFT [*,/] [*,/] $/

next node: IntConv,
prev node: Nat,
up to node: Subsystem Numbers