Unification via the \(\lambda s_e\)-style of explicit substitutions (Q2743636)

In this paper the authors adapt the higher-order unification method of \textit{G. Dowek, T. Hardin} and \textit{C. Kirchner} [Inf. Comput. 157, 183-235 (2000)] to a \(\lambda s\)-style calculus of explicit substitutions [\textit{F.Kamareddine} and \textit{A. Ríos}, Lect. Notes Comput. Sci. 982, 45-62 (1995)]. The method of Dowek et al. [loc. cit.] is based on a different substitution calculus, in \(\lambda \sigma\)-style [\textit{M. Abadi, L. Cardelli, P.-L. Curien} and \textit{J.-J. Lévy}, J. Funct. Program. 1, 375-416 (1991; Zbl 0941.68542)]. Explicit substitutions enable to reduce the problem of higher-order unification to first-order unification. As mentioned by the authors the advantage of using \(\lambda s\) instead of \(\lambda \sigma\) are mainly consequences of the differences between both calculi: 1. Only one sort of objects is needed: terms. There is no need of substitution objects like in \(\lambda \sigma\). 2. Detection of redexes depends on the search for solutions of simple arithmetic constraints. Moreover, the presentation using \(\lambda s\) is for me clearer than the one using \(\lambda \sigma\).