Notes on Transformation Orderings

Joachim Steinbach
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, W-6750 Kaiserslautern, GERMANY
E-mail: steinba@informatik.uni-kl.de

Abstract
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.

Keywords
Termination of Term Rewriting Systems, Reduction Orderings

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1992/papers/
file: Steinbach.SR-92-23.ps.SEKI.Z