next up previous contents
Next: Command Reference Up: Programming Style Previous: Recursion

Abstraction and Reduction Algorithms

In this section, verbatim text from prover output is presented. The reader should remember that default precedence under Mark2 is equal for all operators, and that all operators associate to the right.

We present a limited abstraction tactic. This tactic ABSTRACT has the form

ABSTRACT @ ?x:

?y = 

(ABSCONST @ ?x) =>> (ABSINFIX @ ?x) 
=>> (ABSCOMP @ ?x) =>> (ABSID @ ?x) => ?y

The tactic takes as a parameter the term with respect to which we will abstract, and applies a tactic taken from a list of alternatives (each of which inherits the parameter.

ABSID @ ?x:

?x = 

Id @ ?x

The only thing which distinguishes the ABSID subtactic from the converse of the defining axiom of the identity function Id is the presence of the parameter, which ensures that only the term from which we are abstracting will have this subtactic applied to it.

ABSCOMP @ ?x:

?f @ ?y = 

COMP <= ?f @ (ABSTRACT @ ?x) => ?y

COMP:

(?f @@ ?g) @ ?x = 

?f @ ?g @ ?x

We display the ABSCOMP subtactic and the defining axiom COMP of the function composition infix @@ on which it depends. The recursive application of ABSTRACT should convert ?y to something of the form ?Y @ ?x, and application of the converse form of COMP to ?f @ ?Y @ ?x will give (?f @@ ?Y) @ ?x. Note that it is assumed that ?x does not appear as a subterm of the function ?f; this restriction is essentially the same as the restriction on abstraction in EFT. It is possible to write more powerful abstraction tactics, but this one has proved adequate for most applications we have worked on.

ABSINFIX @ ?z:

?x ^+ ?y = 

RAISE => ((ABSTRACT @ ?z) => ?x) 
^+ (ABSTRACT @ ?z) => ?y

The built-in theorem RAISE is described elsewhere in this documentation. If ^ + is assumed to have trivial relative types, RAISE has the effect of the theorem RAISE0: (?f @ ?x) ^ + (?g @ ?x) = (?f :^ + ?g) @ ?x. The theorem has more complicated effects on operators which have nontrivial relative types. The reason why the theorem RAISE is needed is that operators (at least, operators with nontrivial type information) are not first-class objects in the logic of Mark2, and abstraction with respect to operators presents logical difficulties. The theorem RAISE0 above can now be stated as an axiom or proved as a theorem using RAISE, but even this kind of abstraction was not possible until we permitted the declaration of operator variables with fixed type information.

The effect of the recursive applications of ABSTRACT should be to convert the whole term to the form RAISE => (?X @ ?z) ^ + (?Y @ ?z), and application of RAISE will convert this to the form (?X :^ + ?Y) @ ?z.

The three subtactics above handle the cases where we see the term from which we are abstracting by itself, or where we see a function application or an infix term. In all other cases, we use a constant function as our abstraction:

ABSCONST @ ?x:

?y = 

[?y] @ ?x

This tactic differs from the converse of the defining axiom for constant functions only in having a parameter. Its effect is to express ?y as a function of ?x in a trivial way. The alternative control structure is very useful here, since this subtactic applies to any term at all! The abstraction tactics written before alternative rule infixes were available applied this subtactic first, then looked at the result and reversed it where it could be recognized that the other cases applied; these algorithms were a little harder to understand!

The execution of the term (ABSTRACT @ ?x) => ?t always has the effect of producing a term of the form ?T @ ?x; for a wide class of terms t the term T will not contain any instance of the term ?x. The term matching ?x does not have to be a variable!

We present a reduction algorithm which ``undoes'' the abstraction algorithm above.

REDUCE:

?x = 

((LEFT @ REDUCE) *> (RIGHT @ REDUCE) *> RAISE) 
<<= ((RIGHT @ REDUCE) *> COMP) =>> CONST =>> Id 
=> ?x

This algorithm has simpler recursion than the ABSTRACT algorithm, but it involves the use of more sophisticated control structures. The theorems Id and CONST (not exhibited) have the effect of applying identity and constant functions respectively. The theorem COMP is exhibited above (the definition of function composition). The effect of the *> operator is to cause (in the first instance) the theorem RIGHT @ REDUCE to be applied as well when COMP is applicable (this is the ``guarded command'' format described above). We examine the parameterized theorem RIGHT:

RIGHT @ ?th:

?x ^+ ?y = 

?x ^+ ?th => ?y

This theorem takes a theorem ?th as a parameter, and applies it to the right subterm of the term to which the parameterized theorem is applied. This is useful when the subterm to which this theorem is to be applied does not yet exist in the term to which the parameterized theorem is applied (in this case, the subterm in question is to be created by the application of COMP).

A segment of output of the tactic debugger is exhibited to illustrate how this works:

((LEFT @ REDUCE) *> (RIGHT @ REDUCE) *> RAISE) 
<<= ((RIGHT @ REDUCE) *> COMP) =>> CONST =>> Id 
=> (?f @@ Id) @ ?x

(RIGHT @ REDUCE) => ?f @ Id @ ?x

?f @ REDUCE => Id @ ?x

The parameterized theorem LEFT used above is exactly analogous in form to RIGHT, except that it operates on left subterms. A related theorem is the theorem $, (used below) exhibiting the possibility of theorems whose names are operators. This theorem has the effect of applying the theorem which is its argument in its ``converse'' form:

 $?th:

?x = 

?th <= ?x

In connection with proving theorems like LEFT, RIGHT, and $, it is useful to note that the rule introduction commands will accept variables as theorems!

The effect of the complex theorem ((LEFT @ REDUCE) *> (RIGHT @ REDUCE) *> RAISE), applied in the reverse sense, which is the last alternative in REDUCE is to apply the converse of RAISE (if it is applicable) and follow this by reducing the left and right subterms of the resulting term.

The use of guarded command format eliminates the necessity in earlier versions of special theorems for each of the separate cases.

As an example of the application of abstraction and reduction algorithms, we present a tactic which implements the axiom (HYP) of EFT in a very powerful form:

PIVOT:

(?a = ?b) || ?x , ?y = 

(RIGHT @ LEFT @ REDUCE) => HYP => (?a = ?b) 
|| ((ABSTRACT @ ?a) => ?x) , ?y

The effect of this tactic is to substitute the term matching ?b for the term matching ?a throughout the term matching ?x. The effect of abstraction is to convert ?x to something like ?X @ ?a. The theorem HYP from the logical preamble can then be applied:

HYP:

(?a = ?b) || (?f @ ?a) , ?c = 

(?a = ?b) || (?f @ ?b) , ?c

and the reduction algorithm (directed to the appropriate subterm) cleans up. The user never sees an abstraction term:

PIVOT => (?a = ?b) || (?a & ?a) , ?b

val it = () : unit
- execute();


{(?a = ?b) || (?b & ?b) , ?b}

The use of theorems like PIVOT may be largely superseded by the new facility for reasoning under hypotheses (see above), but it is still an instructive programming example.

We exhibit abstraction and reduction theorems which use the new variable binding capabilities of Mark2: these algorithms actually use the synthetic abstraction and reduction algorithms in conjunction with the built-in theorem VALUE (documented here) and the axiom BETA also given (note the use of the theorem $ described above):

BETA:

[?f @ ?1] = 

?f

BETAABSTRACT @ ?x:

?y = 

(LEFT @ VALUE @ [REDUCE]) => (LEFT @  $BETA) 
=> (ABSTRACT @ ?x) => ?y

BETAREDUCE:

?f @ ?x = 

REDUCE 
=> (BETA => (VALUE @ [ABSTRACT @ ?1]) => ?f) @ ?x

When working with variable binding contexts, it is useful to remember that there are strong restrictions on the conditions under which free variables of Mark2 can match terms containing bound variables.

It is useful to be aware that the new theorems EVAL and BIND implement abstraction and reduction directly for functions expressed by variable binding contexts; use of the bound-variable-free abstraction features of the prover is now entirely optional.


next up previous contents
Next: Command Reference Up: Programming Style Previous: Recursion

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997