<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>13</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">José Bernardo Barros</style></author><author><style face="normal" font="default" size="100%">Joseph Goguen</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Semantics of Non-terminating Rewrite Systems using Minimal Coverings</style></title><tertiary-title><style face="normal" font="default" size="100%">PRG Technical Monographs</style></tertiary-title></titles><dates><year><style  face="normal" font="default" size="100%">1995</style></year><pub-dates><date><style  face="normal" font="default" size="100%">March</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jbb/files/prg118.pdf</style></url></related-urls></urls><number><style face="normal" font="default" size="100%">PRG-118</style></number><publisher><style face="normal" font="default" size="100%">Programming Research Group, Oxford University</style></publisher><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;We propose a new semantics for rewrite systems based on interpreting rewrite rules as inequations between terms in an ordered algebra. In particular, we show that the algebra of normal forms in a terminating system is a uniquely minimal covering of the term algebra. In the non-terminating case, the existence of this minimal covering is established in the completion of an ordered algebra formed by rewriting sequences. We thus generalize the properties of normal forms for non-termination systems to this minimal covering. These include the existence of normal forms for arbitrary rewrite systems, and their uniqueness for confluent systems, in which case the algebra of normal forms is isomorphic to the canonical quotient algebra associated with the rules when seen as equations. This extends the benefits of algebraic semantics to systems with non-deterministic and non-terminating computations. We first study properties of abstract orders and then instantiate these to term rewriting systems.&lt;/p&gt;
</style></abstract></record></records></xml>