Re: [isabelle] Gcd and algebraic structures



Hallo,

syntactic type classes such as this are not unusual. They allow
overloading of constants (such as 0, +, *, gcd, …) without restricting
the way in which these constants can be used. In case of gcd, I think
one could make a good argument for assuming basic facts about GCDs in
the type class.

Anyway, if you want to generalise the GCD, I would recommend you
completely ignore the current GCD theory and the gcd type class, because
it already defines a gcd on e.g. the natural numbers and the integers,
and your more general formalisation will probably also yield some GCD
implementation on the natural numbers and integers – resulting in a
clash of these two definitions.

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.

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.

Cheers,
Manuel


On 29/08/14 19:53, Jose Divasón wrote:
> Dear all,
>
> I would like to formalise some linear algebra structures, such as principal
> ideal rings, principal ideal domains, unique factorization domains and so
> on.
>
> As part of those structures, there exist some basic operations over rings
> such as gcd and div, which are already implemented in the Isabelle library.
> For instance, there is a class gcd in the library which has been
> instantiated by int and nat:
>
> class gcd = zero + one + dvd +
>   fixes gcd :: "'a => 'a => 'a"
>     and lcm :: "'a => 'a => 'a"
>
> begin
>
>
>
> Nevertheless, this class seems to me somehow strange, because it doesn’t
> fix any property about gcd and lcm, so it could be instantiated by almost
> anything.
>
> Moreover, the notion of greatest common divisor can be properly defined in
> commutative rings, and also in principal ideal rings, although in general
> there need not exist just one for every pair of elements.
>
> My doubt is how to include that concept in the principal ideal ring class
> that I’m formalising.
>
> I think that there are (at least) three options:
>
> 1.- “Forget” the gcd class that exists in the library and define gcd inside
> my class:
>
> class pir = comm_ring_1 + assumes all_ideal_is_principal: "∀I. ideal I ⟶
> principal_ideal I"
>
> begin
>
> definition "gcd_pir a b = ....."
>
> end
>
> 2.- Define a class called “pir_gcd”, extending gcd and assuming what gcd
> must satisfy.
>
> class pir_gcd = comm_ring_1 + gcd + assumes all_ideal_is_principal: "∀I.
> ideal I ⟶ principal_ideal I"  and "∀a b. gcd a b = ..." and "∀a b. lcm a b
> = ..."
>
> 3.- Option 1 + interpretations/sublocales.
>
> class pir = comm_ring_1 + assumes all_ideal_is_principal: "∀I. ideal I ⟶
> principal_ideal I"
>
> begin
>
> definition "gcd_pir a b = ....."
>
> definition "lcm_pir a b = ....."
>
> interpretation gcd "0::'a" 1 "times::'a=>'a=>'a" "gcd_pir" "lcm_pir" .
>
> sublocale gcd "0::'a" 1 "times::'a=>'a=>'a" "gcd_pir" "lcm_pir" .
>
> end
>
> By the way, what is the difference between interpretation and sublocale in
> this context?
>
> Which is the recommended option? At first I though that it was the last
> one, but then I wondered why the second one has been used in the library
> (there are two classes: semiring and semiring_div in the library instead of
> only one of them).
>
> Thanks,
> Jose





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