Informally, a reflective logic is a logic in which important aspects of its metatheory can be represented at the object level in a consistent way, so that the object-level representation correctly simulates the relevant metatheoretic aspects. In other words, a reflective logic is a logic which can be faithfully interpreted in itself. Maude's language design and implementation make systematic use of the fact that rewriting logic is reflective [14, 15, 10]. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way.
A naive implementation of reflection can be very expensive both in time and memory use. Therefore, a good implementation must provide efficient ways of performing reflective computations. This section explains how this is achieved in Maude through its predefined META-LEVEL module. We first discuss the semantics of metalevel computations, and how their efficiency can be dramatically increased by conservatively extending the universal theory U to a metalevel theory M with descent functions and rules that allow lowering deductions at higher levels of reflection to much more efficient deductions at lower levels. Then, we explain how terms and modules are meta-represented in META-LEVEL, and how these semantic principles are supported in important special cases by the META-LEVEL module in a built-in way.
The important topic of internal strategy languages, that use reflection in an essential way, is discussed separately, in Section 2.6. Besides strategies, reflection makes possible many advanced metaprogramming applications. One important such application is Full Maude which, as discussed later in this document, makes essential use of reflection to provide Maude with a rich and extensible module algebra; this is a special instance of a general class of applications in which, using reflection, we can use Maude as a metalanguage to reify other languages and logics within rewriting logic (see Section 2.8.2). The paper [11] summarizes, and gives references for, a number of other important applications, including uses of rewriting logic as a logical framework and the development of theorem proving tools.