A Reduction Ordering for Higher-Order Terms
Jürgen Avenhaus, Carlos Lorı́a-Sáenz, Joachim Peter Steinbach · 1995
We investigate one of the classical problems of the theory of term rewriting, namely termination. We present an ordering for comparing higher-order terms that can be utilized for testing termination and decreasingness of higher-order conditional term rewriting systems. The ordering relies on a first-order interpretation of higher-order terms and a suitable extension of the RPO.