Non-determinsitic algebraic rewriting as adjunction

TL;DR

This paper introduces a general model theoretic framework for algebraic rewriting that handles non-determinism, extending traditional assumptions, and demonstrates its soundness, completeness, and modularity in computational models.

Contribution

It develops a novel semantics for algebraic rewriting using preordered algebra and characterizes rewriting as a persistent adjunction, advancing the theoretical understanding of non-deterministic rewriting.

Findings

Proves soundness and completeness of an abstract rewriting model

Characterizes algebraic rewriting as a persistent adjunction

Establishes a modularity result for algebraic rewriting

Abstract

We develop a general model theoretic semantics to rewriting beyond the usual confluence and termination assumptions. This is based on preordered algebra which is a model theory that extends many sorted algebra. In this framework we characterise rewriting in arbitrary algebras rather than term algebras (called algebraic rewriting) as a persistent adjunction and use this result, on the one hand for proving the soundness and the completeness of an abstract computational model of rewriting that underlies the non-deterministic programming with Maude and CafeOBJ, and on the other hand for developing a compositionality result for algebraic rewriting in the context of the pushout-based modularisation technique.