Information Technology Reference
In-Depth Information
Monotonicity in Calculational Proofs
David Gries
Computer Science, Cornell University, gries@cs.cornell.edu
Computer Science, University of Georgia, gries@cs.uga.edu
Abstract. We discuss the use of weakening and strengthening steps in
calculational proofs. We present a metatheorem concerning monotonicity
of positions in a formula that should have a more prominent place in the
teaching of such proofs and give supporting examples.
Introduction
We are dealing with a calculational predicate logic with equality, using the no-
tation of [3]. The universal quantication (
8x R
P
:
) is equivalent to the more
8x:R ) P
9x R
P
standard
and the existential quantication (
:
) is equiva-
lent to
is called the range of the quantication. Using this notation
allows us to have a unied notation for expressing all sorts of quantications,
including summations and products.
A few more notational conventions: The operator
9x:R ^ P
.
R
denotes equality on
booleans; it is more traditionally represented by symbol
,
.And
f:x
denotes
the application of function
.
Now for the reason for this little paper. In making a calculational step like
f
to argument
x
(
8x
:
P ^ R
)
)h
P ) P _ Q i
Weakening
8x
(
:(
P_Q
)
^R
)
we are implicitly using the fact that the occurrence of variable
that is being
replaced is in a monotonic position |weakening that position weakens the whole
formula. To make the proof more precise and complete, the fact should be made
explicit. We use a long-known but basically forgotten theorem for this purpose
and show how it is used in several calculational proofs.
P
Monotonicity
A function
f
is monotonic in its argument if
x ) y
implies
f:x ) f:y
(for
all
x; y
). It is antimonotonic if
x ) y
implies
f:x ( f:y
(for all
x; y
).
are monotonic in each of
their operands, negation is antimonotonic in its operand,
The following facts are well-known:
_
and
^
)
is monotonic in its
consequent and antimonotonic in its antecedent, (
8x R
:
P
) is monotonic in
Search WWH ::




Custom Search