RE: [Camllist] Efficient and canonical set representation?
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20031117 (17:04) 
From:  Diego Olivier Fernandez Pons <Diego.FERNANDEZ_PONS@e...> 
Subject:  Re: [Camllist] Rounding mode 
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 floatingpoint 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 32bit to 64bit and back, performing a 32bit arithmetic operation on such 32bit numbers can produce a different result than performing a 64bit arithmetic operation on their 64bit 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 camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners