论文标题
非确定代数重写作为邻接
Non-determinsitic algebraic rewriting as adjunction
论文作者
论文摘要
我们开发了一种通用模型理论语义，以重写通常的汇合和终止假设。这是基于预定的代数，该代数是扩展许多分类代数的模型理论。 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基于下班的模块化技术。
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.
