Rewriting, and equational unification: The higher-order cases

Abstract

We give here a general definition of term rewriting in the simply typed λ-calculus, and use it to define higher-order forms of term rewriting systems, 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.