D A Wolfram.
September 1990.
We give here a general definition of term rewriting in the simply typed lambda-calculus, and use it to define higher-order forms of term rewriting systems, narrowing, and equational unification and their properties. This provides a basis for generalizing the first- and restricted higher-order results for these concepts. As examples, we generalize Plotkin's criteria for building-in equational theories, and show that pure third-order equational matching is undecidable. This approach simplifies computations in applications involving lexical scoping, and equations. We discuss open problems and summarize future research directions.