Re: [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  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

[Makarius]

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

[David Matthews]

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

[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-...@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

[Manuel Eberl]

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

[Florian Haftmann]

>> 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=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=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

[Makarius]

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=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=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

[Florian Haftmann]

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

[Makarius]

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