[isabelle-dev] Polynomial theory

[Brian Huffman]

Quoting Amine Chaieb <ac638 at cam.ac.uk>:

> Hi,
>
>
> 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  
be necessary.

> 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.

- Brian

>
>
> Best wishes,
>
> Amine.