×

Higher-order unification: a structural relation between Huet’s method and the one based on explicit substitutions. (English) Zbl 1138.03014

Summary: We compare two different styles of Higher-Order Unification (HOU): the classical HOU algorithm of Huet for the simply typed \(\lambda \)-calculus and HOU based on the \(\lambda \sigma \)-calculus of explicit substitutions. For doing so, first, the original Huet algorithm for the simply typed \(\lambda \)-calculus with names is adapted to the language of the \(\lambda \)-calculus in de Bruijn’s notation, since this is the notation used by the \(\lambda \sigma \)-calculus. Afterwards, we introduce a new structural notation, called unification tree, which eases the presentation of the subgoals generated by Huet’s algorithm and its behaviour. The unification tree notation will be important for the comparison between Huet’s algorithm and unification in the \(\lambda \sigma \)-calculus whose derivations are presented into a structure called derivation tree. We prove that there exists an important structural correspondence between Huet’s HOU and the \(\lambda \sigma \)-HOU method: for each (sub-)problem in the unification tree there exists a counterpart in the derivation tree. This allows us to conclude that the \(\lambda \sigma \)-HOU is a generalization of Huet’s algorithm and that solutions computed by the latter are always computed by the former method.

MSC:

03B40 Combinatory logic and lambda calculus
03B25 Decidability of theories and sets of sentences
03B35 Mechanization of proofs and logical operations

Software:

SUBSEXPL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J., Explicit substitutions, Journal of Functional Programming, 1, 4, 375-416 (1991) · Zbl 0941.68542
[2] Ayala-Rincón, M.; Kamareddine, F., Unification via the \(\lambda s_e\)-style of explicit substitution, The Logical Journal of the Interest Group in Pure and Applied Logics, 9, 4, 489-523 (2001) · Zbl 0987.03012
[3] Ayala-Rincón, M.; Kamareddine, F., On applying the \(\lambda s_e\)-style of unification for simply-typed higher order unification in the pure lambda calculus, WoLLIC 2001 Selected Papers. WoLLIC 2001 Selected Papers, Matemática Contemporânea, 24, 1-22 (2003) · Zbl 1073.03007
[4] Ayala-Rincón, M.; de Moura, F. L.C.; Kamareddine, F., Comparing and implementing calculi of explicit substitutions with eta-reduction, WoLLIC 2002 Selected Papers. WoLLIC 2002 Selected Papers, Annals of Pure and Applied Logic, 134, 1, 5-41 (2005) · Zbl 1067.03042
[5] Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics (1984), North-Holland · Zbl 0551.03007
[6] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), CUP
[7] de Bruijn, N. G., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Mat., 34, 5, 381-392 (1972) · Zbl 0253.68007
[8] Dowek, G.; Hardin, T.; Kirchner, C., Higher-order unification via explicit substitutions, Information and Computation, 157, 183-235 (2000) · Zbl 1005.03016
[9] Dowek, G., Higher-order unification and matching, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. II (2001), MIT Press/Elsevier), 1009-1062, (Chapter 16) · Zbl 1011.03005
[10] Goldfarb, W., The undecidability of the second-order unification problem, TCS, 13, 2, 225-230 (1981) · Zbl 0457.03006
[11] Hindley, J. R., Basic Simple Type Theory, Cambridge Tracts in Theoretical Computer Science, vol. 42 (1997), CUP · Zbl 0906.03012
[12] Huet, G., A unification algorithm for typed \(λ\)-calculus, TCS, 1, 27-57 (1975) · Zbl 0332.02035
[13] Huet, G., Higher order unification 30 years later, (Carreño, V. A.; Muñoz, C. A.; Tahar, S., Theorem Proving in Higher Order Logics—TPHOLs 2002. Theorem Proving in Higher Order Logics—TPHOLs 2002, Lecture Notes in Computed Science, vol. 2410 (2002), Springer), 3-12 · Zbl 1013.68541
[14] Liang, C.; Nadathur, G.; Qi, X., Choices in representation and reduction strategies for lambda terms in intesional contexts, Journal of Automated Reasoning, 33, 2, 89-132 (2004) · Zbl 1102.68019
[15] de Moura, F. L.C.; Ayala-Rincón, M.; Kamareddine, F., SUBSEXPL: A tool for simulating and comparing explicit substitutions calculi, Journal of Applied Non-Classical Logics, 16, 1-2, 119-150 (2006), (special issue on Implementation of Logics) · Zbl 1184.68469
[16] T. Nipkow, Higher-order critical pairs, in: Proc. 6th IEEE Symp. Logic in Computer Science, 1991, pp. 342-349; T. Nipkow, Higher-order critical pairs, in: Proc. 6th IEEE Symp. Logic in Computer Science, 1991, pp. 342-349
[17] A. Ríos, Contributions à l’Étude de Λ;; A. Ríos, Contributions à l’Étude de Λ;
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.