RE: [Caml-list] Are you sure the new "=" of 3.08 is good ?

RE: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Harrison, John R]

| I spend one complete day to adapt Phox (my theorem prover) to 3.08
| because the new = does not check first physical equality.

If that's true, it would probably be bad news for the efficiency of my
theorem prover (HOL Light) as well, though I haven't run any actual
comparisons. (I have it running under 3.06, 3.07 and 3.08 on different
machines --- only the camlp4 part was different each time.)

| sin x with x > 10e100 gives a value which is certainly wrong since you

| can not compute the modulo 2 pi for such a big number.
| sin x should give nan when |x| is too big.

You can perfectly well compute it, and the general consensus among the
floating-point community is that trig functions should do the best they
reasonably can even on huge arguments. Techniques for doing this kind
of reduction reasonably efficiently have been known for at least 20
years, e.g.

@ARTICLE{payne-hanek,                                               
        author          = "M. Payne and R. Hanek",
        title           = "Radian Reduction for Trigonometric
Functions",
        journal         = "SIGNUM Newsletter",   
        year            = 1983,              
        volume          = 18,                     
        number          = 1,          
        pages           = "19--24"}               

Taking the sin of large numbers may indeed indicate bad code, but so may
lots of other eccentric uses of library functions.

John.

-------------------
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

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1006 bytes --]


> You can perfectly well compute it, and the general consensus among the
> floating-point community is that trig functions should do the best they
> reasonably can even on huge arguments. Techniques for doing this kind
> of reduction reasonably efficiently have been known for at least 20
> years, e.g.

Yes you can perfectly compute sin 10e100.

But if x is the result of any computation (with rounding error), and x 
is huge, sin x may be any value between -1 and 1. So the best value from 
sin x is either 0 (your possible error is minimum) or nan.


-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[David Brown]

On Fri, Oct 08, 2004 at 07:49:17AM +0200, Christophe Raffalli wrote:
> 
> >You can perfectly well compute it, and the general consensus among the
> >floating-point community is that trig functions should do the best they
> >reasonably can even on huge arguments. Techniques for doing this kind
> >of reduction reasonably efficiently have been known for at least 20
> >years, e.g.
> 
> Yes you can perfectly compute sin 10e100.
> 
> But if x is the result of any computation (with rounding error), and x 
> is huge, sin x may be any value between -1 and 1. So the best value from 
> sin x is either 0 (your possible error is minimum) or nan.

sin 10e100 (1e101) isn't meaningful with any kind of floating point
precision I'm aware of.  Any numerical process that is attempting to take
the sin of a value like this has long since lost any meaningful digits out
of the number.

Dave

-------------------
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

RE: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Harrison, John R]

| As I said in an earlier post, you can do
| 
|   let (=?) x y = (Pervasives.compare x y = 0)
| 
| and use =? instead of = in places where you need the "early stop"
| behaviour.

OK. I wanted to be sure this was a recommended solution, not just
something that happens to work at the moment.

| Of course, if the speed of equality is critical, you can also define
| your own comparison functions for the types of interest, or even (as
| Damien suggested) implement hash-consing.

In fact, the key function is an alpha-conversion test on
name-carrying lambda-terms. Since it's almost always expected to
succeed with full equality after a shallow comparison, I now do an
equality test first to get the early-out behaviour. I can just
change it to put an "==" into the main recursion when it hasn't
gone through any lambdas.

John.

-------------------
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

RE: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Harrison, John R]

| What I did in my soon-to-be-released automatic prover, following
| advice from Pierre Weis, was to hash-cons all the terms used by the
| program.  Now I only need to use pointer equality: if the pointers
| are not the same then I know the terms are not the same.  The speedup
| was a factor of 100 because my program does lots of comparisons and
| hashing of terms.

Yes, it might well be worth looking at that again. I tried it once
in CAML Light and the results were disappointing. But one reason was
that something like weak pointers either didn't exist or I didn't
know about them, so my hash tables rendered some ephemeral stuff 
non-collectible.

I'll look forward to the release of your prover!

John.

-------------------
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

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Xavier Leroy]

> For LCF-style theorem provers, I think it's quite important that when
> comparing terms (or similar tree structures) for equality, there should
> be a quick "yes" when two high-level subgraphs are pointer eq. [...]
> I guess like Christophe Raffalli I had just assumed this would be
> the case based on long experience with ML-family languages, rather than
> through any explicit discussion in the documentation.

I agree the behaviour your describe (x == y implies x = y) is very
reasonable.  Unfortunately, nan <> nan is also very reasonable, at
least if you believe in IEEE floats, and you cannot have both...

We agonized a long time on this issue before settling on the current
compromise: "=" is compatible with IEEE float equality, and
Pervasives.compare implements the behaviour you expect (early stop if ==).

> Can you clarify what we need to do in order to guarantee this
> behaviour?

As I said in an earlier post, you can do

  let (=?) x y = (Pervasives.compare x y = 0)

and use =? instead of = in places where you need the "early stop" behaviour.

I advise against Damien's suggestion of defining

  let (=) x y = (Pervasives.compare x y = 0)

because the predefined "=" operator is known to the compiler and is
type-specialized to much more efficient code when comparing ints,
floats or strings.  No such type specialization takes place when "="
is defined in terms of Pervasives.compare.

Of course, if the speed of equality is critical, you can also define
your own comparison functions for the types of interest, or even (as
Damien suggested) implement hash-consing.

Hope this clarifies the issue.

- Xavier Leroy

-------------------
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

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Damien Doligez]

On Oct 8, 2004, at 18:35, Harrison, John R wrote:

> For LCF-style theorem provers, I think it's quite important that when
> comparing terms (or similar tree structures) for equality, there should
> be a quick "yes" when two high-level subgraphs are pointer eq. For
> example,

What I did in my soon-to-be-released automatic prover, following
advice from Pierre Weis, was to hash-cons all the terms used by the
program.  Now I only need to use pointer equality: if the pointers
are not the same then I know the terms are not the same.  The speedup
was a factor of 100 because my program does lots of comparisons and
hashing of terms.

-- Damien

-------------------
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

RE: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Harrison, John R]

| > I was assuming two things about equal:
| > - scan of block from left to right
| > - a test on adress equality on pointer before follwing the pointer 
| > (which is now wrong in 3.08).
| 
| That was true of the old implementation, but has never been
guaranteed.

For LCF-style theorem provers, I think it's quite important that when
comparing terms (or similar tree structures) for equality, there should
be a quick "yes" when two high-level subgraphs are pointer eq. For
example,

  Constr(small_1,big) = Constr(small_2,big)

(where small_1 = small_2) should return "true" without recursing down
"big". This often comes up when generic theorems are instantiated and
one then checks that the instantiation does make certain terms match
up.

I guess like Christophe Raffalli I had just assumed this would be
the case based on long experience with ML-family languages, rather than
through any explicit discussion in the documentation. Can you clarify
what we need to do in order to guarantee this behaviour?

John.

-------------------
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

RE: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Harrison, John R]

| But if x is the result of any computation (with rounding error), and x

| is huge, sin x may be any value between -1 and 1. So the best value
from 
| sin x is either 0 (your possible error is minimum) or nan.

The job of the library function should be to solve the simple
mathematical
task of returning an accurate sin, not indulge in a speculative critique
of
the user's error analysis.

Sure, the input is most likely either a previously rounded result or
some
inexact physical measurement. But it *might* be a precise value. Or the
result may be used in such a way that the error will not be an issue,
e.g.
if one subsequently does something like "1 + sin(x)/x". Returning NaN
would
force the user to indulge in many tedious checks instead of simply using
the straightforward algorithm.

John.

-------------------
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

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Xavier Leroy]

> I spend one complete day to adapt Phox (my theorem prover) to 3.08
> because the new = does not check first physical equality. Hopefully, the 
> backtracking ocamldebugger let me pin point the many "=" which were 
> looping, otherwise I would have spend a month !!!

If you get non-termination with the = comparison in 3.08, it means
your program is comparing cyclic data structures, which could also
have caused looping with the old = comparison.  It's just that the new =
loops "more easily" than the old one.  But I would argue that your
original code was living dangerously close to the edge.  Don't feel
bad: in developing 3.08 we found several instances of misuses of =
over cyclic structures (types) in the OCaml compiler...

> I was assuming two things about equal:
> - scan of block from left to right
> - a test on adress equality on pointer before follwing the pointer 
> (which is now wrong in 3.08).

That was true of the old implementation, but has never been guaranteed.

As others mentioned, you can recover the behaviour above in 3.08
(it also works in earlier releases) as follows:

let (=?) x y = (Pervasives.compare x y = 0)

and use =? instead of = where appropriate.

> So the comparison between both "=" gives
> 
> old "=":
> - can have much better complexity of some specific data structure
> - nan = nan => true
> 
> new "="
> - can have a small linear speedup on some specific data structure
> - nan = nan => false
> 

You're missing the essential point: the old "=" was inconsistent over
floats, i.e. you'd get different results from the generic = and the
type-specialized = over floats.  Semantic consistency takes precedence
over efficiency.

> Finally, the IEEE norm about floating point arithmetic is not perfect 
> yet.

Maybe not, but it's a consensus that took umpteenth years to achieve
(and got Kahan a Turing award), so one needs very very strong reasons
to depart from it.  

- Xavier Leroy

-------------------
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

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Damien Doligez]

On Oct 8, 2004, at 10:31, Christophe Raffalli wrote:

> I knew and read that (at least the diagnostic was easy),
> but it was still enoyying to have to look for the change to do among 
> 15000
> lines of code. And being forced to use compare x y instead of x = y is 
> ugly.

let (=) x y = compare x y = 0;;

-- Damien

-------------------
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

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Sébastien Furic]

Christophe Raffalli wrote:
> 
> I spend one complete day to adapt Phox (my theorem prover) to 3.08
> because the new = does not check first physical equality. Hopefully, the 
> backtracking ocamldebugger let me pin point the many "=" which were 
> looping, otherwise I would have spend a month !!!
> 
> I was assuming two things about equal:
> - scan of block from left to right
> - a test on adress equality on pointer before follwing the pointer 
> (which is now wrong in 3.08).
> 
> Then in a data type with some structure starting with an identifier 
> filed like
> 
> type symbol = structh { id : int; ... },
> 
> if you have the property that two structures with the same id are always 
> physically equal, the old "=" would never scan the structure itself.

  IMHO it is often better to define your own equality predicates because 
"=" has another annoying property : it fails when comparing "external" 
objects and this failure happens only when comparison reaches those 
objects (note that the type system is perfectly happy, even in the 
presence of "external" objects). For instance, imagine one of the fields 
of a record you want to compare is a Big_int : your program will fail 
only if "=" can't decide for inequality before reaching those fields.

         Objective Caml version 3.08.1

# #load "nums.cma";;
# type test = { n: Num.num };;
type test = { n : Num.num; }
# { n = Num.num_of_string"10000000000000000000000000000000" } = { n = 
Num.num_of_string "200000000000000000000000000000000" };;
Exception: Invalid_argument "equal: abstract value".

  I discovered this behavior when I was developping libraries to handle 
DAGs for a symbolic manipulation program written in OCaml (using the Num 
library). All the preliminary tests of the libraries were OK (I only 
used "internal" objects) but the day I had to use them I had a great 
surprise : they were not as "generic" as I believed them to be.
   In conclusion, if you want your modules to be truly generic, never 
use "polymorphic" equality.

  Cheers,

  Sébastien.

-------------------
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

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1621 bytes --]

Jean-Christophe Filliatre wrote:
> Christophe Raffalli writes:
>  > 
>  > I spend one complete day to adapt Phox (my theorem prover) to 3.08
>  > because the new = does not check first physical equality. 
> 
> Indeed, and it was mentioned in Ocaml 3.08 changes:
> 
> ======================================================================
> * Revised handling of NaN floats in polymorphic comparisons.
>   The polymorphic boolean-valued comparisons (=, <, >, etc) now treat
>   NaN as uncomparable, as specified by the IEEE standard.
>   The 3-valued comparison (compare) treats NaN as equal to itself
>   and smaller than all other floats.  As a consequence, x == y
>   no longer implies x = y but still implies compare x y = 0.
> ======================================================================

I knew and read that (at least the diagnostic was easy),
but it was still enoyying to have to look for the change to do among 15000
lines of code. And being forced to use compare x y instead of x = y is ugly.

> but Pervasives.compare still checks for physical equality first. It's
> clear when having a look at byterun/compare.c.
> 

And assoc now use compare ...


-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]

Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Jean-Christophe Filliatre]

Christophe Raffalli writes:
 > 
 > I spend one complete day to adapt Phox (my theorem prover) to 3.08
 > because the new = does not check first physical equality. 

Indeed, and it was mentioned in Ocaml 3.08 changes:

======================================================================
* Revised handling of NaN floats in polymorphic comparisons.
  The polymorphic boolean-valued comparisons (=, <, >, etc) now treat
  NaN as uncomparable, as specified by the IEEE standard.
  The 3-valued comparison (compare) treats NaN as equal to itself
  and smaller than all other floats.  As a consequence, x == y
  no longer implies x = y but still implies compare x y = 0.
======================================================================

but Pervasives.compare still checks for physical equality first. It's
clear when having a look at byterun/compare.c.

-- 
Jean-Christophe

-------------------
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

[Caml-list] Are you sure the new "=" of 3.08 is good ?

[Christophe Raffalli]

I spend one complete day to adapt Phox (my theorem prover) to 3.08
because the new = does not check first physical equality. Hopefully, the 
backtracking ocamldebugger let me pin point the many "=" which were 
looping, otherwise I would have spend a month !!!

I was assuming two things about equal:
- scan of block from left to right
- a test on adress equality on pointer before follwing the pointer 
(which is now wrong in 3.08).

Then in a data type with some structure starting with an identifier 
filed like

type symbol = structh { id : int; ... },

if you have the property that two structures with the same id are always 
physically equal, the old "=" would never scan the structure itself.

The new "=" can dramatically change the complexity of a program using 
such a structure. It can even loop if your data type are cyclic but all 
cycle need to traverse a structure with the above property (in this case 
the old "=" did not loop).

I imagine there are other examples where the old "=" can be much faster 
than the new one.

So the comparison between both "=" gives

old "=":
- can have much better complexity of some specific data structure
- nan = nan => true

new "="
- can have a small linear speedup on some specific data structure
- nan = nan => false

Clearly for most ocaml programmer the old "=" was better.

Moreover, code relying on, nan = nan to give false are very suspicious 
to me !!! If you need to debug, you have better to insert assertion 
about your floats.

Finally, the IEEE norm about floating point arithmetic is not perfect 
yet. For instance it makes nothing about transcendentals function (see 
below) so I really do not think this norm is so good that OCaml MUST 
respect it for polymorphic equality (a new better norm may appear one day).

--
Here are two small problems with the actual implementation of float:

asin 1.000001 gives nan while some floating point expression which you 
can mathematically prove to be in [-1, 1] gets computed as 1 + epsilon !
so asin x should be equal to asin 1 if x > 1 (idem for -1) otherwise all 
call to asin shoud do a comparison with 1 and -1

sin x with x > 10e100 gives a value which is certainly wrong since you 
can not compute the modulo 2 pi for such a big number.
sin x should give nan when |x| is too big.

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------

-------------------
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