[isabelle-dev] Polynomial theory
brianh at cs.pdx.edu
Sun Jan 11 18:39:21 CET 2009
Quoting Amine Chaieb <ac638 at cam.ac.uk>:
> This looks like a nice version of Clemen's Algebra/poly/Univ_Poly2.thy.
> I guess it is "justified" to add code-axioms here to implement 'a poly
> with a list, or better once one proves the relation to the executable
> version, I think Florian has a fancy mechanism to make it work?
As I pointed out in my other email, 'a poly should be directly
executable, using 0 and pCons as constructors.
> We have many polynomials in Isabelle and we need some serious work to
> unify the approaches. There is still the locale based (maybe the most
> abstract version Algebra/Univ_Poly.thy). I also have a reflective
> formalization of Multivariate polynomials which I have not committed.
> When we add the Vectors theory (the finite Cartesian product
> construction) we could formalize multivariate polynomials appropriately,
> then Univariate polynomials will become again an instance of that
> general theory. I don't know what is the best 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.
For multivariate polynomials, one way to get these would be to simply
iterate the univariate polynomial type constructor. For example, you
can think of the type 'a poly poly as representing polynomials over
two variables with coefficients in 'a.
If you want something more general (maybe you want to reason about
polynomials with an arbitrary number of variables) then maybe a monoid
ring (http://en.wikipedia.org/wiki/Monoid_ring) would be a good
generalization to use. This could be a type constructor with two
parameters, one for the ring of coefficients, and one for the monoid
of exponents. Then ('a, nat) monoid_ring would represent univariate
polynomials, and ('a, 'b multiset) monoid_ring could represent
multivariate polynomials, where 'b is a finite type indexing all of
the indeterminate variables. I'm not sure why a Vectors theory would
> I recently developed (and still developing) a theory of (univariate)
> formal power series (infinite polynomials, if we like) and was
> originally also hoping to deduce everything about polynomials from it.
> It introduces a type constructor 'a fps which is isomorphic to nat => 'a.
> Unfortunately the class mechanism can only constrain the range 'a and
> hence we can not recover the polynomials from that formalization. But if
> you happen to see a way to do it, then please let me know.
I have thought about formal power series as well, and I had noticed
that many proofs about addition and multiplication are the same as
with polynomials. I think it would be simple to define one in terms of
the other. If you don't do it already, we would want to define 'a fps
using a typedef, rather than as a type synonym. Then we could define
addition, multiplication, etc. on 'a fps, and give instances for
group, ring, and idom classes. Then we could define 'a poly as the
subset of "finite" elements of 'a fps. We just need to prove that
operations like addition and multiplication preserve the "finite"
property, and we could inherit all of the other properties of those
operations from 'a fps.
> Best wishes,
More information about the isabelle-dev