Rewriting logic is reflective [14, 10] in a precise mathematical way, namely, there is a finitely presented rewrite theory U that is universal in the sense that we can represent in U any finitely presented rewrite theory R (including U itself) as a term |¯R¯| , any terms t,t' in R as terms |¯t¯| , |¯t'¯| , and any pair (R, t) as a term < |¯R¯| , |¯t¯| >, in such a way that we have the following equivalence
($) R |- t --> t' <=> U |- < |¯R¯| , |¯t¯| > --> < |¯R¯| , |¯t'¯| >.Since U is representable in itself, we can achieve a "reflective tower" with an arbitrary number of levels of reflection, since we have
R |- t -> t' <=> U |- < |¯R¯| , |¯t¯| > -> < |¯R¯| , |¯t'¯| > <=> U |- < |¯U¯| , |¯< |¯R¯| , |¯t¯| >¯| > -> < |¯U¯| , |¯< |¯R¯| , |¯t'¯| >¯| >...In this chain of equivalences we say that the first rewriting computation takes place at level 0, the second at level 1, and so on. In a naive implementation, each step up the reflective tower comes at considerable computational cost, because simulating a single step of rewriting at one level involves many rewriting steps one level up. It is therefore important to have systematic ways of lowering the levels of reflective computations as much as possible--so that a rewriting subcomputation happens at a higher level in the tower only when this is strictly necessary.
To achieve a systematic descent into equivalent rewriting computations at lower levels, the key idea is to exploit the equivalence ($). A detailed proof of this equivalence has been given for the case of unconditional and unsorted theories [10]. The extension to the case of interest for Maude--namely to conditional rewrite theories with membership equational logic [41, 5] as the underlying equational logic--although nontrivial, is essentially unproblematic. We therefore assume a universal theory U for this more general class of finitely presented rewrite theories. In particular, the signature SigmaU of U has sorts Term, Module, and Kind, whose respective elements |¯t¯| : Term, |¯R¯| : Module, and |¯K¯| : Kind represent terms, rewrite theories, and kinds13 in a signature, respectively. We assume that there is also an equationally defined Boolean predicate parse:Module ×Kind ×Term --> Bool so that parse( |¯R¯| , |¯K¯| , |¯t¯| )= true if t is an R-term of kind K, and parse( |¯R¯| , |¯K¯| , |¯t¯| )= false otherwise.
We can exploit the equivalence ($) by introducing the notion of descent function, that is, a function that, given metalevel representations for a rewrite theory R and a term t in it, rewrites such a term in R according to a given strategy and returns the meta-representation of the resulting term. Such functions can be simply expressed in terms of a general sequential interpreter function I for rewriting logic. This is a partial function that takes three arguments: a finitely presented rewrite theory R, a term t, and a deterministic strategy S. In case of termination it returns either the term t' to which t was rewritten according to S, or an error message that is not a term in R. The function is undefined in case the strategy does not terminate. For any finitely presented rewrite theory R, terms t,t' in it, and admissible deterministic strategy S, any such interpreter function must of course satisfy the correctness requirement
(b) I(R,t,S) = t' => R |- t --> t'.The point is that, regardless of the particular details of I, we can always equationally axiomatize any such effective interpreter function by means of a Church-Rosser, but in general nonterminating, finitary equational theory I. This can be done in a signature that we can assume contains SigmaU as a subsignature. By extending our universal theory U with the new sorts, operations, and equations of I, we obtain an extended rewrite theory U U I. A descent function is then a function
d : Module ×Term ×Parameters --> Termsuch that there is a deterministic strategy expression Sd with a single free variable of sort Parameters satisfying the equality
d( |¯R¯| , |¯t¯| ,p) = |¯I(R,t,Sd(p))¯| .Such descent functions are of course easily definable equationally as definitional extensions of the theory U U I. Note that, since we have only added some new equations, the only rewrite rules in U U I are exactly those in U. But, given a descent function d, we can now exploit the equivalence ($) by adding to U U I a descent rule
where M:Module, x,y:Term, K: Kind, and p:Parameters. The equivalence ($) can be exploited for efficiency reasons with such a rule, because the sequential interpreter I can be a built-in function such as the Maude interpreter; therefore, instantiating M with |¯R¯| , we can use efficient deduction in R to perform deduction in U. Let M denote a rewrite theory of the form M = U U I U D, where D is the addition of several descent functions and of their associated descent rules. We shall call M a metalevel theory.
d:<M, x> --> <M, y> if parse(M,K,x)= true /\ parse(M,K,y)= true /\ d(M,x,p)=y.
The addition of descent rules to U is of course conservative, in the sense of not adding any rewrites that could not be performed, albeit less efficiently, in U itself, since for any descent rule d we have14,
Note that, by applying several descent functions, we can descend several levels in the reflective tower. Assume that M includes descent functions d and d', and let R and t be an arbitrary rewrite theory and a term in it; then we have, for example,
M |- < |¯R¯| , |¯t¯| > --> d < |¯R¯| , |¯t'¯| > => I(R,t,Sd(p)) = t' => b R |- t --> t' <=> $ U |- < |¯R¯| , |¯t¯| > --> < |¯R¯| , |¯t'¯| >.
That is, a meta-metalevel computation can be efficiently carried out at the object level. An example of this kind of combined descent is given in Section 3.3. More generally, we should view descent functions as basic strategies, that can be used as fundamental building blocks to define internal strategy languages [16, 10], in which they can be combined with each other and with more complex strategies at several levels of reflection to perform efficiently sophisticated metalevel computations (see section 2.6).
d( |¯M¯| , |¯d'( |¯R¯| , |¯t¯| ,p')¯| ,p) = |¯I(M,d'( |¯R¯| , |¯t¯| ,p'),Sd(p))¯| = |¯I(M, |¯I(R,t,Sd'(p'))¯| ,Sd(p))¯| .