[isabelle-dev] Euclidean Ring

[Manuel Eberl]

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