Re: [isabelle-dev] Proper sign of gcd / lcm on type int
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 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-...@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-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
On 02/06/2016 08:19, Manuel Eberl wrote: 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. 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. David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
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
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
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-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
>> Both are ok in my view; ironically, lcm is used more often in >> Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial, >> though: >> >> Integer.gcd = PolyML.gcd >> Integer.lcm = abs oo PolyML.lcm > > These two lines are the plan. Is that a good one or a bad one? I tinkered around with (a) fractions.gcd in Python and (b) http://api.mathjs.org/ (a) has mixed signs for gcd (b) has everything normalized Maybe this is evidence that we are rather free in choosing our sign rules, and then normalizing could be a legitimate choice, conceeding that most practical occuring lcm computations concern non-negative denominators. Cheers, Florian > > Presently, I have used PolyML.IntInf.gcd and PolyML.IntInf.lcm for > rat.ML (see da38571dd5bd). It somehow violates our cozy Isabelle/ML > library environment to refer to structure PolyML. > > > BTW, AFP has special code generator setup for PolyML.IntInf.gcd here: > > https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Gauss_Jordan/Code_Generation_IArrays_SML.thy?at=default&fileviewer=file-view-default#Code_Generation_IArrays_SML.thy-33 > > https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Echelon_Form/Examples_Echelon_Form_IArrays.thy?at=default&fileviewer=file-view-default#Examples_Echelon_Form_IArrays.thy-44 > > Luckily, this is only gcd and not lcm, so it coincides already. > > > Makarius > > > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
On 01/06/16 21:27, Florian Haftmann wrote: > Note that the mixed signs of PolyML.IntInf.lcm maintain the property > > gcd a b * lcm a b = a * b > > whereas the lcm in GCD.thy obeys > > gcd a b * lcm a b = normalize a * normalize b > > which emphasises the dual nature of the gcd/lcm lattice. > > Both are ok in my view; ironically, lcm is used more often in > Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial, > though: > > Integer.gcd = PolyML.gcd > Integer.lcm = abs oo PolyML.lcm These two lines are the plan. Is that a good one or a bad one? Presently, I have used PolyML.IntInf.gcd and PolyML.IntInf.lcm for rat.ML (see da38571dd5bd). It somehow violates our cozy Isabelle/ML library environment to refer to structure PolyML. BTW, AFP has special code generator setup for PolyML.IntInf.gcd here: https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Gauss_Jordan/Code_Generation_IArrays_SML.thy?at=default&fileviewer=file-view-default#Code_Generation_IArrays_SML.thy-33 https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Echelon_Form/Examples_Echelon_Form_IArrays.thy?at=default&fileviewer=file-view-default#Examples_Echelon_Form_IArrays.thy-44 Luckily, this is only gcd and not lcm, so it coincides already. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
Hi Makarius, > 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? well, I tend to say they are Isabelle/HOLish. You could also legitimately specify polymorphic gcd as gcd :: nat => nat => nat gcd :: int => int => nat gcd :: … but then you cannot use (single-parameter) type classes. Or you could only specify properties on equivalence classes, e.g. gcd a a =[dvd]= a where a =[dvd]= b <--> a dvd b && b dvd a but such properties cannot be used as rewrite rules of the simplifier. > 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.) Note that the mixed signs of PolyML.IntInf.lcm maintain the property gcd a b * lcm a b = a * b whereas the lcm in GCD.thy obeys gcd a b * lcm a b = normalize a * normalize b which emphasises the dual nature of the gcd/lcm lattice. Both are ok in my view; ironically, lcm is used more often in Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial, though: Integer.gcd = PolyML.gcd Integer.lcm = abs oo PolyML.lcm Cheers, Florian > > > 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 > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Proper sign of gcd / lcm on type int
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