Information Technology Reference
In-Depth Information
(defun-sk<k> in<> (p F)
(exists (C) (and (k-polynomialsp C) (equal p (lin-comb C F)))))
The use of
exists
in this definition is just syntactic sugar. Roughly speaking,
the above construction introduces a Skolem function
in<>-witness
,withargu-
ments
p
and
F
, which is axiomatized to choose, if possible, a list
C
of polynomial
coecients such that when linearly combined with the polynomials in
F
,
p
is ob-
tained. Thus,
C
is a witness of the membership of
p
to the ideal generated by
F
,
and
in<>
is defined by means of
in<>-witness
. The following theorems establish
that our definition of ideal in Acl2 meets the intended closure properties:
(defthm |p in <F> & q in <F> => p + q in <F>|
(implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F))
(implies (and (in<> p F) (in<> q F)) (in<> (+ p q) F))))
(defthm |q in <F> => p * q in <F>|
(implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F))
(implies (in<> q F) (in<> (* p q) F))))
Whenever a theorem about
in<>
is proved we have to provide Acl2 with
a hint to construct the necessary witness. For example, to prove that polyno-
mial ideals are closed under addition we straightforwardly built an intermediate
function computing the witness of
p
+
q ∈F
from those of
p ∈F
and
q ∈F
.
Definition 3.
The congruence induced by an ideal
I
, written as
≡
I
, is defined
by
p ≡
I
q ⇐⇒ p − q ∈ I
.
The definition of
≡
F
in Acl2 is immediate
3
:
(defun<k> =<> (p q F)
(in<> (+ p (- q)) F))
Clearly, the ideal membership problem for an ideal
I
is solvable if, and only
if, its induced congruence
≡
I
is decidable. Polynomial reductions will help us to
design decision procedures for that congruence.
4
Polynomial Reductions
Let
<
M
= 0 a polynomial and let
lm
(
p
) denote the leader monomial of
p
with respect to
<
M
.
Definition 4.
Let
f
be a well-founded ordering on monomials,
p
=0
be a polynomial. The reduction relation on polynomi-
als induced by
f
, denoted as
→
f
,isdefinedsuchthat
p →
f
q
if
p
contains a
monomial
m
=0
such that there exists a monomial
c
such that
m
=
−c ·
lm
(
f
)
and
q
=
p
+
c · f
.If
F
=
{f
1
,...,f
k
}
is a finite set of polynomials, then the
→
F
=
i
=1
→
f
i
.
3
For the sake of readability, we use
defun-sk<k>
and
defun<k>
, instead of
defun-sk
and
defun
. These are just macros which add an extra parameter
k
(the number of
variables) to a function definition, so we do not have to specify it in each function
application. When
k
is not involved,
defun
is used.
reduction relation induced by
F
is defined as
Search WWH ::
Custom Search