[FOM] Question on Axioms for FP-Arithmetic

[A. Mani]

I see that almost all of the formal presentations of 
floating point arithmetic (FPA) are geared towards
 implementation specific formal verification. These 
are usually not 'logic-friendly'.

Suppose we define FP numbers in the following way:
Let T be a tolerance relation on the set of rationals Q, 
that is defined via 
(x,y)\in T iff |x - y|< e (for a fixed rational e).
Then the blocks of T form an initial set of FP numbers. 

A block B of T is a subset of Q, that satisfies 
the property B^2 \subseteq T and there is no C s.t 
B \subset C. and C has the same property (C^2 \subseteq T). 
In other words, B is maximal w.r.t B^2 \subseteq T. Here the 
blocks will look like intervals of the form (a-e/2, a+e/2), -, + being 
usual arithmetical operations. 

(Tolerances are fully determined by their set of blocks - for this result see 
(for example):Chajda, Ivan 'Algebraic Theory of Tolerances' 
Olomouc Univ press, 1991)

For defining FP operations like +, -, \cdot and \frac on these we can 
make use of an additional set of tolerances on Q \cap [-n,n] 
for some n. It is possible to avoid explicit chop etc this way.

Finally it is possible to model FPA by partial algebras 
satisfying some quasi equations.  

Are there better methods?


Best

A. Mani
 
 

 
-- 
A. Mani
Member, Cal. Math. Soc