1. Specification of the Reverse of a Sequence
The reverse predicate reverses the elements of a sequence. It is
represented by valid expressions of the form
(reverse <sequence> <reversed_sequence>),
an example being (reverse (a b c) (c b a)).
A specification of this predicate is as follows:
(reverse () ()).
(reverse (% $seq) ($rev %))<
(reverse ($seq) ($rev)).
We refer to the standard definition of axiomatic language as
"General Axiomatic Language" (GAL), where string variables can occur
anywhere in a sequence, The above specification is defined in GAL.
For this proof, we will use a restricted form of axiomatic language
called "Simplified Axiomatic Language" (SAL), where string variables
can only occur at the ends of sequences. Our revised specification
with labeled SAL axioms is as follows:
! append1 - append one expression to end of a sequence
a0 (append1 () %x (%x)).
a1 (append1 (% $) %x (% $'))< (append1 ($) %x ($')).
! reverse - reverse a sequence
r0 (reverse () ()).
r1 (reverse (% $seq) %rev')<
(reverse ($seq) %rev)),
(append1 %rev % %rev').
The append1 function appends a single expression to the end of a sequence.
(An example valid expression is (append1 (x y) z (x y z)).)
When these SAL axioms are given to the current
top-down resolution interpreter, the interpreter computes
the reversed sequence in O(n^2)
time -- quadratic in the length of the sequence. We can do better.
2. Efficient Implementation of Reverse
It turns out the reverse of a sequence can be computed in linear time
by using an "accumulator" predicate, as defined by the following axioms:
! rev_acc - move element between sequence suffix and reversed prefix
! (rev_acc <sequence suffix> <reverse of prefix> <reverse>)
ra0 (rev_acc () ($rev) ($rev))< ! reverse is done
(sequence ($rev)).
ra1 (rev_acc (% $suf) ($rpre) %rev)< ! move element from suffix ..
(rev_acc ($suf) (% $rpre) %rev). ! .. to reversed prefix
! sequence - set of all sequences
s0 (sequence ()).
s1 (sequence (% $))< (sequence ($)).
! reverse (efficient!)
rr (reverse %seq %rev)< (rev_acc %seq () %rev).
For our SAL definition we use a "sequence" predicate as needed so that all
string variables that appear in a conclusion expression will also
appear in a condition.
We need to prove that this efficient O(n) reverse implementation is
equivalent to the O(n^2) specification above.
3. Equivalence of Reverse Specification and Implementation
We need to prove that the O(n^2) specification SAL axioms for reverse
produce the same set of reverse valid expressions as the efficient O(n)
implementation axioms.
A "common axiom set" are those axioms that are part of both the
specification and implementation axiom sets. We repeat these axioms
here with shortened predicate names for conciseness:
! ax set C - Common axioms
a0 (a () %x (%x)). ! append1
a1 (a (% $) %x (% $'))< (a ($) %x ($')).
s0 (s ()). ! sequence
s1 (s (% $))< (s ($)).
ra0 (ra () ($r) ($r))< (s ($r)). ! reverse_accumulator
ra1 (ra (% $s) ($rp) %r)< (ra ($s) (% $rp) %r).
The set of specification axioms S consists of the common axioms C plus
axiom r0,r1:
! ax set S - Specification axioms = C + r0,r1:
r0 (r () ()). ! reverse
r1 (r (% $s) %r')< (r ($s) %r), (a %r % %r').
The set of implementation axioms I consists of the common axioms C plus
axiom rr:
! ax set I - Implementation axioms = C + rr:
rr (r %s %r)< (ra %s () %r). ! efficient reverse
3.1. Some Supporting Valid Clauses
We start with the following valid clauses and their immediate proofs:
ra0x (ra () (%) (%))< (s (%)).
= instance of axiom ra0
ra0y (ra () (%) (%)).
= two unfolds of ra0x
raz (ra (%' $s) (%) %r)< (ra (%' $s) (%) %r).
= instance of generic valid clause % < % .
The following key clause will be more difficult to prove:
rx (ra ($s) (%) %r')< (ra ($s) () %r), (a %r % %r').
When this clause is used as an induction hypothesis, we can unfold
valid clauses against it to produce other hypothesized clauses that
are used later in the induction proof of rx:
unfold raz with rx:
raza (ra (%' $s) (%) %r')< (ra (%' $s) () %r), (a %r % %r').
-- this is a "hypothesized valid" clause
unfold raza cond 1 wrt Common axiom set C:
razb (ra (%' $s) (%) %r')< (ra ($s) (%') %r), (a %r % %r').
-- this is also a hypothesized valid clause
The induction proof of rx is as follows:
unfold rx cond 1 wrt Common ax C:
rx0a (ra () (%) %r')< (s ()), (a () % %r').
unfold rx0a cond 1 wrt C:
rx0b (ra () (%) %r')< (a () % %r').
unfold rx0b cond 1 wrt C:
rx0 (ra () (%) (%)).
= ra0y -- proved
rx1 (ra (%' $s) (%) %r')< (ra ($s) (%') %r), (a %r % %r').
= hypothesized clause razb -- proved!
-- proved!
3.2. Prove Imp Axiom rr Valid wrt Spec Axiom Set S
To prove equivalence between specification and implementation
reverse axiom sets, we need to show that the Implementation axioms
are valid clauses with respect to the Specification axioms and
vice versa. Since the Common axioms are in both the Specification
and Implementation axiom sets, we only need to show the Implementation
axiom rr to be a valid clause with respect to the Specification axiom set:
rr (r %s %r)< (ra %s () %r). ! from above
We first need another supporting valid clause and some "hypothetical valid
clauses":
rz (r %s %r)< (r %s %r).
= instance of % < % .
unfold rz with induction hypothesis rr:
rza (r %s %r)< (ra %s () %r).
-- hypothesized valid clause
unfold rza cond 1 with ra1:
rzb (r (% $s) %r)< (ra ($s) (%) %r).
-- hypothesized valid clause
Our induction proof of rr is as follows:
unfold rr wrt ax set S (= C + r0,r1):
rr0 (r () ())< (s ()).
unfold rr0 cond 1:
rr00 (r () ().
= r0 -- proved
rr1 (r (% $) %r)< (ra ($) (%) %r).
= hypothesized clause rzb -- proved
-- proved!
3.3. Prove Spec Axioms r0,r1 Valid wrt Imp Axiom Set I
We need to prove that specification axioms r0,r1 are valid clauses with
respect to the Implementation axiom rr plus the Common axioms.
We first need some supporting valid clauses defined from rr:
rr (r %s %r)< (ra %s () %r). -- from above
rr' (r (% $s) %r)< (ra (% $s) () %r). -- inst of rr
rr" (r (% $s) %r)< (ra ($s) (%) %r). -- unf rr' w ra1
rrx (r (% $s) %r)< (ra ($s) () %r-), (a %r- % %r). -- unf rr" w rx
Proofs of r0,r1 valid wrt Implementation axioms are as follows:
r0 (r () ()).
= rr unfolded with ra0, unf w s0 -- proved
r1 (r (% $) %r')< (r ($) %r), (a %r % %r').
unfold r1 cond 1 wrt Imp ax set
r11 (r (% $) %r')< (ra ($) () %r), (a %r % %r').
= rrx -- proved
Thus the Specification axioms are valid clauses with respect to the
Implemention axioms and vice versa, so the Specification and Implementation
axiom sets are equivalent.
back
to Axiomatic Language Proof Page
back
to Axiomatic Language Home Page