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.

Fri Sep 5 16:28:58 MDT 1997