Reflection in rewriting logic. Metalogical foundations and metaprogramming applications.

*(English)*Zbl 1003.03032
Stanford, CA: CSLI Publications. xiv, 200 p. (2000).

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.

Intuitively, 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 \[ T\vdash \varphi\text{ iff }U\vdash \text{ rep}(T, \varphi). \] 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.

To give an example, if \({\mathcal L}\) is the class of Turing programs, then any universal Turing machine is a metainterpreter for \({\mathcal L}\).

The 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.

Intuitively, 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 \[ T\vdash \varphi\text{ iff }U\vdash \text{ rep}(T, \varphi). \] 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.

To give an example, if \({\mathcal L}\) is the class of Turing programs, then any universal Turing machine is a metainterpreter for \({\mathcal L}\).

The 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.

Reviewer: Jürgen Avenhaus (Kaiserslautern)

##### MSC:

03B70 | Logic in computer science |

68-02 | Research exposition (monographs, survey articles) pertaining to computer science |

68Q42 | Grammars and rewriting systems |

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q05 | Models of computation (Turing machines, etc.) (MSC2010) |

68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |