[isabelle-dev] Proper sign of gcd / lcm on type int
eberlm at in.tum.de
Thu Jun 2 09:19:40 CEST 2016
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.
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
> 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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev