[FOM] Question on Axioms for FP-Arithmetic
a_mani_sc_gs at yahoo.co.in
Sun Sep 14 13:23:45 EDT 2008
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?
Member, Cal. Math. Soc
More information about the FOM