MetaPRL Term Rewriting
The MetaPRL term rewriter is easilty the most complex piece of the refiner. Rewrites are defined using second-order substitution. The variable syntax is extended to include variables that specify terms with bound variables, or substitutions. The notation for a second order variable is a variable followed by a list of subterms in brackets: like the following v[t1; t2]. A rewrite is specified in two parts: a redex pattern, and a contractum pattern, and occurrences of second order variables are treated differently by the rewriter. Consider the following example:
rewrite beta : apply{lambda{x. 'b['x]}; 'a} <--> 'b['a]
This rewrite definition is used to define beta-reduction in the lambda-calculus. The redex pattern is the application apply{lambda{x. 'b['x]}; 'a}. There are two second-order variables in the pattern: the variables 'b['x] and 'a. The variable 'b['x] represent a term, with a possible occurrence of a free variable 'x. The variable 'a also represents a term, but without any special occurrences of free variables.
The contractum definition includes the same variables, but the free variable has been replaced by the term represented by 'a. In any rewrite definition, the second order variables in the redex specify matching, and the second-order variables in the contractum specify substitution. In fact, the rewrite definition for beta can be translated to an equaivalent substitution form. Let 'b['x <- 'a] represent substitution of the term 'a for the variable 'x in the term 'b. The beta rewrite is equivalent to the following definition:
rewrite beta : apply{lambda{x. 'b}; 'a} <--> 'b['x <- 'a]
The application of a rewrite is to a a normal term. Redex matching is defined recursively. A redex pattern is either a second-order variable, or it is a term with redex patterns for its subterms. A term pattern matches a (regular) term if the operators are equal, the arities of the subterms are equal, and the subterm patterns match each of the subterms of the (regular) term. A second-order variable 'v['x1; ...; 'xn] matches any term.
When a redex is matched, the values matched by each of the second-order variables are saved, along with renaming for the bound variables. When the contractum is constructed, substituion is used to construct term values for each of the second-order variables in the contractum. For example, suppose we apply the beta rewrite to a specific term
apply{lambda{z. 'y + 'z}; 1}
The redex matching produces the following results:
'a: 'a = 1
'b['x]: ('x = 'z): 'b['x] = 'y + 'x
This table specifies that that variable 'x is renamed to 'z, and term 'b['z] is the body of the lambda: 'y + 'z. The construction of the contractum substitutes the value for 'a (1), for the variable 'x (which has been renamed to 'z), and the result of the application is the term 'y + 1
The difference between the second-order form of a rewrite, and the substitution form arises when multiple occurences of a second order variable occur in a redex pattern. These multiple patterns specify term equivalences. For example, we might define a rewrite that "doubles" its argument:
rewrite double : ('x + 'x) <--> (2 * 'x)
This rewrite uses syntactic equivalence: the following application is valid:
(7 + 7) --> 2 * 7
But the following rewrite fails:
(2 + (1 + 1)) --> fails
The rewriter is implemented in four parts:
These four parts are implemented as separate modules sharing common type definitions, and the result rewriter module Rewrite is constructed by composing the four modules.