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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle >> -dev >> >> > _______________________________________________ > isabelle-dev mailing list isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-d > ev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev