Recursively defined (quasi) orders on terms
M.C.F. Ferreira · 1997
We study the problems involved in the recursive definition of (quasi) orders on terms, focussing on the question of establishing well-definedness, and the properties required for partial and quasi-orders: irreflexivity and transitivity, and reflexivity and transitivity, respectively. These properties are in general difficult to establish and this has in many cases come down in the literature as folklore results. Here we present a general scheme that allows us to show that relations are well-defined and represent partial or quasi-orders. Known path orders as semantic, recursive and lexicographic path order as well as Knuth-Bendix order fit into the scheme. Additionally we will also discuss how to obtain other properties commonly found in term orders (amongst which well-foundedness) as an integrated feature of the scheme. Keywords: Path Orders, term rewriting, semantic path order , recursive path order , lexicographic path order, Knuth-Bendix order . Contents 1 Introduction 2 2 Prelimi...