Reflection and metalevel computation

Rewriting logic is reflective in a precise mathematical way, namely, there is a finitely presented rewrite theory $\mathcal{U}$ that is universal in the sense that we can represent in $\mathcal{U}$ any finitely presented rewrite theory $\mathcal{R}$ (including $\mathcal{U}$ itself) as a term $\overline\mathcal{R}$, any terms $t,t'$ in $\mathcal{R}$ as terms $\overline{t}, \overline{t'}$, and any pair $(\mathcal{R}, t)$ as a term $\langle\overline\mathcal{R}, \overline{t}\rangle$, in such a way that we have the following equivalence

$\; \; \mathcal{R} \vdash t \longrightarrow t' \;\;\Leftrightarrow\;\; \mathcal{... ...e{t}\rangle \longrightarrow \langle\overline\mathcal{R}, \overline{t'}\rangle.$

Since $\mathcal{U}$ is representable in itself, we can achieve a ``reflective tower'' with an arbitrary number of levels of reflection:

$\mathcal{R}\vdash t \rightarrow t' \;\Leftrightarrow\; \mathcal{U}\vdash \langl... ...{U}, \overline{\langle\overline\mathcal{R}, \overline{t'}\rangle}\rangle \ldots$

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.

In Maude, key functionality of the universal theory $\mathcal{U}$ has been efficiently implemented in the functional module META-LEVEL. This module includes the modules META-MODULE and META-TERM. As an overview,

• in the module META-TERM, Maude terms are metarepresented as elements of a data type Term of terms;
• in the module META-MODULE, Maude modules are metarepresented as terms in a data type Module of modules; and
• in the module META-LEVEL,
  • operations upModule, upTerm, downTerm, and others allow moving between reflection levels;
  • the process of reducing a term to canonical form using Maude's reduce command is metarepresented by a built-in function metaReduce;
  • the processes of rewriting a term in a system module using Maude's rewrite and frewrite commands are metarepresented by built-in functions metaRewrite and metaFrewrite;
  • the process of applying (without extension) a rule of a system module at the top of a term is metarepresented by a built-in function metaApply;
  • the process of applying (with extension) a rule of a system module at any position of a term is metarepresented by a built-in function metaXapply;
  • the process of matching (without extension) two terms at the top is reified by a built-in function metaMatch;
  • the process of matching (with extension) a pattern to any subterm of a term is reified by a built-in function metaXmatch;
  • the process of searching for a term satisfying some conditions starting in an initial term is reified by built-in functions metaSearch and metaSearchPath; and
  • parsing and pretty-printing of a term in a module, as well as key sort operations such as comparing sorts in the subsort ordering of a signature, are also metarepresented by corresponding built-in functions.

The functions metaReduce, metaApply, metaXapply, metaRewrite, metaFrewrite, metaMatch, and metaXmatch are called descent functions, since they allow us to descend levels in the reflective tower. The paper [15] provides a formal definition of the notion of descent function, and a detailed explanation of how they can be used to achieve a systematic, conservative way of lowering the levels of reflective computations.

The importation graph in Figure 11.1 shows the relationships between all the modules in the metalevel. The modules NAT-LIST and QID-LIST provide lists of natural numbers and quoted identifiers, respectively (see Section 7.12.1), and the module QID-SET provides sets of quoted identifiers (see Section 7.12.2). Notice that QID-SET is imported (in protecting mode) with renaming

  (op empty to none, op _,_ to _;_ [prec 43])#

abbreviated to $\beta$ in the figure.

Figure 11.1: Importation graph of metalevel modules