# [isabelle] HOL/../Polynomial + afp/../Polynomial

`In the Isabelle2013-1 distribution there is a new type of multi-variate
``polynomial [1], which is the basis for proving the Fundamental Theorem
``of Algebra etc. In addition to providing algebraic structure, the
``executable version of [1] corresponds to a _recursive_ representation.
`

`In the AFP is another type of executable multi-variate polynomial [2] in
``_distributive_ representation. This specific representation is required
``for specific algorithms, for instance, the Groebner Bases algorithm.
`

`After promising trials with both, [1] and [2], we envisage to develop
``theories for algebraic geometry including efficient polynomial
``algorithms --- and we have many, many questions. The first question is,
``what we consider the most principal one:
`

`(a) given a type of multi-variate polynomial providing algebraic
``structure (like [1]) with new properties added
``(b) given several executable representations for polynomials, at least
``recursive (like "pCons" in [1]) and distributive (like "monom list" in
``[2]) with respective conversions
``? What is the most succinct way to share the properties from (a) with
``several representations (b) in Isabelle (such that generated code
``"inherits" properties from (a)) ?
`
We are grateful for any input and prepared for not-so-easy suggestions,
Walther
[1] http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Polynomial.html
[2] http://afp.sourceforge.net/entries/Polynomials.shtml

`[3]
``http://isabelle.in.tum.de/dist/library/HOL/HOL-Decision_Procs/Reflected_Multivariate_Polynomial.html
`

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