[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
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 500111040 USA / leavens@cs.iastate.edu
phone: (515)2941580 fax: (515)2940258 ftp site: ftp.cs.iastate.edu
URL: http://www.cs.iastate.edu/~leavens/homepage.html
FollowUp(s):