Re: [isabelle] Gcd and algebraic structures



Hi José,

after studying your answers I would recommend that you should follow the
approach in HOL-Algebra, i.e. use locales with explicit carriers.

Using type classes has a somehow inherent bias toward totality, e.g.
class idom assumes that the whole type (except 0, of course) forms an
integral domain.  What you want is the real algebraic notion where an
integral domain is a subset of a bigger domain (aka type).  Here it is
where the explicit carriers come in.  Similar for gcd also.

Hope this helps,
	Florian


On 02.09.2014 13:07, Jose Divasón wrote:
> 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
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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