Is this OK?

Is this OK?

[N Hur]

Sorry for no French.

Why are the two answers below different?

(* a camllight session *)

#(-234)/4
;;
- : int = -58


#div_big_int (big_int_of_string "-234") (big_int_of_string "4");;
- : big_int = -59


(*	end	*)

Thanks for advance for any explanation.

Namhyun Hur

Re: Is this OK?

[Jean-Christophe Filliatre]

> (* a camllight session *)
> 
> #(-234)/4
> ;;
> - : int = -58
> 
> 
> #div_big_int (big_int_of_string "-234") (big_int_of_string "4");;
> - : big_int = -59

There is OK. Indeed, when defining the  quotient and the remainder you
must specify the range of the remainder. Usually, you specify that the
remainder of the division of a by b is between  0 and b-1, whatever is
the sign of a. That is the case in the big_in library.

But in the case of Caml division, the  specification is different: the
remainder has the same sign that a, which is negative in your example.

But in both cases you always have

	a = b * (a/b) + (a mod b)

which is the expected invariant.


-- 
Jean-Christophe FILLIATRE
  mailto:Jean-Christophe.Filliatre@lri.fr
  http://www.lri.fr/~filliatr

Re: Is this OK?

[Xavier Leroy]

> Why are the two answers below different?
> (* a camllight session *)
> #(-234)/4
> ;;
> - : int = -58
> 
> #div_big_int (big_int_of_string "-234") (big_int_of_string "4");;
> - : big_int = -59
> Thanks for advance for any explanation.

In computer arithmetic, integer division has never been well specified
for non-positive arguments.  There are at least two sensible behaviors:

        (a) round towards zero          e.g. (-1) / 2 = 0
        (b) round towards -infinity     e.g. (-1) / 2 = -1

Each of these two behaviors satisfies two of the following three
desirable properties of integer division and modulus, but not all
three:

        (1)   (-a) / b = a / (-b) = - (a/b)
        (2)   a = (a/b) * b + (a mod b)
        (3)   0 <= a mod b < abs(b)

More precisely, (a) satisfies (1) and (2) but not (3) (the modulus can
be negative), while (b) satisfies (2) and (3) but fails (1).  

It is easy to see that (1), (2) and (3) cannot be satisfied
simultaneously anyway, so behaviors (a) and (b) are as good as you'll
ever get.

Most processors implement behavior (a), and therefore most C programs
also follow (a)  (though the C reference manual does not fully specify
integer division and modulus for negative arguments, and therefore (a)
and (b) are both legal).  Since the Caml bytecode interpreter is a
C program, that's also the behavior you get.

The bignum library uses its own signed arithmetic over big integers,
and elected to implement behavior (b), i.e. round towards -infinity,
thus ensuring that the modulus is always positive.  The reason for
this choice, I guess, is that (b) is much better than (a) if you're
doing modulo arithmetic.

So, there is basically no solution to this problem, except providing
two division operations and two modulus operations, one set following
(a) and the other following (b).

- Xavier Leroy

Re: Is this OK?

[Damien Doligez]

>From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>

>But in the case of Caml division, the  specification is different: the
>remainder has the same sign that a, which is negative in your example.

This is not quite true.  In the case of integer division in Caml Light,
the result is unspecified when either argument is negative.  This is
clearly stated in the documentation.

-- Damien