Volume 6: January - December 1996

Issue 3: June 1996

Abstract


Unification of higher-order patterns in linear time and space

  • Unification of higher-order patterns in linear time and space
  • Z. Qian FB3 Informatik, Universitat Bremen, Bremen, Germany

    ABSTRACT

    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.

    Keywords: Higher-order unification, complexity of unification.

    Pages: 315 - 341

    Part of the OUP Journal of Logic and Computation WWW service


    General Information

    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