From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA17682; Mon, 17 Nov 2003 18:04:31 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA17422 for ; Mon, 17 Nov 2003 18:04:30 +0100 (MET) Received: from shiva.jussieu.fr (shiva.jussieu.fr [134.157.0.129]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id hAHH4T100200 for ; Mon, 17 Nov 2003 18:04:29 +0100 (MET) Received: from ibm3.cicrp.jussieu.fr (ibm3.cicrp.jussieu.fr [134.157.15.3]) by shiva.jussieu.fr (8.12.10/jtpda-5.4) with ESMTP id hAHH4SqY010591 ; Mon, 17 Nov 2003 18:04:28 +0100 (CET) Received: from ibm1.cicrp.jussieu.fr (ibm1.cicrp.jussieu.fr [134.157.15.1]) by ibm3.cicrp.jussieu.fr (8.8.8/jtpda/mob-V8) with ESMTP id SAA49884 ; Mon, 17 Nov 2003 18:03:32 +0100 Received: from localhost (fernande@localhost) by ibm1.cicrp.jussieu.fr (8.8.8/jtpda/mob-v8) with ESMTP id SAA2555964 ; Mon, 17 Nov 2003 18:03:29 +0100 Date: Mon, 17 Nov 2003 18:03:28 +0100 (NFT) From: Diego Olivier Fernandez Pons To: bhurt@spnz.org cc: caml-list@inria.fr Subject: Re: [Caml-list] Rounding mode In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Antivirus: scanned by sophie at shiva.jussieu.fr X-Loop: caml-list@inria.fr X-Spam: no; 0.00; pons:01 pons:01 etu:99 caml-list:01 rounding:01 discusion:99 arithmetics:01 topological:01 subtyping:01 equalities:01 uniqueness:01 forall:01 topological:01 arithmetics:01 infinities:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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