{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:32:49Z","timestamp":1784845969833,"version":"3.55.0"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,9,30]],"date-time":"2021-09-30T00:00:00Z","timestamp":1632960000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,9,30]],"date-time":"2021-09-30T00:00:00Z","timestamp":1632960000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2022,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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<jats:italic>pattern<\/jats:italic>subset of higher-order unification was designed to be a small extension to first-order unification that respects the laws governing<jats:italic>\u03bb<\/jats:italic>-binding (i.e., the equalities for<jats:italic>\u03b1<\/jats:italic>,<jats:italic>\u03b2<\/jats:italic>, and<jats:italic>\u03b7<\/jats:italic>-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\u2019s 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.<\/jats:p>","DOI":"10.1007\/s10472-021-09774-y","type":"journal-article","created":{"date-parts":[[2021,9,30]],"date-time":"2021-09-30T15:10:01Z","timestamp":1633014601000},"page":"455-479","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Functions-as-constructors higher-order unification: extended pattern unification"],"prefix":"10.1007","volume":"90","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3261-0180","authenticated-orcid":false,"given":"Tomer","family":"Libal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,9,30]]},"reference":[{"key":"9774_CR1","unstructured":"The Twelf project. http:\/\/twelf.org\/ (2016)"},{"key":"9774_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A., Pientka, B.: Higher-order dynamic pattern unification for dependent types and records. In: Typed Lambda Calculi and Applications, pp 10\u201326. Springer (2011)","DOI":"10.1007\/978-3-642-21691-6_5"},{"key":"9774_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013664. Springer (1986)","DOI":"10.1007\/3-540-16780-3_128"},{"key":"9774_CR4","doi-asserted-by":"crossref","unstructured":"Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: Crafting a Proof Assistant. In: Types for Proofs and Programs, pp 18\u201332. Springer (2006)","DOI":"10.1007\/978-3-540-74464-1_2"},{"key":"9774_CR5","doi-asserted-by":"crossref","unstructured":"Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: Hints in Unification. In: International Conference on Theorem Proving in Higher Order Logics, pp 84\u201398. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03359-9_8"},{"key":"9774_CR6","unstructured":"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)"},{"key":"9774_CR7","volume-title":"The Lambda Calculus: Its Syntax and Semantics, Volume 103 of Studies in Logic and the Foundations of Mathematics","author":"H Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, Volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier, New York (1984)"},{"key":"9774_CR8","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO \u2013 a Higher Order Theorem Prover. In: 15Th Conf. on Automated Deduction (CADE), pp 139\u2013144 (1998)","DOI":"10.1007\/BFb0054256"},{"key":"9774_CR9","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical Big Operators. In: Theorem Proving in Higher Order Logics, Montreal, Canada (2008)","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"9774_CR10","doi-asserted-by":"crossref","unstructured":"Bove, A., Dybjer, P., Norell, U.: A Brief Overview of Agda - A Functional Language with Dependent Types. In: TPHOLs, vol. 5674, pp 73\u201378. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"9774_CR11","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Satallax: An Automatic Higher-Order Prover. In: Automated Reasoning, pp 111\u2013117. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"9774_CR12","doi-asserted-by":"crossref","unstructured":"Church, A.: A formulation of the Simple Theory of Types. J of Symbolic Logic (1940)","DOI":"10.2307\/2266170"},{"key":"9774_CR13","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/BF00630923","volume":"14","author":"M Dalrymple","year":"1991","unstructured":"Dalrymple, M., Shieber, S.M., Pereira, F.C.N.: Ellipsis and higher-order unification. Linguist. Philosop. 14, 399\u2013452 (1991)","journal-title":"Linguist. Philosop."},{"issue":"1","key":"9774_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00141-2","volume":"206","author":"D Duggan","year":"1998","unstructured":"Duggan, D.: Unification with extended patterns. Theor. Comput. Sci. 206(1), 1\u201350 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"9774_CR15","doi-asserted-by":"crossref","unstructured":"Fettig, R., L\u00f6chner, B.: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In: RTA 1996, LNCS, pp 347\u2013361 (1103)","DOI":"10.1007\/3-540-61464-8_64"},{"key":"9774_CR16","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W Goldfarb","year":"1981","unstructured":"Goldfarb, W.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225\u2013230 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"9774_CR17","doi-asserted-by":"publisher","first-page":"1125","DOI":"10.1017\/S0960129518000427","volume":"29.8","author":"F Guidi","year":"2019","unstructured":"Guidi, F., Coen, C.S., Tassi, E.: Implementing type theory in higher order constraint logic programming. Math. Struct. Comput. Sci. 29.8, 1125\u20131150 (2019)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9774_CR18","doi-asserted-by":"crossref","unstructured":"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\u201328 (2017)","DOI":"10.1145\/3110266"},{"key":"9774_CR19","unstructured":"Makoto, H.: A functional implementation of function-as-constructor higher-order unification. In: Proc. 31st International Workshop on Unification (UNIF\u201917) (2017)"},{"key":"9774_CR20","unstructured":"Hamana, M., Abe, T., Murase, Y., Sakaguchi, K.: The System SOL: Second-Order Laboratory. In: 6th International Workshop on Confluence (2020)"},{"key":"9774_CR21","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G Huet","year":"1973","unstructured":"Huet, G.: The undecidability of unification in third order logic. Inf. Control. 22, 257\u2013267 (1973)","journal-title":"Inf. Control."},{"key":"9774_CR22","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed \u03bb-calculus. Theor. Comput. Sci. 1, 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"9774_CR23","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G Huet","year":"1978","unstructured":"Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Informatica 11, 31\u201355 (1978)","journal-title":"Acta Informatica"},{"key":"9774_CR24","unstructured":"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)"},{"issue":"1","key":"9774_CR25","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R McDowell","year":"2002","unstructured":"McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. on Computational Logic 3(1), 80\u2013136 (2002)","journal-title":"ACM Trans. on Computational Logic"},{"issue":"4","key":"9774_CR26","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation 1(4), 497\u2013536 (1991)","journal-title":"J. of Logic and Computation"},{"key":"9774_CR27","doi-asserted-by":"crossref","unstructured":"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\u2013255 (1986)","DOI":"10.3115\/981131.981165"},{"issue":"4","key":"9774_CR28","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14 (4), 321\u2013358 (1992)","journal-title":"J. Symb. Comput."},{"key":"9774_CR29","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order logic. Cambridge University Press, Cambridge (2012)"},{"issue":"3","key":"9774_CR30","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/s00165-016-0393-z","volume":"29","author":"D Miller","year":"2017","unstructured":"Miller, D.: Proof checking and logic programming. Form. Asp. Comput. 29(3), 383\u2013399 (2017)","journal-title":"Form. Asp. Comput."},{"key":"9774_CR31","first-page":"287","volume":"1632","author":"G Nadathur","year":"1999","unstructured":"Nadathur, G., Mitchell, D.J.: System description: Teyjus \u2013 A compiler and abstract machine based implementation of \u03bb prolog. CADE 16, LNAI 1632, 287\u2013291 (1999)","journal-title":"CADE 16, LNAI"},{"key":"9774_CR32","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Functional unification of higher-order patterns. In: Vardi, M. (ed.) 8th Symp. on Logic in Computer Science, pp 64\u201374. IEEE (1993)","DOI":"10.1109\/LICS.1993.287599"},{"key":"9774_CR33","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Markus, W.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS. Springer, Berlin (2002)"},{"key":"9774_CR34","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Unification and anti-unification in the Calculus of Constructions. In: Kahn, G. (ed.) 6th Symp. on Logic in Computer Science, pp 74\u201385. IEEE (1991)","DOI":"10.1109\/LICS.1991.151632"},{"key":"9774_CR35","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2013 A meta-logical framework for deductive systems. CADE 16, LNAI 1632, pp. 202\u2013206 Trento (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"key":"9774_CR36","doi-asserted-by":"crossref","unstructured":"Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR, LNCS, vol. 6173, pp 15\u201321 (2010)","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"9774_CR37","unstructured":"Qi, X., Gacek, A., Holte, S., Nadathur, G., Snow, Z.: The Teyjus system \u2013 version 2. http:\/\/teyjus.cs.umn.edu\/ (2015)"},{"key":"9774_CR38","doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H.: Minlog. In: Wiedijk, F. (ed.) The Seventeen Provers of the World, volume 3600 of LNCS, pp 151\u2013157. Springer (2006)","DOI":"10.1007\/11542384_19"},{"issue":"1-2","key":"9774_CR39","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W Snyder","year":"1989","unstructured":"Snyder, W., Gallier, J.H.: Higher order unification revisited: Complete sets of transformations. J. Symb. Comput. 8(1-2), 101\u2013140 (1989)","journal-title":"J. Symb. Comput."},{"key":"9774_CR40","unstructured":"Tassi, E.: Private communication (Unknown Month 2016)"},{"key":"9774_CR41","unstructured":"Tiu, A.F.: An extension of L-lambda unification http:\/\/www.ntu.edu.sg\/home\/atiu\/llambdaext.pdf (2002)"},{"key":"9774_CR42","doi-asserted-by":"crossref","unstructured":"Qian, Z.: Linear Unification of Higher-Order Patterns. Proc. Coll. Trees in Algebra and Programming (1993)","DOI":"10.1007\/3-540-56610-4_78"},{"key":"9774_CR43","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, 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\u00fcr Informatik (2020)","DOI":"10.46298\/lmcs-17(4:18)2021"},{"key":"9774_CR44","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/j.ipl.2003.12.008","volume":"89.6","author":"T Yokoyama","year":"2004","unstructured":"Yokoyama, T., Hu, Z., Takeichi, M.: Deterministic second-order patterns. Inform. Process. Lett. 89.6, 309\u2013314 (2004)","journal-title":"Inform. Process. Lett."},{"key":"9774_CR45","volume-title":"Deterministic Higher-Order patterns for program transformation international symposium on Logic-Based program synthesis and transformation","author":"Y Tetsuo","year":"2004","unstructured":"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)"},{"issue":"5","key":"9774_CR46","first-page":"71","volume":"21","author":"Y Tetsuo","year":"2004","unstructured":"Tetsuo, Y., Hu, Z., Takeichi, M.: Deterministic second-order patterns for program transformation. Comput. Softw. 21(5), 71\u201376 (2004). In Japanese","journal-title":"Comput. Softw."},{"key":"9774_CR47","doi-asserted-by":"crossref","unstructured":"Ziliani, B., Sozeau, M.: A unification algorithm for Coq featuring universe polymorphism and overloading. ICFP, 179\u2013191 (2015)","DOI":"10.1145\/2858949.2784751"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-021-09774-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-021-09774-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-021-09774-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T02:48:27Z","timestamp":1725850107000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-021-09774-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,30]]},"references-count":47,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["9774"],"URL":"https:\/\/doi.org\/10.1007\/s10472-021-09774-y","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,30]]},"assertion":[{"value":"10 September 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 September 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}