Unification of λ-terms
The computations that arise in the course of proof search with higher-order logic programs often require finding substitutions for essentially existentially quantified variables that make two different terms λ-convertible. In Chapter 4 we characterized such higher-order unification problems using a mixed quantifier prefix over a “matrix” involving a conjunction of equations. Specifically, unification problems are formulas of the form
where n, m ≥ 0, Qi is either ∀ or ∃ for 1 ≤ i ≤ n and t1, s1,…,tm, sm are λ-terms such that, for 1 ≤ j ≤ m, tj and sj are of the same type. In Chapter 4 we made a distinction between the notion ...