Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. Information and Computation 157, 183–235 (2000)
Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case for higher-order patterns. Technical Report 3591, INRIA (December 1998)
Huet, G.: A unification algorithm for typed λ-calculus. Theoretical Computer Science 1, 27–57 (1975)
Liang, C., Nadathur, G., Qi, X.: Choices in representation and reduction strategies for lambda terms in intensional contexts. Journal of Automated Reasoning 33, 89–132 (2005)
Michaylov, S., Pfenning, F.: An empirical study of the runtime behavior of higher-order logic programs. In: Conference Record of the Workshop on the λProlog Programming Language, Philadelphia, July-August (1992)
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation 1(4), 497–536 (1991)
Miller, D.: Unification under a mixed prefix. Journal of Symbolic Computation 14, 321–358 (1992)
Nadathur, G., Linnell, N.: An SML implementation of higher-order pattern unification, Source code available from the first author’s web page (January 2004)
Nadathur, G., Miller, D.: An overview of λProlog. In: Bowen, K.A., Kowalski, R.A. (eds.) Fifth International Logic Programming Conference, August 1988, pp. 810–827. MIT Press, Cambridge (1988)
Nadathur, G., Mitchell, D.J.: System description: Teyjus—a compiler and abstract machine based implementation of λProlog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)
Nipkow, T.: Higher-order critical pairs. In: Proc. 6th IEEE Symp. Logic in Computer Science, pp. 342–349. IEEE Press, Los Alamitos (1991)
Nipkow, T.: Functional unification of higher-order patterns. In: Eighth Annual IEEE Symposium on Logic in Computer Science, June 1993, pp. 64–74. IEEE Computer Society Press, Los Alamitos (1993)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Pfenning, F.: Logic programming in the LF logical framework. In: Huet, G., Plotkin, G.D. (eds.) Logical Frameworks. Cambridge University Press, Cambridge (1991)
Pfenning, F.: Unification and anti-unification in the Calculus of Constructions. In: Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 74–85 (1991)
Pfenning, F., Schürmann, C.: System description: Twelf — a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Pientka, B., Pfenning, F.: Optimizing higher-order pattern unification. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 473–487. Springer, Heidelberg (2003)
Qian, Z.: Unification of higher-order patterns in linear time and space. Journal of Logic and Computation 6(3), 315–341 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nadathur, G., Linnell, N. (2005). Practical Higher-Order Pattern Unification with On-the-Fly Raising. In: Gabbrielli, M., Gupta, G. (eds) Logic Programming. ICLP 2005. Lecture Notes in Computer Science, vol 3668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562931_28
Download citation
DOI: https://doi.org/10.1007/11562931_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29208-1
Online ISBN: 978-3-540-31947-4
eBook Packages: Computer ScienceComputer Science (R0)