Re: [Caml-list] Rounding mode

[Diego Olivier Fernandez Pons <Diego.FERNANDEZ_PONS@etu.upmc.fr>]

    Bonjour,

> Actually, I wonder if type systems could be extended to detect
> numerical instabilities ?

I forgot to answer to that question...

There was a discusion on the types forum

http://www.cis.upenn.edu/~bcpierce/types/archives/current/msg01419.html

The main problem could be stated as "what properties do you want to
guarantee for your arithmetics" : algebraic properties ? topological
properties ? subtyping properties ?

Several examples violated algebraic properties were given by Tim
Sweeney in his post (Leibniz equalities, uniqueness of the zero,
forall x. x = x, etc.)

Several examples of topological properties were given by Joe Darcy :

- 'compactification' "IEEE 754 floating-point arithmetics is a
complete system; that is for all inputs, every arithmetic operation in
the standard has a defined IEEE 754 value as a result [...] There are
two ways to add infinite values to the field of real numbers : 1. a
single infinity 2. two affine infinities ..." Actually, there are much
more ways of compactifying a locally compact space and
'compactification' hasn't the same mathematical meaning than
'completion' or 'inner operations' but that is not the problem here.

- funny theorems on limits and series like 'if the general term of a
serie converges, then the whole serie converges'

The subtyping question seems to be related to commutative diagrams :
we want the surjection (e.g. 64 -> 32 bits) to commute with arithmetic
operations.

"Though one can losslessly convert from 32-bit to 64-bit and back,
performing a 32-bit arithmetic operation on such 32-bit numbers can
produce a different result than performing a 64-bit arithmetic
operation on their 64-bit extensions, and then converting back."


We surely can answer to some of these question : with respect to group
properties there is a well known theorem 'any subgroup of R either is
dense or has the form aZ'. In both cases they are infinite. Therefore
you cannot expect any floting points arithmetic to keep all group
properties.

For the typing question, we can give part of an answer :

(I use stochastic arithmetic because interval arithmetic is usually
too pessimistic. I am not a statistician but they all seem to agree
with the fact that in many cases being 'almost sure' is much more easy
than being 'absolutely sure')

Cestac allows you to compute the 'meaningful part' of a computation
(in a statistical sense). Then you can see a result like a couple
float * int where the integers gives the number of exact digits.

If you see a coercion like a surjection (f, n) -> (f, m) with m < n
(which just means that you loose accuracy) then :

(i) We can construct a 'clean' family of subtyping operators that is
such as there is at least one surjection that commutes with your
computations (which one of course depends on the stability of the
given computations).

(ii) We can construct a 'type system' which ensures dynamically that
every result is 'well typed'. Actually, this is exactly what CADNA
does but as a library.


        Diego Olivier


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners