Archive for the 'Higher-order patterns' Category

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

By Gopalan Nadathur and Natalie Linnell, from ICLP 2005, available from Gopalan Nadathur’s website:

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.


Optimizing higher-order pattern unification

By Brigitte Pientka and Frank Pfenning, from CADE 2003, available from Frank Pfenning’s website:

We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such as linearization, which eliminates many unnecessary occurs-checks. The presented modal framework explains a number of features of the current implementation of higher-order unification in Twelf and provides insight into several optimizations. Experimental results demonstrate significant performance improvement in many example applications of Twelf, including those in the area of proof-carrying code.

Higher-order term indexing using substitution trees

By Brigitte Pientka, from ACM Transactions on Computational Logic, available from Brigitte Pientka’s website:

We present a higher-order term indexing strategy based on substitution trees for simply typed lambda-terms. There are mainly two problems in adapting first-order indexing techniques. First many operations used in building an efficient term index and retrieving a set of candidate terms from a large collection are undecidable in general for higher-order terms. Second, the scoping of variables and binders in the higher-order case presents challenges. The approach taken in this paper is to reduce the problem to indexing linear higher-order
patterns, a decidable fragment of higher-order terms, and delay solving terms outside of this fragment. We present insertion of terms into the index based on computing the most specific linear generalization of two linear higher-order patterns, and retrieval based on matching two linear higher-order patterns. Our theoretical framework maintains that terms are in βη-normal form, thereby eliminating the need to re-normalize and raise terms during insertion and retrieval. Finally, we prove correctness of our presented algorithms. This indexing structure is implemented as part of the Twelf system to speed up the execution of the tabled higher-logic programming interpreter.

Relating higher-order pattern unification and nominal unification

By James Cheney, from UNIF 2005, available from James Cheney’s website:

Higher-order pattern unification and nominal unification are two approaches to unifying modulo some form of α-equivalence (consistent renaming of bound names). The higher-order and nominal approaches seem superficially dissimilar. However, we show that a natural concretion (or name-application) operation for nominal terms can be used to simulate the behavior of higher-order patterns. We describe a form of nominal terms called nominal patterns that includes concretion and for which unification is equivalent to a special case of higher-order pattern unification, and then show that full higher-order pattern unification can be reduced to nominal unification via nominal patterns.

This is one in a series of three papers detailing the precise connection between higher-order pattern unification and nominal unification (they’re essentially “the same thing”).  Levy and Villaret expanded on Cheney’s work, removing the need for the translation to nominal patterns, with the concretion operator.  They demonstrated that higher-order pattern unifiability is preserved under their translation.  However, Dowek and Gabbay took Levy and Villaret’s results further, and came up with a translation where higher-order unifiers are preserved (they also sharpened Levy and Villaret’s result in another direction, by demonstrating that the Dowek/Gabbay translation is optimum, in a certain manner).

EDIT: the Dowek/Gabbay conference paper isn’t yet available, though the material from that paper will be in a journal paper “Permissive nominal terms and their unification” by Dowek, Gabbay and Mulligan, hopefully to appear soon.  If you have access to the ACM academic archive, then the Levy and Villaret paper is available here.