[Prev][Next][Index]

# Polynomial specifications

• Subject: Polynomial specifications
• From: leavens@cs.iastate.edu (Gary Leavens)
• Date: 17 Nov 95 00:00:49 GMT
• Keywords: polynomials, LSL
• Newsgroups: comp.specification.larch
• Organization: Iowa State University, Ames, Iowa
• Summary: specification of polynomials

```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
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);
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)
else if degree(p1) < degree(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,
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
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));
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
else rest_of_poly(p)[i]);

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
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,
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):