Unification via Explicit Substitutions: The Case of Higher-Order Patterns.

Abstract

Following the general method and related completeness results on using explicit substitutions to perform higher-order unification proposed in [5], we investigate in this paper the case of higher-order patterns as introduced by Miller. We show that our general algorithm specializes in a very convenient way to patterns. We also sketch an efficient implementation of the abstract algorithm and its generalization to constraint simplification. 1 Introduction Typed -calculi of various sorts are used pervasively in logical frameworks and their implementations (e.g., Prolog [16], Isabelle [19], or Elf [22]) and in general reasoning systems such as Coq or Nuprl. Unlike functional programming languages, these implementations require access to the body of -terms for such operations as substitution, normalization, matching, or unification. Their efficient implementation is therefore a central problem in theorem proving and higher-order logic programming. While at present there is no conclusive evi...