[isabelle-dev] Polynomial theory

[Florian Haftmann]

Dear all,

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
a constant

  coeffs :: 'a poly => 'a list

such that

  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.

Opinions?


	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

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: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090112/c3569800/attachment.sig>