Higher order unification via explicit substitutions. (English) Zbl 1005.03016

Summary: Higher order unification is equational unification for \(\beta\eta\)-conversion. But it is not first order equational unification, as substitution has to avoid capture. Thus, the methods for equational unification (such as narrowing) built upon grafting (i.e., substitution without renaming) cannot be used for higher order unification, which needs specific algorithms. Our goal in this paper is to reduce higher order unification to first order equational unification in a suitable theory. This is achieved by replacing substitution by grafting, but this replacement is not straightforward as it raises two major problems. First, some unification problems have solutions with grafting but no solution with substitution. Then equational unification algorithms rest upon the fact that grafting and reduction commute. But grafting and \(\beta\eta\)-reduction do not commute in \(\lambda\)-calculus and reducing an equation may change the set of its solutions. This difficulty comes from the interaction between the substitutions initiated by \(\beta\eta\)-reduction and the ones initiated by the unification process. Two kinds of variables are involved: those of \(\beta\eta\)-conversion and those of unification. So, we need to set up a calculus which distinguishes between these two kinds of variables and such that reduction and grafting commute. For this purpose, the application of a substitution of a reduction variable to a unification one must be delayed until this variable is instantiated. Such a separation and delay are provided by a calculus of explicit substitutions. Unification in such a calculus can be performed by well-known algorithms such as narrowing, but we present a specialised algorithm for greater efficiency. At last we show how to relate unification in \(\lambda\)-calculus and in a calculus with explicit substitutions. Thus, we come up with a new higher order unification algorithm which eliminates some burdens of the previous algorithms, in particular the functional handling of scopes. Huet’s algorithm can be seen as a specific strategy for our algorithm, since each of its steps can be decomposed into elementary ones, leading to a more atomic description of the unification process. Also, solved forms in \(\lambda\)-calculus can easily be computed from solved forms in \(\lambda\sigma\)-calculus.


03B40 Combinatory logic and lambda calculus
03B15 Higher-order logic; type theory (MSC2010)
03B35 Mechanization of proofs and logical operations
68Q42 Grammars and rewriting systems


Automath; ETPS
Full Text: DOI Link


[1] Abadi, M.; Cardelli, L.; Curien, P.L.; Lévy, J.J., Explicit substitutions, J. functional programming, 1, 375-416, (1991) · Zbl 0941.68542
[2] Andrews, P.B., Resolution in type theory, J. symbolic logic, 36, 414-432, (1971) · Zbl 0231.02038
[3] Andrews, P.B., An introduction to mathematical logic and type theory: to truth through proof, (1986), Academic Press New York · Zbl 0617.03001
[4] Barendregt, H.P., The lambda-calculus, its syntax and semantics, Studies in logic and the foundation of mathematics, (1984), Elsevier Science North-Holland Amsterdam · Zbl 0551.03007
[5] Barendregt, H.P., Lambda calculi with types, () · Zbl 0549.03012
[6] Borovanský, P., Implementation of higher-order unification based on calculus of explicit substitutions, (), 363-368
[7] Briaud, D., Higher order unification as a typed narrowing, (), 131-138
[8] Chen, H.; Hsiang, J.; Kong, H.C., On finite representations of infinite sequences of terms, (), 100-114
[9] Church, A., A formulation of the simple theory of types, J. symbolic logic, 5, 56-68, (1940) · JFM 66.1192.06
[10] Curien, P.-L., Categorical combinators, sequential algorithms and functional programming, (1993), Birkhäuser Basel · Zbl 0814.68085
[11] Curien, P.-L.; Hardin, T.; Lévy, J.J., Confluence properties of weak and strong calculi of explicit substitutions, J. assoc. comput. Mach., 43, 362-397, (1996) · Zbl 0885.03014
[12] Curien, P.-L.; Rios, A., Un résultat de complétude pour LES substitutions explicites, C. R. acad. sci. Paris, 312, 471-476, (1991) · Zbl 0717.68053
[13] Dauchet, M., Simulation of Turing machines by a regular rule, Theoret. comput. sci., 103, 409-420, (1992) · Zbl 0753.68052
[14] de Bruijn, N., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church – rosser theorem, Indag. math., 34, 381-392, (1972) · Zbl 0253.68007
[15] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (), 244-320 · Zbl 0900.68283
[16] Dougherty, D.J., Higher-order unification via combinators, Theoret. comput. sci., 114, 273-298, (1993) · Zbl 0772.68061
[17] Dougherty, D.J.; Johann, P., A combinatory logic approach to higher-order E-unification, Theoret. comput. sci., 139, 207-242, (1995) · Zbl 0874.68271
[18] Dowek, G., A complete proof synthesis method for the cube of type systems, J. logic comput., 3, 287-315, (1993) · Zbl 0789.68123
[19] Dowek, G.; Hardin, T.; Kirchner, C., Higher-order unification via explicit substitutions, extended abstract, (), 366-374
[20] Dowek, G.; Hardin, T.; Kirchner, C.; Pfenning, F., Unification via explicit substitutions: the case of higher-order patterns, ()
[21] Goldfarb, D., The undecidability of the second order unification problem, Theoret. comput. sci., 13, 225-230, (1981) · Zbl 0457.03006
[22] Goubault-Larrecq, J., Technical report, (January 1997)
[23] Herbrand, J., Recherches sur la théorie de la démonstration, Travaux soc. sci. lett. varsovie, III, 33, (1930) · JFM 56.0824.02
[24] Hintermeier, C.; Kirchner, C.; Kirchner, H., Dynamically-typed computations for order-sorted equational presentations—extended abstract, (), 450-461
[25] Huet, G., The undecidability of unification in third order logic, Inform. and control, 22, 257-267, (1973) · Zbl 0257.02038
[26] Huet, G., A unification algorithm for typed lambda calculus, Theoret. comput. sci., 1, 27-57, (1975) · Zbl 0337.68027
[27] Hullot, J.-M., Canonical forms and unification, (), 318-334
[28] Hussmann, H., Unification in conditional equational theories, (), 543-553
[29] Jouannaud, J.-P.; Kirchner, C., Solving equations in abstract algebras: a rule-based survey of unification, (), 257-321
[30] Kirchner, C.; Kirchner, H.; Vittek, M., Designing constraint logic programming languages using computational systems, (), 131-158
[31] Kirchner, C.; Ringeissen, C., Higher-order equational unification via explicit substitutions, Algebraic and logic programming ALP-HOA, Lecture notes in computer science, 1298, (1997), Springer-Verlag Berlin, p. 61-75 · Zbl 0888.03007
[32] Kirchner, H.; Hermann, M., Meta-rule synthesis from crossed rewrite systems, (), 143-154
[33] Krivine, J.-L., Lambda calculus, types and models, (1993), Ellis Horwood Chichester · Zbl 0779.03005
[34] Martelli, A.; Montanari, U., An efficient unification algorithm, ACM trans. programming languages systems, 4, 258-282, (1982) · Zbl 0478.68093
[35] Middeldorp, A.; Hamoen, E., Completeness results for basic narrowing, Appl. algebra eng. commun. comput., 5, 213-253, (1994) · Zbl 0810.68088
[36] Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification, (), 253-281
[37] Miller, D., Unification under a mixed prefix, J. symbolic comput., 14, 321-358, (1992) · Zbl 0768.68067
[38] Muñoz, C., A left linear variant of λσ, Proceedings 6th international joint conference ALP’97-HOA’97, Southampton, UK, Lecture notes in computer science, 1298, (1997), Springer-Verlag Berlin
[39] Nadathur, G., Tech. report, (May 1996)
[40] Nadathur, G.; Wilson, D.S., A representation of lambda terms suitable for operations on their intensions, Proceedings of the 1990 ACM conference on lisp and functional programming, (1990), ACM Press New York, p. 341-348
[41] Nadathur, G.; Wilson, D.S., Tech. report, (January 1997)
[42] Pagano, B., X.R.S.: explicit reduction systems, a first-order calculus for higher-order calculi, (), 66-80
[43] Plotkin, G., Building-in equational theories, Mach. intelligence, 7, 73-90, (1972) · Zbl 0262.68036
[44] Rı́os, A., Contributions à l’étude des λ-calculs avec des substitutions explicites, (1993), U. Paris VII
[45] Siekmann, J.; Schmidt-Schauß, M., Unification algebras: an axiomatic approach to unification, equation solving and constraint solving, SEKI report, (1988)
[46] Snyder, W.; Gallier, J., Higher order unification revisited: complete sets of tranformations, J. symbolic comput., 8, 101-140, (1989) · Zbl 0682.03034
[47] Werner, A., Normalizing narrowing for weakly terminating and confluent systems, (), 415-430
[48] Williams, J.G., Instanciation theory. on the foundations of automated deduction, Lecture notes in artificial intelligence, 518, (1991), Springer-Verlag Berlin
[49] Dowek, G.; Hardin, T.; Kirchner, C., Rapport de recherche, (1998)
[50] Dowek, G.; Hardin, T.; Kirchner, C., HOL-lambda – sigma: an intensional first-order expression of higher-order logic, (), 317-331 · Zbl 0944.03007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.