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

*(English)*Zbl 1138.03014Summary: 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
PDF
BibTeX
XML
Cite

\textit{F. L. C. de Moura} et al., J. Appl. Log. 6, No. 1, 72--108 (2008; Zbl 1138.03014)

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, 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, 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, (), 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, (), 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 |

[17] | A. Ríos, Contributions à l’étude de λ-calculs avec des substitutions explicites, Thèse de doctorat, Université Paris VII, 1993 |

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.