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.

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.

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

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 clauseThe 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!

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 aboveWe 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 clauseOur 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!

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 rxProofs 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