back to Axiomatic Language Proof Page

Proof of Reverse Specification/Implementation Equivalance

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

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