RIA - Rational Interval Arithmetics¶
The domain ``RationalInterval`` (abbrev. ``RIA``) implements Rational Interval Arithmetics. We were inspired by the article Guaranteed Proofs Using Interval Arithmetic. For basic definitions see section 2.1 therein.
Basic Interval Operations¶
"+" : (%,%) -> %
"-" : (%,%) -> %
"*" : (%,%) -> %
"/" : (%,%) -> %
"^" : (%,I) -> %
"-" : % -> %
abs : % -> %
elt : (Q, %) -> %
coerce: % -> OutputForm
coerce: List Q -> %
coerce: Float -> %
coerce: DF -> %
concise : % -> OutputForm
Constructors and Query Functions¶
mki : (Q,Q) -> %
lb : % -> Q
ub : % -> Q
mid : % -> Q
len : % -> Q
frep : % -> OF
These functions and operations are explained in detail below. Note that
Q means the rationals (\(\mathbb{Q}\)).
Q ==> Fraction Integer
Type: Void
In order to use the library we have to load it:
)lib RIA
RationalInterval is now explicitly exposed in frame initial
RationalInterval will be automatically loaded when needed from
/home/kfp/Development/physqty/Untitled Folder/RIA.NRLIB/RIA
Construction of Intervals¶
The first method to construct a rational interval is to use the
constructor function mki which expects two arguments: the lower
bound lb and the upper bound ub returning an object of type
RationalInterval.
I:=mki(1/2,2/3)
Warning: HyperTeX macro table not found
1 2
[-,-]
2 3
Type: RationalInterval
Another method is to coerce a list [lb,ub], where
\(lb \leq ub\in\mathbb{Q}\).
I2:=[1/2,2/3]::RIA
1 2
[-,-]
2 3
Type: RationalInterval
Note that the arguments must be rational numbers, failing which produces an error:
I3:=[0.5,0.6666]::RIA
Cannot convert the value from type List(Float) to RationalInterval .
error
However, we can coerce the arguments of course:
I3:=[0.5::Q,0.6666::Q]::RIA
1 3333
[-,----]
2 5000
Type: RationalInterval
So, as we can see, floating point numbers are converted to rationals.
Query functions¶
Objects of type RationalInterval are not lists, therefore the usual
way to access elements will not work. There are special query functions
expecting an interval as argument.
Length of I, i.e. \(ub-lb\)¶
len I
1
-
6
Type: Fraction(Integer)
The function frep gives a floating point representation of the
interval. This function merely is for use with the PQTY package, so
use with care.
frep I
0.5833333333_3333333333 ± 0.0833333333_3333333333_3
Type: OutputForm
digits(8)
frep I
20
Type: PositiveInteger
0.58333333 ± 0.083333333
Type: OutputForm
Intervals can be added, multiplied, scaled and so on. To each operation an example is given below. For the sake of clarity we use integer rationals:
A:=[-1::Q,2]::RIA
B:=[5::Q,8]::RIA
[- 1,2]
Type: RationalInterval
[5,8]
Type: RationalInterval
A+B
[4,10]
Type: RationalInterval
A-B
[- 9,- 3]
Type: RationalInterval
-B
[- 8,- 5]
Type: RationalInterval
-- so A+(-B) should equal A-B
A+(-B)
[- 9,- 3]
Type: RationalInterval
A*B
[- 8,16]
Type: RationalInterval
A/B
1 2
[- -,-]
5 5
Type: RationalInterval
B^2
[25,64]
Type: RationalInterval
-- expecting an error
A^2
TYPE-ERROR:
#<TYPE-ERROR expected-type: CONS datum: NIL>
-- however: A^3
A^3
[- 1,8]
Type: RationalInterval
B^3
[125,512]
Type: RationalInterval
It is obvious that intervals containing 0 properly cannot
exponentiated by even integers. Also acting as denominator is usually
not possible.
abs A
[0,2]
Type: RationalInterval
abs B
[5,8]
Type: RationalInterval
abs (A^5)
[0,32]
Type: RationalInterval
The operation ``elt`` means scaling the inteval by a rational number:
(2/3) A
2 4
[- -,-]
3 3
Type: RationalInterval
5 B
[25,40]
Type: RationalInterval
3 (A+B)
[12,30]
Type: RationalInterval
digits(10)
(12.45666666::Q) A
8
Type: PositiveInteger
6254156 12508312
[- -------,--------]
502073 502073
Type: RationalInterval
There are coercions from Float and DF (DoubleFloat) to type
RIA which are not very useful in this context but are useful in
other packages:
Coercions and pitfalls¶
-- Attention: Float type depends on precision, digits ...
1.234567::RIA
50737 50737
[-----,-----]
41097 41097
Type: RationalInterval
digits(10)
1.234567::DoubleFloat::RIA
10
Type: PositiveInteger
118164173 118164173
[---------,---------]
95713050 95713050
Type: RationalInterval
digits(20) -- note difference
1.234567::DoubleFloat::RIA
10
Type: PositiveInteger
1234567 1234567
[-------,-------]
1000000 1000000
Type: RationalInterval
r:DoubleFloat:=%pi/2
1.5707963267948966
Type: DoubleFloat
r::RIA
80143857 80143857
[--------,--------]
51021164 51021164
Type: RationalInterval
Show RIA¶
)show RIA
RationalInterval is a domain constructor
Abbreviation for RationalInterval is RIA
This constructor is exposed in this frame.
------------------------------- Operations --------------------------------
?*? : (%,%) -> % ?+? : (%,%) -> %
-? : % -> % ?-? : (%,%) -> %
?/? : (%,%) -> % ?^? : (%,Integer) -> %
abs : % -> % coerce : DecimalExpansion -> %
coerce : DoubleFloat -> % coerce : Float -> %
coerce : % -> OutputForm concise : % -> OutputForm
convert : % -> String elt : (Fraction(Integer),%) -> %
frep : % -> OutputForm lb : % -> Fraction(Integer)
len : % -> Fraction(Integer) mid : % -> Fraction(Integer)
tm_frep : % -> OutputForm ub : % -> Fraction(Integer)
coerce : List(Fraction(Integer)) -> %
mki : (Fraction(Integer),Fraction(Integer)) -> %
Decimal Expansions¶
While Float implements arbitrary precision floating point
arithmetic, DoubleFloat is intended to make accessible hardware
floating point arithmetic, either native double precision, or IEEE.
Many operations are not expected to be fully accurate when using
DoubleFloat. In particular, sin and cos will lose all
precision for large arguments. The Float domain provides an
alternative to the DoubleFloat domain. It provides an arbitrary
precision model of floating point arithmetic. This means that accuracy
problems are eliminated by increasing the working precision where
necessary. Float provides some special functions such as erf,
the error function in addition to the elementary functions. The
disadvantage of Float is that it is much more expensive than small
floats when the latter can be used. Note that for big numbers
DoubleFloat may overflow!
Another useful type is DecimalExpansion: allows rational numbers
to be presented as repeating decimal expansions.
DE ==> DecimalExpansion
Type: Void
1/3::DE
_
0.3
Type: DecimalExpansion
d:=1234567/100000::DE
12.34567
Type: DecimalExpansion
d::RIA
1234567 1234567
[-------,-------]
100000 100000
Type: RationalInterval
d::Float
d::DoubleFloat
12.34567
Type: Float
12.34567
Type: DoubleFloat