Email Gateway (Aug 19 2022 at 15:41): Email Gateway (Aug 19 2022 at 15:41):From: Jose Divasón <jose.divasonm@unirioja.es>
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
Email Gateway (Aug 19 2022 at 15:41):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 19 2022 at 15:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jose,
your are actually stumbling over the issue that HOL so far does not
really provide a hierarchy of type classes for divisibility in rings
(say, factorial ring, euclidean ring etc.)
Here my thoughts of what can be done with reasonable effort at the moment
1) The syntactic gcd type class.
Cf. also Manuel's mail. Syntactic type classes can also be seen as an
instance of the traditional »worse is better« philosophy of UNIX: if you
do not know how to provide the right policy, restrict yourself to
provide a mechanisms while leaving the user to provide its own policy on
his own.
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
Remarks:
a) I strongly believe the assumptions capture the essence of gcd,
whatever the underlying structure is.
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).
c) Here I have chosen »semiring«/»ring« as a base point. Maybe gcd
itself suggests are 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).
d) The specification implicitly states
I. the a gcd exists
II. that is is functional, i.e. normalising wrt. to units
But it does not assume anything how this normalisation actually looks
like, i.e. concrete instances are free to normalise in a specific way.
3) Specific instances for GCD in more specific algebraic structures
a) e.g. for euclidean rings
class euclidean_(semi)ring = …
begin
…
definition gcd_eucl where … -- ‹definition via euclidean algorithm›
…
end
class euclidean_(semi)ring_gcd = euclidean_(semi)ring + gcd
assumes "gcd = gcd_eucl"
begin
subclass (semi)ring_gcd
…
end
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.
b) e.g. for factorial rings
class factorial_(semi)ring = …
begin
…
definition factorization :: "'a => 'a mulitset" where …
…
end
class factorial_(semi)ring_gcd = factorial_(semi)ring + gcd
assumes "gcd a b = msetprod (factorization a + factorization b)"
begin
subclass (semi)ring_gcd
…
end
By the way, what is the difference between interpretation and sublocale in
this context?
»interpretation« pulls in facts into the current target context, which
is closed at the final »end« – »confined interpretation«.
»sublocale« establishes a permanent connection.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
[…]
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
signature.asc
Email Gateway (Aug 19 2022 at 15:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
[…]
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"
2)
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.
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).
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:50):From: Manuel Eberl <eberlm@in.tum.de>
On 02/09/14 13:07, Jose Divasón wrote:
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_domainit is suggested that a
particular Euclidean function fis notpart of the structure of a
Euclidean domain).
I am aware of that, but I saw no reason why a single sufficiently nice
(i.e. fulfilling the “b ≠ 0 ⟹ f (a mod b) < f a” and "b ≠ 0 ⟹ f a ≤ f
(a*b)” conditions) should not suffice. I cannot think of a circumstance
in which you might require several different euclidean size functions.
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))"You can do that and then define euclidean_size with Hilbert choice and
get all the properties you need with exists_euclidean_size. I see no
drawbacks, but, as stated before, I also don't see any real advantages
that would justify it – apart from the fact that you can drop the
monotonicity assumption, because if any euclidean size function exists,
then a monotonic one exists. (which you'd have to prove, of course)
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.I do not think that this is an issue. If I recall correctly, I never use
euclidean_size in any code equations – it is only required for the
termination proof of the Euclidean algorithm, and termination measures
do not have to be executable.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 15:56):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 19 2022 at 16:01):From: Jose Divasón <jose.divasonm@unirioja.es>
Thanks for all answers,
2014-09-04 9:11 GMT+02:00 Florian Haftmann <
florian.haftmann@informatik.tu-muenchen.de>:
Unfortunately, we would prefer to avoid HOL-Algebra: our final goal is to
formalise some well-known algorithms to obtain canonical forms of matrices
over principal ideal rings (echelon forms, Hermite) and generate code of
them*. To do that, we have already developed some infrastructure in the
HOL-Multivariate Analysis library (and its representation of matrices) that
we would like to reuse.
Defining a gcd in an arbitrary ring could be cumbersome working with
structures represented by type classes. Nevertheless, we are mainly
interested in working on principal ideal rings, where any two elements have
a gcd. Hence, gcd would be a total function, and appropriate for a type
class representation. We just wanted to take the chance to implement some
additional Abstract Algebra (commutative rings, integral domains) in a
proper way (including operations such as gcd), but maybe we will have to
reshape this goal.
Fortunately, as far as we know in GCD Domain, Principal Ideal Ring,
Principal Ideal Domain, Factorial Domain and Euclidean Domain, which are
the structures where we plan to work, gcd is a total function.
I will go on thinking about it,
Best,
Jose
Email Gateway (Aug 19 2022 at 16:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jose,
ok, this sounds indeed that you should go for type classes. In case,
others can then use work and generalize it.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:07):From: Jose Divasón <jose.divasonm@unirioja.es>
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
Last updated: Apr 24 2024 at 16:18 UTC