Also see Evaluation and Rewriting for newer supplementary material. The modern method eliminates the baroque restrictions, thanks to [Howe 1989 LICS].
This appendix gives a more precise description of the direct computation rules than the one given in chapter 8. It should probably be ignored by those who find the previous description adequate, for the details are rather complicated.
The direct computation rules allow one to modify a goal by directing the system to perform certain reduction steps within the conclusion or a hypothesis. The ``direct'' in ``direct computation'' refers to the fact that no well--formedness subgoals are entailed. The present form of these rules, involving ``tagged terms'' as described in chapter 8, was chosen to provide the user with a high degree of control over what reductions are performed. The tagged terms may be somewhat inconvenient at the rule--box level, but it is expected that the vast majority of uses of these rules will be by tactics.
First, we define what it means to compute a term for n steps (for n a nonnegative integer). To do this we define a function on terms t. Roughly speaking, is the result of doing computation (as described in chapter 5) on t until it can be done no further or until a total of n reductions have been done, whichever comes first. The precise definition is as follows. If t is not a term_of term and not a noncanonical term, or if n is 0, then is t. If t is term_of(name) then is , where is the term extracted from the theorem named name. If t is a noncanonical term with one principal argument e then replace e in t by to obtain , and let k be the number of replacements of redices by contracta done by . If n>k, and is a redex, then is , where is the contractum of . If t is noncanonical with two principal arguments (e.g., int_eq) then replace the leftmost one, e, with to obtain , and let k be the number of reductions done by . If is not a canonical term of the right type then is ; otherwise, it is , where is treated as having one (the second) principal argument.
Having now defined we can define what it means to do the computations indicated by a tagging. If T is a term with tags then the computed form of T is obtained by successively replacing subterms of T of the form [[n;t]] or [[*;t]], where t has no tags in it, by or , respectively, where is defined in the obvious way.
It seems very plausible that one should be able to put tags anywhere in a term. Unfortunately, it has not yet been proved that this would be sound, so there is at present a rather complicated restriction, based on technical considerations, on the set of subterm occurrences that can legally be tagged . Let T be a term and define a relation on subterm occurrences of T by if and only if u occurs properly within v. A may be tagged if there are u and v with such that: