next up previous contents
Next: 15. The Iota Constructor Up: 2. User's Guide Previous: 13. Simplification


14. Macetes

In addition to its simplifier, IMPS also provides a separate mechanism for manipulating formal expressions by applying theorems. Unlike simplification, it is under the control of the user. The basic idea is that some expression manipulation procedures--for instance, conditional rewrite rules--are in fact direct applications of theorems. Other expression manipulation procedures can be formed from existing ones using a simple combination language. These expression manipulation procedures are called macetes.14.1 Formally, a macete is a function M which takes as arguments a context $\Gamma$ and an expression e (called the source expression) and returns another expression $M(\Gamma,e)$ (called the replacement expression). In general, the replacement expression does not have to be equal to the source expression.

Macetes serve two somewhat different purposes:

14.1 Classification

A macete can be atomic or compound. Compound macetes are obtained by applying a macete constructor to a list of one or more macetes.

Atomic macetes are classified as:

Macetes can be also classified according to the relation between the source and replacement expressions.

14.2 Atomic Macetes

14.2.1 Schematic Macetes

A schematic macete can be associated to any formula in two ways depending on the kind of matching procedure used. IMPS has two general forms of matching called expression matching and translation matching.

Let us consider first the case of expression matching. To any IMPS formula we can associate:

Suppose the formula is $\forall x_1\mbox{:}\sigma_1, \ldots
,x_n\mbox{:}\sigma_n,\varphi,$ where $\varphi$ itself is not a universal formula. The patterns are extracted from $\varphi$ depending on the form of $\varphi$ as described by the following table:

Form Source Replacement Conditions Spec.
$\varphi_1 \wedge \cdots \wedge \varphi_n \supset t_1 \simeq t_2 \, \dagger$ t1 t2 $\varphi_1, \ldots, \varphi_n$ Bid.
$\varphi_1 \wedge \cdots \wedge \varphi_n \supset t_1 = t_2 \, \dagger$ t1 t2 $\varphi_1, \ldots, \varphi_n$ Bid.
$\varphi_1 \wedge \cdots \wedge \varphi_n \supset \psi_1 \Leftrightarrow \psi_2$ $\psi_1$ $\psi_2$ $\varphi_1, \ldots, \varphi_n$ Bid.
$\varphi\supset \psi$ $\psi$ $\varphi$ None Back.
$t_1 \simeq t_2 \, \dagger$ t1 t2 None Bid.
$t_1 = t_2 \, \dagger$ t1 t2 None Bid.
$\psi_1 \Leftrightarrow \psi_2$ $\psi_1$ $\psi_2$ None Bid.
$\neg \psi$ $\psi$ $\mbox{${\sf F}$ }$ None Bid.
$\psi$ $\psi$ $\mbox{${\sf T}$ }$ None Bid.


We now describe how a schematic macete M is obtained from the source, replacement, condition patterns, and direction specifier of a formula. Given a context $\Gamma$ and an expression t, the result of applying M to $\Gamma$ and t is determined as follows: Let ${\cal
P}$ be the set of paths $l=(l_1, \ldots, l_n)$ to subexpressions elof t which satisfy all of the following conditions:

The replacement formula is obtained by replacing each subexpression el by $\rho_l(e_l).$ Macetes obtained in this way are called elementary macetes.

Whenever you enter a theorem into a theory, the associated schematic macete is automatically installed, so that you can use it in deductions by hitting the key m.

The case of translation matching is similar, but instead of considering only convergence requirements, we need to insure that the translation component of the translation match is a theory interpretation. Macetes obtained in this way are called transportable macetes. The use of a theorem as a transportable macete must be entered into its usage list when the theorem is entered.

14.2.2 Nondirectional Macetes

Frequently it is useful to construct a schematic macete from an arbitrary formula by using a matching and substitution procedure which does not obey the variable capturing protections and other restrictions of normal matching. We refer to this as nullary matching and substitution. For instance, to apply a theorem which involves quantification over functions, one often has to build a lambda-abstraction of a sub-expression. We shall see later on how this can be done.

14.3 Compound Macetes

Compound macetes are built from atomic macetes and other compound macetes using macete constructors. The constructors are:

Now whether the resulting macete is bidirectional or backward-directional, can be determined by considering the bidirectionality or backward-directionality each of the components.

14.4 Building Macetes

Schematic macetes are for the most part installed by the system when theorems installed.

Elementary macetes are automatically installed when a theorem is added to a theory. The name of the installed macete is the same as the name of the theorem which generates it.
Transportable macetes are installed when the transportable-macete modifier is present in the usage list of a theorem or axiom. Moreover, in this case, the name of the installed macete is the name of theorem which generates it with the prefix tr%.

Macetes are also automatically built when atomic sort and constant definitions are made by the user.

For directly defined constants, the macete corresponding to the constant defining equation is installed. This macete is named
If the usage list of the definition includes the rewrite modifier and the defined constant is a function, the constant defining equation in applied form is also include as a macete named
For recursively defined constants, a number of macetes are installed:
The equation axioms named
The minimality axiom named
The minimality theorem named
For defined atomic sorts a number of macetes are installed:
The sort defining axiom named
Some auxiliary theorems named

Nondirectional schematic macetes usually are not associated to theorems. The form def-schematic-macete can be used for building schematic macetes of all kinds. You can build compound macetes using the form def-compound-macete.

14.5 Applicable Macetes

A macete is ``applicable'' to a formula if applying the macete modifies the formula in some way. The only sure-fire way of determining whether a macete is applicable, is to actually apply the macete and see the result. However, there are simple heuristic conditions which can be used to quickly determine that some macetes are not applicable. For example, for an elementary bidirectional macete, if the left hand side of the macete does not match any subexpression of the formula, then clearly the macete it is not applicable. For transportable macetes other similar inapplicability conditions are used. Macetes are tabulated in such a way that it is possible to quickly throw out inapplicable ones using these heuristic conditions. IMPS exploits this to provide users with a dynamic help facility for selecting macetes. The use of this facility is explained more extensively in Chapter 4.

14.6 Hints and Cautions

Conceptually the macete mechanism is extremely simple. Users however, should not underestimate its power, usefulness, and flexibility. The utility of macetes hinges on three facts:
Though there are various modes of applying macetes, the default mode, with minor premises, is the one you want to use in most cases. The without-minor-premises macete constructor is often useful for building compound macetes to be used in this mode.

next up previous contents
Next: 15. The Iota Constructor Up: 2. User's Guide Previous: 13. Simplification
System Administrator