> 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
