Notes on Transformation Orderings
Joachim Peter Steinbach · 1999
. An important property and also a crucial point of a term rewriting system is its termination. Transformation orderings, developed by Bellegarde & Lescanne strongly based on a work of Bachmair & Dershowitz, represent a general technique for extending orderings. The main characteristics of this method are two rewriting relations, one for transforming terms and the other for ensuring the well-foundedness of the ordering. The central problem of this approach concerns the choice of the two relations such that the termination of a given term rewriting system can be proved. In this communication, we present a heuristic-based algorithm that partially solves this problem. Furthermore, we show how to simulate well-known orderings on strings by transformation orderings. This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt). 1 Introduction and Notations Term rewriting systems (TRS, for short) are based on directed equations (called rules) which may be used ...