Re: [isabelle-dev] Euclidean Ring
Hi Manuel, On 27/06/15 09:06, Florian Haftmann wrote: What about: »a = unit_factor a * normalize a« Sounds reasonable. See now cb21b7022b00 ff. After accepting that gcd must always target a normalized segment of the underlying ring structure, it is quite obvious how the abstract specification for lcm and gcd must look like. See theory GCD.thy. Using »normalize«, the propositions »a is associated to b« becomes simply »normalize a = normalize b« – logically a little stronger since an explicit normalization is required, but morally equal since such a normalization can be easily provided for all typical candidates. This insight seems to me the final breakthrough after spending approx. 10 years of thinking on gcd. See (EF1) in https://en.wikipedia.org/wiki/Euclidean_domain#Definition – note the »either r = 0 or f(r) f(b)«. Note »either r -- a mod b = 0 -- b dvd a«. Without that termination condition, you cannot prove that polynomials are an euclidean semiring. That is not entirely true. Your weaker assumption allows for a slightly simpler instantiation, but my previous instantiation for polynomials used definition [simp]: euclidean_size_poly p \equiv (if p = 0 then 0 else degree p + 1) I see. I turned to the original specification again. (see https://github.com/3of8/isabellehol_gcd/blob/master/Polynomial.thy and also the other files on that Github repository) Having material in drawers is risky since, without mechanical connection to the distribution, it gets rotten quite fast. Is there anything from there still missing in the Isabelle repository? What comes next? The existing theorems on gcd/lcm/Gcd/Lcm on nat/int must be generalized as far as possible, duplicates identified and possibly thrown away. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Euclidean Ring
As for the terminology, I think I did not find this concept in the
literature and just invented names that seemed reasonable to me at the
time. I agree that normalization_factor perhaps gives the wrong idea; if
you want to change it to something else, I have no objections, but I do
think ‘orient’ sounds a bit strange, especially for rings like the
polynomials.
What about: »a = unit_factor a * normalize a«
2. A generic lcm definition. [...]
I think so. With this definition, ‘lcm (2X²) (2X²)’ would return ‘4X²’,
which is certainly not what we want. If you put this definition in
semiring_gcd, you cannot change it later either. Or am I missing
something here?
I see. Hence an abstract specification of lcm requires normalization to
be at hand already (which seems not to be a problem).
I still had the hope that it would be possible to develop an abstract
specification for gcd which would form a lattice: »gcd a a = a«. But
now I cam to realize that for Gcd :: 'a set = 'a this would require a
complete lattice operation or such on the units, which just does not
make any sense for polynomials over rats or reals. So I think now it is
best if the gcd operations only target the normalized segment of the
underlying ring, with the weaker »gcd a a = normalize a«.
The deeper reason why we deal with normalization at all is that we have
no rewrite machinery for equivalences, otherwise »gcd a a =(dvd)= a«
would do.
3. Gcd/Lcm. In your Gcd/Lcm approach, Lcm is the »more primitive«
definition. Did you just take this over from src/HOL/GCD.thy, or is
there a deeper reason to do it this way round?
I don't remember. I remember that it took me quite a long time to make
this definition work; the case of what to do when you want to take the
Gcd/Lcm of an infinite set was tricky. I think I was under the
impression that handling the case of infinitely many elements was easier
to handle in Lcm, but I do not remember why. I may also be mistaken.
The Gcd/Lcm involves only euclidean size and nothing of the euclidean
algorithm. Maybe it is sufficient to specify the abstract properties of
Gcd/Lcm abstractly in a typeclass like semiring_Gcd and do everything
else on the instance level.
Well, normalisation can be seen as a map sending a ring element to the
equivalence class of all associated elements. In the case of units,
there is an obvious candidate for a canonical representative for this
equivalence class, namely 1. For other equivalence classes, I do not
think that is the case. One could intuitively argue that, in the ring of
polynomials, X is a better representative than -X. In other rings,
like the ring of Gaussian integers, things are not so clear. What should
be the representative of the associated elements {1+i, 1-i, i-1, -1-i}?
I do not think there is an obvious candidate.
Well, for the Gaussian integers, the upper right quadrant could be a
»natural« choice. (Btw. a formalisation of the Gaussian integers could
be a nice student project.)
I therefore think that the choice of what is normalised and what is not
is somewhat arbitrary and it is therefore not possible to find a
restriction that does what you want to do in general. Again, I could be
wrong about this; it has been one and a half years since I last worked
on this.
I don't think so either.
I am wondering about changeset f2f1f6860959, ‘generalized to definition
from literature, which covers also polynomials’. Where did you find this
in the literature? What does it achieve?
See (EF1) in https://en.wikipedia.org/wiki/Euclidean_domain#Definition –
note the »either r = 0 or f(r) f(b)«. Note »either r -- a mod b = 0
-- b dvd a«. Without that termination condition, you cannot prove
that polynomials are an euclidean semiring.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Euclidean Ring
On 27/06/15 09:06, Florian Haftmann wrote: What about: »a = unit_factor a * normalize a« Sounds reasonable. I still had the hope that it would be possible to develop an abstract specification for gcd which would form a lattice: »gcd a a = a«. But now I cam to realize that for Gcd :: 'a set = 'a this would require a complete lattice operation or such on the units, which just does not make any sense for polynomials over rats or reals. So I think now it is best if the gcd operations only target the normalized segment of the underlying ring, with the weaker »gcd a a = normalize a«. The deeper reason why we deal with normalization at all is that we have no rewrite machinery for equivalences, otherwise »gcd a a =(dvd)= a« would do. Well, the problem is that the gcd/lcm are best not viewed as operations on ring elements, but rather operations on the equivalence classes w.r.t. association. On these, they actually form a lattice, if I am not mistaken. Perhaps gcd/lcm on the actual ring elements is a ‘prelattice’? Is that a thing? (Btw. a formalisation of the Gaussian integers could be a nice student project.) I coud have sworn we had a formalisation of Gaussian integers somewhere, but I cannot seem to find it anymore. Perhaps I am wrong. See (EF1) in https://en.wikipedia.org/wiki/Euclidean_domain#Definition – note the »either r = 0 or f(r) f(b)«. Note »either r -- a mod b = 0 -- b dvd a«. Without that termination condition, you cannot prove that polynomials are an euclidean semiring. That is not entirely true. Your weaker assumption allows for a slightly simpler instantiation, but my previous instantiation for polynomials used definition [simp]: euclidean_size_poly p \equiv (if p = 0 then 0 else degree p + 1) (see https://github.com/3of8/isabellehol_gcd/blob/master/Polynomial.thy and also the other files on that Github repository) Cheers, Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Euclidean Ring
Hallo,
thanks for all the good work. It's nice to finally see my work
integrated so neatly into HOL.
1. Normalization. Currently, there is normalization_factor such that a
div normalization_factor a yields the normalized elements. My impression
is that the latter should be an operation on its own, say normalize, and
that normalization_factor is a misleading name since it suggests that
actually a * normalization_factor a is the normalized element. Have we
any other plausible name, say »orientation«? The idea is that normalize
and orientation work on integers like abs and sgn.
I do not remember why I chose to do it that way. I do remember weighing
normalization_factor against a ‘normalize’ operation and deciding for
the former. I take it that you have worked with the definitions for a
while now, so if, after that, you think that a ‘normalize’ operation is
better, I defer to your judgement.
As for the terminology, I think I did not find this concept in the
literature and just invented names that seemed reasonable to me at the
time. I agree that normalization_factor perhaps gives the wrong idea; if
you want to change it to something else, I have no objections, but I do
think ‘orient’ sounds a bit strange, especially for rings like the
polynomials.
2. A generic lcm definition. In ordinary lattices, inf and sup are dual
to each other and there is little reason to prefer one over that other.
Concerning gcd and lcm, I have the strong impression that gcd is the
more primitive one and lcm should be solely derived from it. This is
supported by the observation that instantiation proofs get horrible if
you have to derive the characteristic properties of gcd and lcm on, say,
nat, simultaneously. Hence I argue that the specification of
semiring_gcd should contain a plain definition of lcm. Since the plain
semiring_gcd is not supposed to know anything about normalization, this
would lead to a plain »lcm a b = a * b div gcd a b«, in contrast to the
current »lcm a b = a * b div gcd a b div normalization_factor (a * b)«.
Do you foresee any difficulties here?
I think so. With this definition, ‘lcm (2X²) (2X²)’ would return ‘4X²’,
which is certainly not what we want. If you put this definition in
semiring_gcd, you cannot change it later either. Or am I missing
something here?
3. Gcd/Lcm. In your Gcd/Lcm approach, Lcm is the »more primitive«
definition. Did you just take this over from src/HOL/GCD.thy, or is
there a deeper reason to do it this way round?
I don't remember. I remember that it took me quite a long time to make
this definition work; the case of what to do when you want to take the
Gcd/Lcm of an infinite set was tricky. I think I was under the
impression that handling the case of infinitely many elements was easier
to handle in Lcm, but I do not remember why. I may also be mistaken.
A further observation concerns algebraic closedness of normalized
elements. The properties »normalization_factor 1 = 1« and
»normalization_factor (a * b) = normalization_factor a *
normalization_factor b« state that normalized elements form a
multiplicative group. I did not find a reasonable characterization for
the additive behaviour, i.e. a way to enforce that for int normalization
goes for positive elements only and not a funny mixture like 1, -2, 3,
4, 5, -6, 7, -8. The tempting option to demand closedness under addition
does not work for polynomials, since x + x = 2 * x is not normalized any
longer. On the other hand, the theory works without any such enforcement.
Well, normalisation can be seen as a map sending a ring element to the
equivalence class of all associated elements. In the case of units,
there is an obvious candidate for a canonical representative for this
equivalence class, namely 1. For other equivalence classes, I do not
think that is the case. One could intuitively argue that, in the ring of
polynomials, X is a better representative than -X. In other rings,
like the ring of Gaussian integers, things are not so clear. What should
be the representative of the associated elements {1+i, 1-i, i-1, -1-i}?
I do not think there is an obvious candidate.
I therefore think that the choice of what is normalised and what is not
is somewhat arbitrary and it is therefore not possible to find a
restriction that does what you want to do in general. Again, I could be
wrong about this; it has been one and a half years since I last worked
on this.
I am wondering about changeset f2f1f6860959, ‘generalized to definition
from literature, which covers also polynomials’. Where did you find this
in the literature? What does it achieve?
Cheers,
Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
