Information Technology Reference
In-Depth Information
3
Polynomial Rings and Ideals
Let
R
=
K
[
x
1
,...,x
k
] be a polynomial ring on an arbitrary commutative field
K
,where
k ∈
IN. The elements of
R
are polynomials in the indeterminates
x
1
,...,x
k
with the coecients in
K
. Polynomials are built from monomials of
R
, that is, power products like
c · x
a
1
1
···x
a
k
k
,where
c ∈ K
is the coecient,
x
a
1
1
···x
a
k
k
IN .
Therefore, there are several algebraic structures that it is necessary to for-
malize prior to the notion of polynomial. A computational theory of multivariate
polynomials on a coecient field was developed in [8, 9]. This Acl2 formaliza-
tion includes common operations and fundamental properties establishing a ring
structure. The aim was to develop a reusable library on polynomials.
Regarding polynomial representation, we have used a sparse, normalized and
uniform representation. That is, having fixed the number of variables, a canoni-
cal form can be associated to each polynomial. In this canonical representation
all monomials are arranged in a strictly decreasing order, there are no null mono-
mials and all of them have the same number of variables. The main advantage
of this representation arises when deciding equality [9].
Monomial lists are used as the internal representation of polynomials. Mono-
mials are also lists consisting of a coecient and a term. Having selected a set
of variables and an ordering on them, each term is uniquely represented by a
list of natural numbers. Although most of the theory is done for an arbitrary
field, via the encapsulation principle, we use polynomials over the field of rational
numbers for our implementation of Buchberger's algorithm. This alleviates some
proofs at the cost of some generality, as Acl2 can use its built-in linear arith-
metic decision procedure. In any case, the general theory has to be eventually
instantiated to obtain an executable algorithm.
The functions
k-polynomialp
and
k-polynomialsp
recognize polynomials
and polynomial lists (with
k
variables and rational coecients). Analogously,
+
,
*
,
-
and
|0|
stand for polynomial addition, multiplication, negation and
the zero polynomial. Let us now introduce the notion of ideal, along with the
formalization of polynomial ideals in Acl2.
Definition 1.
I ⊆ R
is an ideal of
R
if it is closed under addition and under
the product by elements of
R
.
Definition 2.
The ideal generated by
B ⊆ R
, denoted as
is the term, and
a
1
,...,a
k
∈
B
,isthesetoflinear
combinations of
B
with coecients in
R
. We say that
B
is a basis of
I ⊆ R
if
I
=
. An ideal is finitely-generated if it has a finite basis.
Hilbert's Basis Theorem implies that every ideal in
K
[
x
1
,...,x
k
] is finitely-
generated, if
K
is a field. Polynomial ideals can be expressed in Acl2 by taking
this into account. Let
C
B
and
F
be lists of polynomials. The predicate
p ∈F
can be restated as
∃Cp
=
lin-comb
(
C, F
), where
lin-comb
is a recursive function
computing the linear combination of the elements in
F
with coecients in
C
.
As Acl2 is a quantifier-free logic we use a common trick: we introduce a
Skolem function assumed to return a list of coecients witnessing the ideal
membership. In Acl2 this can be expressed in the following way:
Search WWH ::
Custom Search