Iterative lexicographic path orders

Vincent van Oostrom

Roel de Vrijer

pp. 541-554

in: Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer (eds), Algebra, meaning, and computation, Berlin, Springer, 2006

Abstract

We relate Kamin and Lévy's original presentation of lexicographic path orders (LPO), using an inductive definition, to a presentation, which we will refer to as iterative lexicographic path orders (ILPO), based on Bergstra and Klop's definition of recursive path orders by way of an auxiliary term rewriting sytem.