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)