Unification of higher-order patterns in linear time and space
- 1 June 1996
- journal article
- research article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 6 (3) , 315-341
- https://doi.org/10.1093/logcom/6.3.315
Abstract
Higher-order patterns are simply typed λ-terms in long β-normal form where the arguments of a free variable are always η-equal to distinct bound variables. It has been proved that unification of higher-order patterns modulo α, β and η reductions in the simply typed λ-calculus 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.Keywords
This publication has 0 references indexed in Scilit: