The aim of this research paper is to study in close detail, and to clarify in
some extent, the relationships between two well known approaches to rewriting as
logical deduction, namely, José Meseguer's rewriting logic, and the
constructor-based rewriting logic developed by Mario Rodríguez Artalejo's
research group in Madrid.
The first of these was proposed as a logical framework wherein to represent other logics, and also as a semantic framework for the specification of languages and systems. The experience accumulated throughout the last years has come to support that original intention, having been shown that rewriting logic is a very flexible framework in which many other logics, including first-order logic, intuitionistic logic, linear logic, Horn logic with equality, as well as any other logic with a sequent calculus, can be represented. An important characteristic of these representations that should be stressed is that they are usually quite simple and natural, so that their mathematical properties are often straightforward to derive.
On the other hand, the goal of the constructor-based rewriting logic is to serve as a logical basis for declarative programming languages involving lazy evaluation, offering support, in addition, to nondeterministic functions.
A suitable framework in which to carry out our study is the theory of general logics developed by Meseguer. There, a logic is described in a very abstract manner and two separated components are distinguished in it: an entailment system and an institution, corresponding with the syntantic and the semantic parts of the logic, respectively. Ideally, we would like to find entailment systems and institutions associated to the logics under our consideration so as to be able to define suitable mappings between them; unfortunately, this will prove to be not possible in all cases, and in those occasions we will be forced to leave this formal framework.
Our interest throughout this work will be mainly focused on the simplest versions of both logics, corresponding to an untyped situation. Nevertheless we will also introduce some of their possible extensions in order to point out how our methods could be adapted to deal with more general cases. (Actually, rewriting logic is parameterized by an underlying equational logic, which can vary from the very simple unsorted and unconditional one with which we will be mostly concerned, to the very expressive membership equational logic.)
The final part of this paper tries to contribute with some practical work to the theoretical developments of previous sections. The idea is to define abstract datatypes for the finitely presentable theories in both Meseguer's and Rodríguez-Artalejo's logics, as well as a function mapping theories in this last logic to theories in rewriting logic simulating their behaviour. This function can be defined equationally, and so can be specified in the Maude language associated to rewriting logic, which will allow us to prototype and execute any constructor-based rewriting logic theory.
(BibTeX entry) (gzip'ed Postscript)