Abstract
Unification is a central operation in constructing a range of computational logic systems based on first-order and higher-order logics. First-order unification has several properties that guide its incorporation in such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respects the laws governing λ-binding (i.e., the equalities for α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been used in numerous implemented systems and in various theoretical settings, it is too weak for many applications. This paper defines an extension of pattern unification that should make it more generally applicable, especially in proof assistants that allow for higher-order functions. This extension’s main idea is that the arguments to a higher-order, free variable can be more than just distinct bound variables. In particular, such arguments can be terms constructed from (sufficient numbers of) such bound variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
The Twelf project. http://twelf.org/ (2016)
Abel, A., Pientka, B.: Higher-order dynamic pattern unification for dependent types and records. In: Typed Lambda Calculi and Applications, pp 10–26. Springer (2011)
Andrews, P.B., Pfenning, F., Issar, S., Klapper, C.P.: The TPS theorem proving system. In: Siekmann, J.H. (ed.) CADE 8, LNCS 230, pp 663–664. Springer (1986)
Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: Crafting a Proof Assistant. In: Types for Proofs and Programs, pp 18–32. Springer (2006)
Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: Hints in Unification. In: International Conference on Theorem Proving in Higher Order Logics, pp 84–98. Springer, Berlin (2009)
Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: A system for reasoning about relational specifications. J. of Formalized Reasoning (2014)
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, Volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier, New York (1984)
Benzmüller, C., Kohlhase, M.: LEO – a Higher Order Theorem Prover. In: 15Th Conf. on Automated Deduction (CADE), pp 139–144 (1998)
Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical Big Operators. In: Theorem Proving in Higher Order Logics, Montreal, Canada (2008)
Bove, A., Dybjer, P., Norell, U.: A Brief Overview of Agda - A Functional Language with Dependent Types. In: TPHOLs, vol. 5674, pp 73–78. Springer (2009)
Brown, C.E.: Satallax: An Automatic Higher-Order Prover. In: Automated Reasoning, pp 111–117. Springer (2012)
Church, A.: A formulation of the Simple Theory of Types. J of Symbolic Logic (1940)
Dalrymple, M., Shieber, S.M., Pereira, F.C.N.: Ellipsis and higher-order unification. Linguist. Philosop. 14, 399–452 (1991)
Duggan, D.: Unification with extended patterns. Theor. Comput. Sci. 206(1), 1–50 (1998)
Fettig, R., Löchner, B.: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In: RTA 1996, LNCS, pp 347–361 (1103)
Goldfarb, W.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225–230 (1981)
Guidi, F., Coen, C.S., Tassi, E.: Implementing type theory in higher order constraint logic programming. Math. Struct. Comput. Sci. 29.8, 1125–1150 (2019)
Hamana, M.: How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. In: Proceedings of the ACM on Programming Languages 1.ICFP, pp 1–28 (2017)
Makoto, H.: A functional implementation of function-as-constructor higher-order unification. In: Proc. 31st International Workshop on Unification (UNIF’17) (2017)
Hamana, M., Abe, T., Murase, Y., Sakaguchi, K.: The System SOL: Second-Order Laboratory. In: 6th International Workshop on Confluence (2020)
Huet, G.: The undecidability of unification in third order logic. Inf. Control. 22, 257–267 (1973)
Huet, G.: A unification algorithm for typed λ-calculus. Theor. Comput. Sci. 1, 27–57 (1975)
Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Informatica 11, 31–55 (1978)
Libal, T., Miller, D.: Functions-as-constructors higher-order unification. In: Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (2016)
McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. on Computational Logic 3(1), 80–136 (2002)
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation 1(4), 497–536 (1991)
Miller, D., Nadathur, G.: Some uses of higher-order logic in computational linguistics. In: Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pp 247–255 (1986)
Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14 (4), 321–358 (1992)
Miller, D., Nadathur, G.: Programming with Higher-Order logic. Cambridge University Press, Cambridge (2012)
Miller, D.: Proof checking and logic programming. Form. Asp. Comput. 29(3), 383–399 (2017)
Nadathur, G., Mitchell, D.J.: System description: Teyjus – A compiler and abstract machine based implementation of λ prolog. CADE 16, LNAI 1632, 287–291 (1999)
Nipkow, T.: Functional unification of higher-order patterns. In: Vardi, M. (ed.) 8th Symp. on Logic in Computer Science, pp 64–74. IEEE (1993)
Nipkow, T., Paulson, L.C., Markus, W.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS. Springer, Berlin (2002)
Pfenning, F.: Unification and anti-unification in the Calculus of Constructions. In: Kahn, G. (ed.) 6th Symp. on Logic in Computer Science, pp 74–85. IEEE (1991)
Pfenning, F., Schürmann, C.: System description: Twelf – A meta-logical framework for deductive systems. CADE 16, LNAI 1632, pp. 202–206 Trento (1999)
Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Giesl, J., Hähnle, R. (eds.) IJCAR, LNCS, vol. 6173, pp 15–21 (2010)
Qi, X., Gacek, A., Holte, S., Nadathur, G., Snow, Z.: The Teyjus system – version 2. http://teyjus.cs.umn.edu/ (2015)
Schwichtenberg, H.: Minlog. In: Wiedijk, F. (ed.) The Seventeen Provers of the World, volume 3600 of LNCS, pp 151–157. Springer (2006)
Snyder, W., Gallier, J.H.: Higher order unification revisited: Complete sets of transformations. J. Symb. Comput. 8(1-2), 101–140 (1989)
Tassi, E.: Private communication (Unknown Month 2016)
Tiu, A.F.: An extension of L-lambda unification http://www.ntu.edu.sg/home/atiu/llambdaext.pdf (2002)
Qian, Z.: Linear Unification of Higher-Order Patterns. Proc. Coll. Trees in Algebra and Programming (1993)
Vukmirović, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2020)
Yokoyama, T., Hu, Z., Takeichi, M.: Deterministic second-order patterns. Inform. Process. Lett. 89.6, 309–314 (2004)
Tetsuo, Y., Hu, Z., Takeichi, M.: Deterministic Higher-Order patterns for program transformation international symposium on Logic-Based program synthesis and transformation. Springer, Berlin (2004)
Tetsuo, Y., Hu, Z., Takeichi, M.: Deterministic second-order patterns for program transformation. Comput. Softw. 21(5), 71–76 (2004). In Japanese
Ziliani, B., Sozeau, M.: A unification algorithm for Coq featuring universe polymorphism and overloading. ICFP, 179–191 (2015)
Acknowledgements
We thank Enrico Tassi, Tetsuo Yokoyama and Makoto Hamana for discussions related to this paper. We benefited greatly from the many comments of the anonymous reviewers of an earlier draft as well as of the current draft of this paper. This work has been funded by the ERC Advanced Grant ProofCert.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Libal, T., Miller, D. Functions-as-constructors higher-order unification: extended pattern unification. Ann Math Artif Intell 90, 455–479 (2022). https://doi.org/10.1007/s10472-021-09774-y
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-021-09774-y