Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications

Reflection, the capacity to represent our ideas and to make them the object of our own thoughts, has for many centuries been recognized as a key mark of human intelligence. Clavel's book proposes a general theory of reflective logics and reflective declarative programming languages, that provides a conceptual foundation for judging the extent to which a computational system is reflective. Applying this general framework, Clavel makes an in depth study of reflection in rewriting logic. This book presents examples of the powerful potential for reflective programming in a number of novel computer applications.

The very success and extension of reflective ideas in logic and computer science underscores the need for conceptual foundations. In this book, Clavel proposes axiomatic notions for reflective logics and reflective declarative programming languages. The key concept is the notion of a “universal theory” that can simulate the deductions of all other theories in a logic. This axiomatization unifies different strands of research in reflection, including reflective functional, equational, Horn logic, and rewriting logic programming languages. Based on these universal metalogical axioms, Clavel investigates reflection in rewriting logic at both the theoretical and at the practical level. Providing a fully detailed proof of the reflective nature of rewriting logic, Clavel then gives examples of the useful and powerful properties of this reflective nature in a wide range of computer applications.

All these applications are developed using the Maude language, a reflective programming language and environment that implements rewriting logic and supports its reflective capabilities. These examples demonstrate the power of Maude to define and execute mappings of logics, and to represent and execute different languages and models of computation. Clavel also proposes a general method to easily build theorem proving tools in Maude, with examples.

Manuel Clavel is Assistant Professor of Logic at the University of Narre, Spain, and is a consultant at the Computer Science Laboratory of SRI, International.

Introduction

1 General Logics and Rewriting Logic

1.1 General Logics

1.1.1 Syntax
1.1.2 Entailment Systems
1.1.3 Institutions
1.1.4 Logics
1.1.5 Proof Calculli
1.1.6 Generalized Proof Subcalculi
1.1.7 Declarative Languages

1.2 Rewriting Logic

1.2.1 Preliminaries on Σ-algebras, Substituion, and Contexts
1.2.2 The Rules of Rewriting Logic
1.2.3 An Equivalent Proof System
1.2.4 The Meaning of Rewriting Language

1.3 Maude Language

1.3.1 Functional Modules
1.3.2 System Modules
1.3.3 The Semantics of Maude

2 Reflection in General Logics and in Rewriting Logics

2.1 Axiomiatizing Reflective Logics and Declarative Languages

2.1.1 Metainterpreters for Declarative Languages

2.2 Reflective Declarative Languages

2.2.1 Functional Languages
2.2.2 Equational Languages
2.2.3 Horn Logic Languages
2.2.4 Rewriting Logic Languages
2.2.5 Turing Machines

2.3 Internal versus External Strategies
2.4 Reflection in Rewriting Logic

2.4.1 A UUL‾-Universal Theory
2.4.2 A UUL-Universal Theory

3 Reflection and Strategies in Maude

3.1 A Reflective Kernal in Maude

3.1.1 Matarepresenting Terms
3.1.2 Matarepresenting Modules
3.1.3 The Metalevel Functions

3.2 Internal Strategies in Maude

3.2.1 The Module STRATEGY
3.2.2 The Module META-INTERPRETER

4 Applications of Reflective Maude

4.1 Maude as a Metalogical Translator

4.1.1 A Reified Map from Linear Logic to Rewriting Logic

4.2 Maude as a Semantic Framework

4.2.1 An Executable Representation of CCS

4.3 Building Theorem Provers in Maude

4.3.1 A Knuth-Bendix Completion Checker
4.3.2 An Inductive Theorem Prover

5 Conclusion

A Proofs of Auxiliary Lemmas

Bibliography
Index

10/1/2000

ISBN (Paperback — OUT OF PRINT): 1575862387 (9781575862385)
ISBN (Cloth — OUT OF PRINT): 1575862379 (9781575862378)
ISBN (Electronic): 1575869144 (9781575869148)

Reflection in Rewriting Logic

Contents