Special Issue on Order-sorted Rewriting: Foreword of the Guest Editor

✍ Scribed by G. Smolka

• Publisher: Elsevier Science
• Year: 1998
• Tongue: English
• Weight: 89 KB
• Volume: 25
• Category: Article
• ISSN: 0747-7171
• DOI: 10.1006/jsco.1998.0184

✦ Synopsis

Equational logic is ubiquitous in computer science. It is the basis for algebraic specification, rewriting, unification, and equational programming. These techniques evolved in a many-sorted setting, where different sorts are disjoint. Joseph Goguen observed that an order-sorted equational logic modelling sort inclusion would yield a more expressive and natural specification language. In the 1980s, Goguen and Meseguer initiated and sponsored an international collaboration on the development of an executable specification language OBJ based on order-sorted equational logic, prompting foundational work on order-sorted rewriting and unification. Order-sorted rewrite systems can be seen as a special class of conditional rewrite systems. As it turns out, the expressiveness of ordersorted logic results in considerable complications as it comes to confluence, critical pair analysis and completion of order-sorted rewrite systems.

The four papers of this special issue are concerned with three different approaches to order-sorted rewriting and completion. They represent the state of the art of the area and show its wealth and depth.

I would like to thank the authors and the referees of the papers for their considerable efforts that have led to this special issue.