[isabelle-dev] Euclidean Ring
Manuel Eberl
eberlm at in.tum.de
Fri Jun 26 00:36:49 CEST 2015
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
More information about the isabelle-dev
mailing list