Re: [isabelle] Gcd and algebraic structures

Thanks for all answers,

2014-09-04 9:11 GMT+02:00 Florian Haftmann <
florian.haftmann at>:

> after studying your answers I would recommend that you should follow the
> approach in HOL-Algebra, i.e. use locales with explicit carriers.

Unfortunately, we would prefer to avoid HOL-Algebra: our final goal is to
formalise some well-known algorithms to obtain canonical forms of matrices
over principal ideal rings (echelon forms, Hermite) and generate code of
them*. To do that, we have already developed some infrastructure in the
HOL-Multivariate Analysis library (and its representation of matrices) that
we would like to reuse.

Defining a gcd in an arbitrary ring could be cumbersome working with
structures represented by type classes. Nevertheless, we are mainly
interested in working on principal ideal rings, where any two elements have
a gcd. Hence, gcd would be a total function, and appropriate for a type
class representation. We just wanted to take the chance to implement some
additional Abstract Algebra (commutative rings, integral domains) in a
proper way (including operations such as gcd), but maybe we will have to
reshape this goal.

Fortunately, as far as we know in GCD Domain, Principal Ideal Ring,
Principal Ideal Domain, Factorial Domain and Euclidean Domain, which are
the structures where we plan to work, gcd is a total function.

I will go on thinking about it,



* Most of these algorithms need to compute gcds or Bézout’s identity. As
far as I know, these algorithms could be defined and formalized over a
principal ideal ring, but they wouldn’t be executable if we don’t provide
an executable gcd function. Nevertheless, they would be executable on
matrices whose coefficients belong to an euclidean domain (by means of a
computable euclidean algorithm).

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.