Re: Integers and Mathematical Correctness

[vincent.diemunsch@gmail.com]

> > 1. It is not consistent with modular types :
> > 
> 
> >    A = (A/B)*B + (A rem B) is not true for modular types. So modular types
> 
> >    should not have a "rem" operator.
> 
> 
> 
> Actually, I question whether you're correct here.  Can you provide an example of a modular type, and values A and B of that type (B /= 0), such that
> 
>    (A/B)*B + (A rem B) /= A ?
> 

> (using the Ada definitions of the operators)?  I may be missing something, but I don't think it's possible.
> 
> 
>                              -- Adam

Hi Adam,

I tried to create a small example to illustrate. Let's try, and please tell me if I am wrong. 

First suppose that you have 4 processors on which you wish to dispatch some piece of work. Imagine that you have 42 simple computations. Each processor will need to process 10 computations and it remains 2 computations that we give to processor n°4. We do have :

     42 = (42 /  4) *4 + (42 rem 4) = 10*4 + 2;

Now we will use a ring buffer to store our computations, instead of a simple array from 1 ... 42. So the buffer has 1024 entries. The 42 computations are located from location n° 1023 - 29 to location n° 12.
We still have 42 computations :  
    
     Last - First + 1 =  11 - (1023 -29) + 1 = -982 == 42 mod 1024.
    
I see that Ada / Gnat correct the modular value to put in 0 .. 1023 before applying the divide operators
/ and rem. So we get the correct result with modular types :  (-982) / 4 = 10 and (-982) rem 4 = 2. 
And finally : ((-982) / 4 ) * 4 + ((-982) rem 4) = 42 == -982 mod 1024.  But clearly 42 /= -982 from the point of view of integers, even if in Ada (-982) = 42 would return true for modular types defined as mod 1024.

So you are right : that means that

      A = (A/B)*B + (A rem B)

holds providing that we understand it the Ada way, which is something like :  

A mod 1024 == Round((A mod 1024) / (B mod 1024))* (B mod 1024) + ((A mod 1024) rem (B mod 1024))

This implies that :
     (-982) / 4 = 10
that I found really ugly and with very little mathematical sense.

And the famous  -A / B  = A / -B = - (A/B)  which is given as the main argument to use "/" instead of "div" is completely false for modular integers in Ada...
   since for exemple -982 /  4 =    42 / 4      = 10
                                982 / -4 = 982 / 1020 = 0
                            -( 982 /  4) = -245 = 779

Now, on the other hand, 

      A = (A div B)*B + A mod B,  

is always true : 
a) for integers : -982 = -246*4 + 2, but I recognize that A div B = -982 div 4 = -246 is of no use for my little problem !!
b) for modular integers (mod 1024), if you set that (-982) div 4 = 10, and (-982) = 42 ! I am not shocked that (-982) div 4 = 10 neither than 982 div (-4) = 0, because the "div" operator is specific and there is no possible confusion with rational division.

So finally I change my mind, the problem is not the "rem" operator for modular type but clearly the use of "/" instead of "div" for modular types. And for signed integers I still would prefer to be able to write Integer (A/B) than simply A/B for the reason that it is simpler in the context of rational types (think of 4 + 1/3 : is it 5/3 or 4 ?).