[isabelle-dev] Euclidean Ring

[Florian Haftmann]

> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150627/f3b0c494/attachment.sig>