[isabelle-dev] Proper sign of gcd / lcm on type int

[Pierpaolo Bernardi]

About signs in divisions etc. I found the following paper very useful:

http://research.microsoft.com/apps/pubs/default.aspx?id=151917

Maybe someone else will find it useful too.

Cheers


On Fri, Jun 3, 2016 at 9:29 PM, Makarius <makarius at sketis.net> wrote:
> On 03/06/16 18:49, David Matthews wrote:
>
>> The Poly/ML implementation was based on the idea that something called a
>> "multiple" ought to follow the usual rules of multiplication; nothing
>> stronger than that.  I don't think I found anything that indicated what
>> the sign should be.  The GCD code uses GMP's GCD if possible; the LCM
>> code is just derived from that.
>>
>> I have no strong opinions on this and I'm happy to change it.  There's
>> also the question of whether to add it to the IntInf structure and
>> signature despite the incompatibility with the "official" library
>> definition.
>
> How is the situation wrt. planned updates of the SML Basic Library
> specification?
>
> Maybe this is a chance to add IntInf.gcd and IntInf.lcm officially,
> which a clear specification about the sign, whatever that might be.
>
>
>         Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev