A Reduction Ordering for Higher-Order Terms

Juergen Avenhaus, Carlos Loria-Saenz, Joachim Steinbach
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, GERMANY
E-mail: avenhaus@informatik.uni-kl.de

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

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1995/
file: Avenhaus.SR-95-03.ps.gz