*To*: cl-isabelle-users at lists.cam.ac.uk, Jose Divasón <jose.divasonm at unirioja.es>, eberlm at in.tum.de*Subject*: Re: [isabelle] Gcd and algebraic structures*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 30 Aug 2014 16:29:28 +0200*In-reply-to*: <54019D85.10906@informatik.tu-muenchen.de>*Organization*: TU Munich*References*: <CA+MUZ5sJZcbZnWkPcX8GQM4Ltr6vidDt0FJR1PXnHyVbpGG+CA@mail.gmail.com> <54019D85.10906@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.0

[…] Some further thoughts. > 2) A fundamental algebraic type class for GCD. > > IMHO this could look like: > >> class semiring_gcd = semiring + gcd + >> assumes "gcd a b dvd a" >> assumes "gcd a b dvd b" >> assumes "c dvd a ⟹ c dvd b ⟹ c dvd gcd a b" >> >> class ring_gcd = ring + semiring_gcd Maybe any (semi)ring_gcd is also a factorial_(semi)ring? The direction <-- is obvious. For --> I am uncertain. http://en.wikipedia.org/wiki/Greatest_common_divisor (section »The gcd in commutative rings«) suggests that it does not hold in general. It also suggests that the base structure should be (sem)idom (integral domain) rather than plain (semi)ring. > GCDs are only unique (modulo association) in integral domains, and only > guaranteed to exist in factorial rings (UIDs). Therefore, I would > recommend that you introduce a predicate is_gcd a b :: 'a => 'a => 'a => > bool for commutative rings in order to handle the situation of multiple > (or no) GCDs. Then you can introduce a function gcd :: 'a => 'a => 'a > for integral domains, yielding a normalised GCD if it exists and > undefined (or 0 or 1 or whatever) otherwise, and for factorial rings, > you can then actually prove that this gcd function is “total”, i.e. it > always returns a GCD. I would not recommend to follow this approach from my current perspective. Generally, it is best practice that algebraic type classes are not a device to speculate about (unique) existence of certain operations etc, but simply have such operations as parameters and postulate certain properties of them. For everything more general, it is usually more suitable to follow HOL-Algebra with its locale hierarchy with explicit carrier etc. which allows to develop real meta-theory. This fundamental best practice distinction is a regularly re-occurring issue on this mailing list. > For normalisation, the approach that I took in my formalisation of > Euclidean rings was to define a function called normalisation_factor :: > 'a => 'a, which returns a unit such that dividing any element of the > ring by that unit yields the same result for all elements in the same > association class, effectively normalising the element. E.g. for > integers, the normalisation factor is the sign of the number; for > polynomials, it is the leading coefficient. The deeper reason why we have to burden ourselves with normalisation at all is the matter of equality vs. equivalence. Ideally, gcd is only determined up to equivalence wrt. divisibility, e.g. (n.b. for suggestiveness I am using infix syntax here): a gcd b ≈ b gcd a where (a ≈ b ⟷ a dvd b ∧ b dvd a) Automation support for equivalence reasoning in Isabelle however is poor. Hence we prefer proper equality a gcd b = b gcd a This requires a normalisation. There are different ways to express this idea, here I will use norm :: α ⇒ α norm_unit :: α ⇒ α such that a = norm a * norm_unit a with norm (norm_unit a) = 1 and norm_unit (norm a) = 1 and norm_unit a dvd 1 (maybe further properties are required also). So, a gcd b = (norm a * norm_unit a) gcd (norm b * norm_unit b) = u * (norm a gcd norm b) where (norm a gcd norm b) is the essential gcd on normalised values and u is a unit factor. How to choose u? Manuel's suggestion is to choose u = 1. What I consider unsatisfying then is that a gcd a = norm a – but not necessarily a gcd a = a Hence we cannot establish that gcd forms a lattice. Can we choose a better u? I am not sure. But what I am thinking of is to provide an explicit »micro lattice« (_ inf _) for the units in the underlying ring structure. Hence, a gcd b = (norm a * norm_unit a) gcd (norm b * norm_unit b) = (norm_unit a inf norm_unit b) * (norm a gcd norm b) which would maintain the lattice property. How to choose (_ inf _) then? Maybe there is no general principle, but here some examples: for nat: _ inf _ = 1 (trivially) for int: every unit is (-1) ^ n for n in {1, 2} (-1) ^ m inf (-1) ^ n = (-1) ^ (m max n) (prefer positive values) for ℤ + iℤ (gauss numbers): every unit is i ^ n for n in {1, 2, 3, 4} i ^ m inf i ^ n = i ^ (m max n) (prefer positive values) for K[x] (polynomials over a field): every unit is in K here we must assume a lattice on K uncertain how this would look like in the general case; for reals, we can use the canonical ordering; what about gauss numbers? maybe polar coordinates? Looks a little bit artificial. But maybe it is the »Isabelle overhead« to get a practically usable system. Just a few thoughs, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Gcd and algebraic structures***From:*Florian Haftmann

**References**:**[isabelle] Gcd and algebraic structures***From:*Jose Divasón

**Re: [isabelle] Gcd and algebraic structures***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Gcd and algebraic structures
- Next by Date: Re: [isabelle] Gcd and algebraic structures
- Previous by Thread: Re: [isabelle] Gcd and algebraic structures
- Next by Thread: Re: [isabelle] Gcd and algebraic structures
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list