Email Gateway (Aug 19 2022 at 12:44): Email Gateway (Aug 19 2022 at 12:44):From: Walther Neuper <wneuper@ist.tugraz.at>
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
Last updated: Apr 23 2024 at 12:29 UTC