Re: [isabelle] Gcd and algebraic structures


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. (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).


  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,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.