Non-determinsitic algebraic rewriting as adjunction
Logic
2022-04-27 v1 Computation and Language
Logic in Computer Science
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.
Cite
@article{arxiv.2204.12133,
title = {Non-determinsitic algebraic rewriting as adjunction},
author = {Răzvan Diaconescu},
journal= {arXiv preprint arXiv:2204.12133},
year = {2022}
}