Linear unification of higher-order patterns

Abstract

Higher-order patterns are simply typed λ-terms in η-long form where free variables F only occur in the form F(x1, …, xk) with x1, …, Ik being distinct bound variables. It has been proved iu [6] that in the simply typed λ-calculus unification of higher-order patterns modulo α, β and η reductions is decidable and unifiable higher-order patterns have a most general unifier. In this paper a unification algorithm for higher-order patterns is presented, whose time and space complexities are proved to be linear in the size of input.