Reflection in rewriting logic. Metalogical foundations and metaprogramming applications (Q2734833)

The author proposes general axiomatic notions of reflective logics based on the theory of general logics. General logics, as developed by Goguen and Burstall and by Meseguer, is a very general framework that contains any given logic as an instance. This allows the author to develop his concepts indepently of any concrete logic.NEWLINENEWLINENEWLINEIntuitively, a logic is called reflective if important aspects of its metatheory (e.g. provability can be expressed at object level). To be more precise, given an entailment system \({\mathcal E}\) and a set of theories \({\mathcal C}\), then \({\mathcal E}\) is \({\mathcal C}\)-reflective iff there is a theory \(U\in{\mathcal C}\) (a universal theory) and a representation function rep such that for all \(T\in{\mathcal C}\) and \(\varphi\in\) sentences\((T)\) we have NEWLINE\[NEWLINET\vdash \varphi\text{ iff }U\vdash \text{ rep}(T, \varphi).NEWLINE\]NEWLINE This notion can be refined for declarative programming languages \({\mathcal L}\). In this case \(U\) is called a metainterpreter for \({\mathcal L}\). Metainterpreters are used to realize internal strategies, i.e., strategies that control the deduction process and can be specified within the logic itself. NEWLINENEWLINENEWLINETo give an example, if \({\mathcal L}\) is the class of Turing programs, then any universal Turing machine is a metainterpreter for \({\mathcal L}\).NEWLINENEWLINENEWLINEThe book first proves in detail that rewriting logic is reflective. Maude is a logical language based on rewriting logic. So the author shows the reflective capabilities of this language. Finally he demonstrates by examples how reflection of rewriting logic can be used in practice to give novel and elegant solutions to important applications. These examples include the demonstration (1) how Maude can be used to define and execute mappings representing a given logic into rewriting logic, (2) how different languages and models of computation can be defined and executed in rewriting logic, and (3) how theorem proving tools for any logic (e.g., testing confluence in equational theories) can be built.