One of the goals of the IMPS system is to assist users in producing formal proofs in which the number of steps and the kinds of justification used for each step are close to those of a rigorous and detailed (but informal) proof. One of the main reasons that formal proofs are usually so long is that many proof steps involve replacement of an occurrence of a term t1 with a term t2 having the same value as t1 and which is obtained from t1 by a variety of theory-specific transformations. A formal proof might require hundreds of steps to justify such a replacement. In IMPS, the simplifier is designed to handle many of these inferences directly without user intervention and to bundle them into a single inference step. The simplifier accomplishes this as follows:
The simplifier can be viewed as a function of a context and an expression e which returns an expression The following condition serves as the correctness requirement for the simplifier: For any context (in a theory ) and expression e, and must together entail . That is to say, either e and e' are both defined and share the same denotation, or else they are both undefined.
The simplifier is a highly recursive procedure. For instance, simplification of a compound expression may require prior simplification of all its components (that this is not always true reflects the fact that the simplification procedure for an expression depends on the constructor of the expression). Simplification of individual expression components is done with respect to the local context of that component in the expression. Thus, for instance, in simplifying an implication , A may be assumed true in the local context relative to which B is simplified. Similarly, in simplifying the last conjunct C of a ternary conjunction , A and B may be assumed in the local context. On the other hand, when a variable-binding operator is traversed, and there are context assumptions in which the bound variable occurs free, then the simplifier must either rename the bound variable or discard the offending assumptions. The strategy of exploiting local contexts is discussed in .
At any stage in this recursive descent, certain theory-specific procedures may be applied to a subexpression of the original expression or to a semantically equivalent form of the original expression. These procedures are called transforms. A transform T takes two arguments, a context and an expression e, and returns two values, an expression and a set of formulas called convergence requirements. To apply a transform T to a context and an expression e means to do one of three things:
The transforms used by the IMPS simplifier include:
The framework for applying rewrite rules is entirely general, and uses pattern matching and substitution in a familiar way. By contrast, the transforms that perform algebraic manipulation use specially coded procedures; they are applied to expressions in a way that may not be easily expressed as patterns. Nevertheless, their validity, like the validity of rewrite rules, depends on theorems, many of which are universal, unconditional equalities (e.g., associative and commutative laws).
Instead of providing a fixed set transforms for manipulating expressions in a limited class of algebraic structures, we have implemented a facility for automatically generating and installing such transforms for general classes of algebraic structures. This is possible since algorithmically the transforms are the same in many cases; only the names have to be changed, so to speak. The algebraic manipulation transform is one component of a data structure called an algebraic processor.
An algebraic processor has either two or three associated transforms. There is one transform for handling terms of the form f(a,b) where f is one of the algebraic operations in the processor definition. A separate transform handles equalities of algebraic expressions. Frequently, when the structure has an ordering relation, there is a third transform for handling inequalities of algebraic expressions.
When an algebraic processor is created, the system generates a set of formulas which must hold in order for its manipulations to be valid. The processor's transforms are installed in a theory only if the system can ascertain that each of these formulas is a theorem of
The user builds an algebraic processor using a specification such as
(def-algebraic-processor FIELD-ALGEBRAIC-PROCESSOR (language fields) (base ((operations (+ +_kk) (* *_kk) (- -_kk) (zero o_kk) (unit i_kk)) commutes)))This specification has the effect of building a processor with a transform for handling terms of the form f(a,b), where f is one the arithmetic functions . For example, the entry
(+ +_kk)tells the transform to treat the function symbol as addition. The transforms are installed in the theory fields by the specification
(def-theory-processors FIELDS (algebraic-simplifier (field-algebraic-processor *_kk +_kk -_kk)) (algebraic-term-comparator field-algebraic-processor))When this form is evaluated, IMPS checks that the conditions for doing algebraic manipulation do indeed hold in the theory fields.
What may be especially infuriating to the user is that the presence of
additional assumptions may actually cause the simplifier to return a
much less usable answer. For instance, in the theory h-o-real-arithmetic, the simplifier will reduce the formula