[isabelle-dev] Polynomial theory
florian.haftmann at informatik.tu-muenchen.de
Mon Jan 12 09:37:13 CET 2009
let me add some observations:
> Actually, I had executability in mind when creating this theory. A new feature, which is not present in the original HOL/Abstract/poly development, is the constructor function pCons :: 'a => 'a poly => 'a poly. It basically means the same thing as Cons in the list-based theory. For example, the polynomial x2 + 2*x + 5 could be written as (pCons 5 (pCons 2 (pCons 1 0))). (It would also be easy to add some list-style syntax for pCons.)
> Anyway, I think it would be easy to do code generation for these polynomials, using 0 and pCons as the constructors. All of the operations defined in the theory would be executable on this representation, including div and mod.
I agree that this seems to be the way to go.
> I think there is probably no point in trying to unify the type-class approach with the locale-based approach from HOL/Algebra. The locale-based HOL/Algebra seems to be most useful for people who want to do meta-reasoning about algebraic structures like groups, rings, etc. On the other hand, the type-class approach is better for people who want to reason within specific groups, rings, etc. The two approaches deserve to exist separately.
There is also a pragmatic distinction: the type/typeclass-oriented
developments in HOL try not be as general as possible at any cost, but
provide a simple base for 80% of all applications; if more general
developments are needed (explicit carriers, equivalence relations),
HOL-Algebra is the way to go.
I think the same argument also applies to the various discussions how to
represent multivariate polynomials: perhaps for many applications the
pragmatic way of using nested univariate polynomials is enough; in
advanced cases more general or more powerful developments are needed.
> The only disadvantage I can think of right now, compared to list-based polynomials, is that "length" is easier to reason about than "degree". However, this is probably just a matter of finding a good set of lemmas about "degree".
I am not sure about this. I think there is still an isomorphism between
"polynomial degree" and "list length" which can be made explicit e.g. by
coeffs :: 'a poly => 'a list
p != 0 ==> length (coeffs p) = Suc (degree p)
or something alike.
Btw. it seems that this polynomial theory would also supersede some
stuff in HOL-Matrix, but this would need a closer examination.
How to continue with this? I would suggest to
* move Univ_Poly to HOL-Library
* incorporate Polynomial into HOL
I do not know how the latter HOL theories (former HOL-Complex) make use
of Univ_Poly exactly, but the usages in Deriv.thy and
Fundamental_Theorem_Algebra.thy seem to be migratable.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev