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

[Amine Chaieb]

I believe Florian's proposal is good. On a proof-engineering level, the
only "inconvinience" is mainly that the property

gcd a b * lcm a b = a * b

does not hold as such but generally I suspect in the form

gcd a b * lcm a b = normalize(a * b)  -- The normalize in GCD.thy perhaps
has the property normalize (a*b) = normalize a * normalize b

This inconvinience is of course outeighted by the canonical representative
choice of representatives as Manuel points out.

The drawback on generated code by

>         Integer.gcd = PolyML.gcd
>         Integer.lcm = abs oo PolyML.lcm


is that in algorithms computing successive gcds, on every recursive call a
normalization step happens. For integers vs PolyML.lcm this might be
unnoticeable, but for more complex structures, appropriate code equations
might be more efficient.

Amine.

On Thu, June 2, 2016 2:19 am, Manuel Eberl wrote:
> Florian has already hinted at it, but I will say it again explicitly:
>
>
> Mathematically, gcd and lcm are not operations on the elements of a
> ring, but on the equivalence classes w.r.t. associatedness (i.e. mutual
> divisibility). In fact, these equivalence classes form a complete lattice
> w.r.t. divisibility, where inf = gcd, sup = lcm, Inf = Gcd, Sup = Lcm, bot
> = 1, top = 0.
>
>
> However, juggling equivalence classes is inconvenient; it is much nicer
> to use representatives, and ideally canonical representatives. This is why,
> in Isabelle, we require that the gcd/lcm be normalised. For natural
> numbers, everything is normalised; for integers, this means that the
> integer is non-negative; for polynomials, it means that the leading
> coefficient is normalised (if the coefficient ring is a field, this means
> the polynomial is zero or must have leading coefficient 1).
>
> I do think that we should enforce the same thing in the ML
> implementation of gcd/lcm. Any definition of gcd/lcm for integers where
> either of them may be negative does not make much sense to me. My guess
> would be that lcm can be negative in the implementation you mentioned
> because the author defined "lcm a b = a * b / gcd a b" with the unstated
> assumption that it is only called for non-negative numbers. Or perhaps
> they thought the sign does not matter.
>
>
> By the way, speaking of GCDs here and of rational numbers in the other
> thread: I am currently working on a theory of normalised fractions for
> arbitrary GCD rings. This builds on top of Amine Chaiebs fraction fields,
> but additionally requires that the numerator and denominator be normalised
> and the denominator be normalised, which makes the representation unique
> and therefore more convenient.
>
> This theory will then easily be instantiable for polynomials and formal
> power series, yielding rational functions and Laurent series, respectively.
> One could even base Isabelle's rational number theory on
> this more general development in the future.
>
>
> Cheers,
>
>
> Manuel
>
>
>
>
> On 31/05/16 21:37, Makarius wrote:
>
>> Dear integer experts,
>>
>>
>> presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to
>>  understand the situation of gcd / lcm for negative arguments.
>>
>> We have the following slightly divergent operations:
>>
>>
>> * HOL gcd / lcm: always >= 0 (via "normalize" which is "abs")
>>
>>
>> * PolyML.IntInf.gcd: always >= 0
>> PolyML.IntInf.lcm: mixed signs, according to product of arguments
>>
>>
>> * Integer.gcd / lcm: mixed signs -- IIRC the implementation was only
>> meant to operate on "nat", which happens to be spelled "int" in ML.
>>
>> My impression is that the HOL definitions are canonical: several number
>>  theory experts have gone over it over the years. Is this correct?
>>
>>
>> An investigation of the (very few) uses of the above Poly/ML and
>> Isabelle/ML operations in Isabelle + AFP supports the following working
>> hypothesis:
>>
>>
>> Integer.gcd / lcm should follow the HOL versions, in "normalizing" the
>> sign, i.e. removing it. (The updated implementation will use
>> PolyML.IntInf gcd for improved performance.)
>>
>>
>>
>> Does this sound like a good idea?
>>
>>
>>
>> Makarius
>> _______________________________________________
>> isabelle-dev mailing list isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle
>> -dev
>>
>>
> _______________________________________________
> isabelle-dev mailing list isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-d
> ev
>