Evaluation and Term Rewriting

Since equality between terms, either with respect to a type or between extensional or intensional type expressions themselves, is symmetric and transitive, any chain of these alterations, in either direction, preserves the denotation of an expression. We shall usually indicate such rewrites like this:

<a,b,c>/x,y,z. f(x;y;z) * <b,c>/y,z. f(a;y;z)

and they may be chained

<a,b,c>/x,y,z. f(x;y;z) * <b,c>/y,z. f(a;y;z) * f(a;b;c)

The "<pre term> * <post term>" form indicates the direction of the intended rewrite, though a rewrite can always be reversed as well. The reason a direction is indicated is that these notations are used in Proofs to indicate rewrites to be performed during steps of inference.

It is possible to indicate subparts of a term to be rewritten, and how to rewrite it. As will be exemplified below, the <term> operator indicates which part the term is to be rewritten. One may always simply indicate that the whole term is rewritten, leaving it to the reader whether subparts are rewritten, but sometimes it helps to focus attention. Also, since these rewrite instructions are created interactively by the user pointing at parts to rewrite, and how to do the rewrite, these <term> indications are actually in the rewrite specification, and are simply being suppressed for improved readability. For example,

if true 1+1 else 2+2 fi * InjCase(true ; 2; 2+2) * 2

was actually derived from the following rewrite specification, and implicitly contains the same information about how to do the rewrite:

if true 1+1 * 2 else 2+2 fi
*
InjCase(true ; 2; 2+2)
*
InjCase(inl() ; 2; 2+2)
*
2

Note that there are more general descriptive, non-schematic methods for specifying rewrites in proofs, and there are methods for performing rewrites that are justified by semantics of equality beyond simply evaluation and definition. These are not discussed here.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html