Re: [isabelle] Gcd and algebraic structures



Thank you both,

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

I knew this kind of classes are not unusual for elements and operations
which characterise the structure, such as 0, 1, + and *. But, from my point
of view, gcd is not part of the definition of the structure ring.

> GCDs are only unique (modulo association) in integral domains, and only

> guaranteed to exist in factorial rings (UIDs)

You are completely right. As you say, GCDs can exist in a commutative ring
(but not for every two elements). They are unique (modulo association) when
they exist in integral domains and any two elements of a UFD have 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.

By the way, in your formalization I have seen you fix the euclidean size in
the euclidean_semiring class. However, a Euclidean domain will admit many
different euclidean size functions (in
http://en.wikipedia.org/wiki/Euclidean_domain it is suggested that a
particular Euclidean function f is not part of the structure of a Euclidean
domain). Would it be possible to define that class this way? Could there be
any potential drawbacks?

class euclidean_semiring = … +

assumes exists_euclidean_size: "∃f::'a => nat. ∀a b. b≠0 ⟶ (∃q r. a = b*q +
r ∧ (r=0 ∨ f r < f b))"

But if one uses this way of defining the euclidean_semiring class, then it
would not be possible to get direct executability (because the
euclidean_size would not be instantiated). Anyway, with your definition it
would be possible to work with different euclidean sizes of the same
structure if the instantiations are done in independent files. I don’t know
which option is more suitable.

> 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

I think this class defines semirings where every two elements have a gcd,
isn’t it? GCD Domain (http://en.wikipedia.org/wiki/GCD_domain) is the most
similar structure that I have seen in the literature. I would like to deal
with the case of gcd in commutative rings (where gcd exists, but not for
every pair of elements).

> a) I strongly believe the assumptions capture the essence of gcd,

> whatever the underlying structure is.

Your assumptions seem good to me.

> b) Whenever you develop type class hierarchies for ring structures, you

> always have a semiring (the additive structure is a monoid, not a group)

> and a ring.  The semiring part of the hierarchy is to accommodate the

> natural numbers (which, in algebra, appear not be that natural after all).

This is a good point because I was going to work above all with principal
ideal rings (and natural numbers aren’t), thank you for remarking it.

> c) Here I have chosen »semiring«/»ring« as a base point.  Maybe gcd

> itself suggests a more specific entry point to start with already, but

> I have found no argument to do so (maybe you would do after some rounds

> of experimenting and thinking).

In my opinion it is a good base point, although as you say it can change
when developing. Anyway, GCD Domain is the structure that usually appears
in the literature to refer a ring where every two elements have a gcd.

> d) The specification implicitly states

>  I. the a gcd exists

But then such a class formalises a structure where any two elements have a
gcd, which is not true for arbitrary rings. So, if we want to work with
structures (such as commutative rings) where two elements could not have
always a gcd, should we define a gcd inside the class instead of fixing it
in the class? Maybe should gcd have type “ ‘a => ‘a => ‘a option ”?

But in the case we are working with structures where every two elements
have a gcd, then fixing a gcd in the class seems to be the best option.

> Note that this work has already been done by Manuel, but is not yet part

> of Isabelle2014.  If you want to build on that, we will find a suitable

> way without need to participate in the ongoing Isabelle development.

I was talking with Manuel and I already have the file of his development
(Euclidean_Algorithm.thy in the repository version of Isabelle).

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

But if the base structure is an integral domain, then we could not deal
with gcd in the natural numbers.

> Even more thoughts.

>

> 1) A characterisation of a factorial ring.

>

> May sth. like this:
>

> class factorial_(semi)ring = (sem)idom +

>   fixes is_prime :: "α ⇒ bool"

>   assumes "(⋀a. a dvd p ⟹ a dvd 1 ∨ p dvd a) ⟹ is_prime p

>   assumes "is_prime p ⟹ a dvd p ⟹ a dvd 1 ∨ p dvd a"

>   assumes "(⋀a b. p dvd a * b ⟹ p dvd a ∨ p dvd b) ⟹ is_prime p

>   assumes "is_prime p ⟹ p dvd a * b ⟹ p dvd a ∨ p dvd b"

Why should is_prime be fixed in the structure? Prime elements (and
irreducible elements) exist in a commutative ring. I have seen that in
Isabelle2013-2 there was a class called “prime” similar to the gcd one:

class prime = one +

 fixes prime :: "'a ⇒ bool"

But it has disappeared in Isabelle2014.

That is why at first I thought that defining gcd inside the class semiring
was the best option, instead of creating a new class semiring_gcd (even if
semiring_gcd would implicitly assume that every two elements have a gcd).

> Maybe --> holds since the given specification for (semi)ring_gcd demands

> that every two elements have a gcd.  From this it might follow that

> unique factors can be carved out using iterative gcd computations (I

> have once seen such a proof for the natural numbers, but I don't know

> whether this generalizes).

Maybe --> doesn’t hold because it would be necessary the “ascending chain
condition on principal ideals”. At least, for domains it is that way (see
http://en.wikipedia.org/wiki/GCD_domain, where it is said that “an integral
domain is a UFD if and only if it is a GCD domain satisfying the
<http://en.wikipedia.org/wiki/Ascending_chain_condition_on_principal_ideals>ascending
chain condition on principal ideals”).

Still the problem of how to define normalisation properly is not addressed,
but it could be similar to the ones of gcd and prime.

Best,

Jose



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