Z. Qian FB3 Informatik, Universitat Bremen, Bremen, Germany
Higher-order patterns are simply typed [lambda]-terms in long [beta]-normal form where the arguments of a free variable are always [eta]-equal to distinct bound variables. It has been proved that unification of higher-order patterns modulo [alpha], [beta], and [eta] reductions in the simply typed [lambda]-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.
: Higher-order unification, complexity of unification.
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Last updated 23 Jul 96
Part of the OUP Journals World Wide Web service.
Copyright Oxford University Press, 1996