KnowledgeBase » SEMINAR » ID = 414

Verifying an Implementation of a Polynomial Algebra ADT

by Paul B. Jackson
1994-1995

Abstract

I will describe work I recently completed in Nuprl in specifying an Abstract Data Type (ADT) for arithmetic operations on multivariate polynomials, and in verifying the correctness of an implementation of this ADT.

The specification is based on a common one found in algebra textbooks such as Lang or Bourbaki:

1. Monomials are a free Abelian monoid on the indeterminates.
   
   
2. Polynomials are a free monoid algebra on the monoid of monomials and the ring of coefficients.

The implementation uses association lists for both monomials and polynomials. Functions defined include those for polynomial addition and multiplication, as well as indeterminate instantiation.

This work illustrates well the capabilities of the Nuprl system; in particular, its facilities for reasoning over abstract algebraic structures such as groups, rings and modules, and for the manipulation of nested summations.

A write-up of this work can be found in a chapter of my thesis, which will be available as a Cornell Tech-Report in the next week or two.