Practical higher-order pattern unification with on-the-fly raising

Gopalan Nadathur, Natalie Linnell

Research output: Contribution to journalConference articlepeer-review

8 Scopus citations


Higher-order pattern unification problems arise often in computations within systems such as Twelf, λProlog and Isabelle. An important characteristic of such problems is that they are given by equations appearing under a prefix of alternating universal and existential quantifiers. Most existing algorithms for solving these problems assume that such prefixes are simplified to a ∀∃∀ form by an a priori application of a transformation known as raising. There are drawbacks to this approach. Mixed quantifier prefixes typically manifest themselves in the course of computation, thereby requiring a dynamic form of preprocessing that is difficult to support in low-level implementations. Moreover, raising may be redundant in many cases and its effect may have to be undone by a subsequent pruning transformation. We propose a method to overcome these difficulties. In particular, a unification algorithm is described that proceeds by recursively descending through the structures of terms, performing raising and other transformations on-the-fly and only as needed.

Original languageEnglish (US)
Pages (from-to)371-386
Number of pages16
JournalLecture Notes in Computer Science
StatePublished - 2005
Event21st International Conference on Logic Programming, ICLP 2005 - Sitges, Spain
Duration: Oct 2 2005Oct 5 2005


Dive into the research topics of 'Practical higher-order pattern unification with on-the-fly raising'. Together they form a unique fingerprint.

Cite this