[Prev][Next][Index]

Polynomial specifications

Quite a while back I posted to this newsgroup a specification
of mathmatical sequences, in view towards specifying the real
numbers.  Steve Garland pointed out how to specify the real
numbers using the concept of a real closed field as an intermediate
stage.  But to do that one needs a specification of polynomials.
I had one (published in earlier versions of the Larch/C++ manual),
but it wasn't very pleasing.  I've since worked out what, I believe,
is a much more elegant specification of polynomials, which I offer
below for your enjoyment.  Any corrections to these would be
appreciated; I've tried doing some LP proofs with them,
but haven't gotten very far...

One interesting aspect of these traits is the following.
There are 3 traits, structured as follows

	Polynomial_basics     Coefficients
                    \           /
                     \         / 
                      \       /
                      Polynomial

meaning that Polyomial includes the other two.  In Polynomial_basics,
the partitioned by clause is a bit clever, in that it makes all polynomials
with the same value at every argument equal.  The trait Coefficients
specifies coefficient lists.  In Polynomial, there is specified
an isomorphism between polynomials and coefficient lists.  Then other
operations on polynomials are specified in a more convenient manner
than would be the case with just pure polynomials or pure coeffieient
lists.

% @(#)$Id: Polynomial_basics.lsl,v 1.3 1995/09/22 22:38:43 leavens Exp leavens $

% Polynomials thought of as functions.
%                               2
% The notation (3 \x 2) means 3x .
% Note that, as functions
%    (3 \x 2) + (5 \x 10) = (5 \x 10) + (3 \x 2) + (0 \x 0)
% and this is specified in the partitioned by clause.

Polynomial_basics(C): trait

  assumes RingWithUnit(C for T)
  includes Natural(Nat), Exponentiation(C, Nat for N)

  introduces
    __ \x __ : C, Nat -> Poly[C]
    __ + __, __ * __: Poly[C], Poly[C] -> Poly[C]
    - __: Poly[C] -> Poly[C]
    evaluate: Poly[C], C -> C
    0, 1: -> Poly[C]

  asserts
    sort Poly[C] generated by \x, +
    sort Poly[C] partitioned by evaluate

    \forall i,j: Nat, a,b: C, p,p1,p2: Poly[C]

      evaluate(a \x i, b) == a * (b ** i);
      evaluate(p1 + p2, b) == evaluate(p1, b) + evaluate(p1, b);

      (a \x i) * (b \x j) == (a * b) \x (i + j);
      (a \x i) * (p1 + p2) == ((a \x i) * p1) + ((a \x i) * p2);
      (p1 + p2) * p == (p1 * p) + (p2 * p);

      evaluate(-p, b) == -evaluate(p, b);

      0:Poly[C] == 0 \x 0;
      1:Poly[C] == 1 \x 0;

  implies
    RingWithUnit(Poly[C] for T)

    \forall i: Nat, a,b: C, p: Poly[C]
      (0:Poly[C]) + p == p;
      (1:Poly[C]) * p == p;
      evaluate((a \x 0) + p, b) == a + evaluate(p, b);
      evaluate(a \x 1, b) = a * b;
      -(a \x i) == ((-a) \x i);

    converts
      __ * __: Poly[C], Poly[C] -> Poly[C],
      - __: Poly[C] -> Poly[C],
      evaluate: Poly[C], C -> C,
      0: -> Poly[C],
      1: -> Poly[C]

% @(#)$Id: Coefficients.lsl,v 1.2 1995/09/22 22:38:43 leavens Exp leavens $

% Polynomials represented as lists of coefficients.

Coefficients(C): trait

  assumes RingWithUnit(C for T)  % stronger than needed, but might want later
  includes String(C, Coeffs[C])

  introduces
    degree: Coeffs[C] -> Int
    leading_coefficient: Coeffs[C] -> C
    rest_of_poly: Coeffs[C] -> Coeffs[C]
    simplify: Coeffs[C] -> Coeffs[C]
    plus, __ + __: Coeffs[C], Coeffs[C] -> Coeffs[C]
    0: -> Coeffs[C]
    - __: Coeffs[C] -> Coeffs[C]
 
  asserts
    sort Coeffs[C] partitioned by degree, leading_coefficient, rest_of_poly

    \forall i,j,n: Int, a,b: C, p,p1,p2: Coeffs[C]

    degree(p) == len(p);
    leading_coefficient(p) == if isEmpty(p) then 0 else head(p);
    rest_of_poly(p) == if isEmpty(p) then {0} else tail(p);

    simplify(a \precat p)
      == if a = 0 /\ ~isEmpty(p)
         then simplify(tail(p))
         else a \precat p;

    plus(p1,p2) == if degree(p1) = degree(p2)
                   then (head(p1) + head(p2)) \precat plus(tail(p1), tail(p2))
                   else if degree(p1) < degree(p2)
                   then head(p2) \precat plus(p1, tail(p2))
                   else head(p1) \precat plus(tail(p1), p2);

    p1 + p2 == simplify(plus(p1, p2));

    0:Coeffs[C] == {0};

    -({a}) == {-a};
    -(a \precat p) == (-a) \precat (-p);

  implies
    AbelianGroup(Coeffs[C] for T,
                 __ + __ for \circ,
                 0 for unit,
                 -__ for __\inv)

    \forall a: C, p: Coeffs[C]

      degree(p) >= 0;
      degree(rest_of_poly(p)) <= degree(p);
      (degree(p) ~= 0) => degree(rest_of_poly(p)) < degree(p);

      (a ~= 0) => (leading_coefficient({a}) = a);
      rest_of_poly({a}) == {0};
      degree({0}) == 0;
      degree({a} + {-a}) == 0;

   converts
     degree: Coeffs[C] -> Int,
     leading_coefficient: Coeffs[C] -> C,
     rest_of_poly: Coeffs[C] -> Coeffs[C],
     simplify: Coeffs[C] -> Coeffs[C],
     plus: Coeffs[C], Coeffs[C] -> Coeffs[C],
     __ + __: Coeffs[C], Coeffs[C] -> Coeffs[C]


% @(#)$Id: Polynomial.lsl,v 1.4 1995/09/22 22:38:43 leavens Exp leavens $

% This specifies both
% the mathematical idea of a polynomial as a function (from Polynomial_basics)
% and the idea of a polynomial as a list of coefficients (from Coefficients).
% The two are combined because otherwise the specification of degree,
% leading_coefficient, and rest_of_poly are as convoluted as
% the theorems in the implies section.

Polynomial(C): trait

  assumes RingWithUnit(C for T)

  includes Polynomial_basics(C), Coefficients(C),
           IntegerAndNatural(Int, Nat)

  introduces
    coefficients: Poly[C] -> Coeffs[C]
    poly: Coeffs[C] -> Poly[C]
    zeros: Nat -> Coeffs[C]             % a helper for coefficients
    __ [ __ ]: Poly[C], Int -> C
    __ - __: Poly[C], Poly[C] -> Poly[C]
    degree: Poly[C] -> Int
    leading_coefficient: Poly[C] -> C
    rest_of_poly: Poly[C] -> Poly[C]
    __ * __: Coeffs[C], Coeffs[C] -> Coeffs[C]
    evaluate: Coeffs[C], C -> C
    1: -> Coeffs[C]

  asserts
    \forall i,j: Int, n: Nat, a,b: C, p,p1,p2: Poly[C], c,c1,c2: Coeffs[C]

    coefficients(a \x 0) == {a};
    coefficients(a \x succ(n)) == a \precat zeros(n);
    coefficients(p1 + p2) == coefficients(p1) + coefficients(p2);

    zeros(0) == empty;
    zeros(succ(n)) == 0 \precat zeros(n);

    poly(empty) == 0 \x 0;
    poly(a \precat c) == (a \x nat(degree(c)+1)) + poly(c);

    p[j] == coefficients(p)[j];

    p1 - p2 == p1 + (-p2);

    degree(p) == degree(coefficients(p));
    leading_coefficient(p) == leading_coefficient(coefficients(p));
    rest_of_poly(p) == poly(rest_of_poly(coefficients(p)));

    c1 * c2 == coefficients(poly(c1) * poly(c2));
    evaluate(c,b) == evaluate(poly(c), b);
    1:Coeffs[C] == {1};

  implies
    RingWithUnit(Coeffs[C] for T)

    sort Poly[C] generated by poly
    sort Poly[C] partitioned by degree, __[__]
    sort Poly[C] partitioned by degree, leading_coefficient, rest_of_poly
    sort Poly[C] partitioned by coefficients

    sort Coeffs[C] generated by coefficients
    sort Coeffs[C] partitioned by poly

    \forall i,j: Int, n,m: Nat, a,b: C, p,p1,p2: Poly[C], c: Coeffs[C]

      poly(coefficients(p)) == p;
      coefficients(poly(c)) == c;

      (j >= 0) => ((p1 - p2)[j] = p1[j] + (-(p2[j])));
      (a \x n)[j] == if (int(n) = j) then a else 0;
      (p1 + p2)[j] == p1[j] + p2[j];

      (i >= 0) => p[i] = (if degree(p) < i then 0
                          else if degree(p) = i
                          then leading_coefficient(p)
                          else rest_of_poly(p)[i]); 

      leading_coefficient(a \x n) == a;
      rest_of_poly(a \x n) == 0 \x 0;

      (degree(p) = i) == (\A j (j > i => p[j] = 0))
                         /\ (p[i] ~= 0 \/ p = 0);
      degree(a \x n) == if (a = 0) then 0 else int(n);   % as 0 \x n == 0 \x 0

      degree((a \x n) + (b \x m))
        == int(if (m = n /\ a+b = 0) then 0 else max(m,n));

      degree(rest_of_poly(p)) <= degree(p);
      (degree(p) ~= 0) => degree(rest_of_poly(p)) < degree(p);

      degree(p1 + p2) ==
        if degree(p1) > degree(p2) then degree(p1)
        else if degree(p1) < degree(p2) then degree(p2)
        else % degree(p1) = degree(p2)
             if degree(p1) = 0 then 0
             else if (leading_coefficient(p1) + leading_coefficient(p2)) = 0
             then degree(rest_of_poly(p1) + rest_of_poly(p2))
             else degree(p1);

   converts
     coefficients: Poly[C] -> Coeffs[C],
     poly: Coeffs[C] -> Poly[C],
     zeros: Nat -> Coeffs[C],
     degree: Poly[C] -> Int,
     leading_coefficient: Poly[C] -> C,
     rest_of_poly: Poly[C] -> Poly[C],
     __ - __: Poly[C], Poly[C] -> Poly[C],
     __ * __: Coeffs[C], Coeffs[C] -> Coeffs[C],
     evaluate: Coeffs[C], C -> C,
     1: -> Coeffs[C]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Comments are welcome.  If there is interest,
I can make these available from the WWW and by ftp in a more standard fashion.

	Gary Leavens
--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html
Follow-Up(s):