A comparison between two logical formalisms for rewriting

TL;DR

This paper compares Meseguer's rewriting logic and CRWL, analyzing their syntactic and semantic relationships, and demonstrates their mutual simulation despite differences in entailment systems.

Contribution

It provides a detailed comparison of two rewriting formalisms, establishing their mutual simulation and generalizing entailment and satisfaction notions.

Findings

Both formalisms can be simulated in each other.

No embedding exists between their institutions.

Generalized notions of entailment and satisfaction are introduced.

Abstract

Meseguer's rewriting logic and the rewriting logic CRWL are two well-known approaches to rewriting as logical deduction that, despite some clear similarities, were designed with different objectives. Here we study the relationships between them, both at a syntactic and at a semantic level. Even though it is not possible to establish an entailment system map between them, both can be naturally simulated in each other. Semantically, there is no embedding between the corresponding institutions. Along the way, the notions of entailment and satisfaction in Meseguer's rewriting logic are generalized. We also use the syntactic results to prove reflective properties of CRWL.