Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Article type: Research Article

Authors: Schmidt-Schauß, Manfred^{a; *} | Kutsia, Temur^b | Levy, Jordi^c | Villaret, Mateu^d | Kutz, Yunus^e

Affiliations: [a] GU Frankfurt, Germany. [email protected] | [b] RISC, JKU Linz, Austria. [email protected] | [c] IIIA - CSIC, Spain. [email protected] | [d] IMA, Universitat de Girona, Spain. [email protected] | [e] GU Frankfurt, Germany. [email protected]

Correspondence: [*] Address for correspondence: Goethe-Universität Frankfurt am Main Fachbereich 12: Informatik und Mathematik, Robert-Mayer-Straße 11-15, 60325 Frankfurt am Main, Grrmany.

Abstract: A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP.

Keywords: Nominal unification, lambda calculus, higher-order expressions, recursive let, atom variables

DOI: 10.3233/FI-222110

Journal: Fundamenta Informaticae, vol. 185, no. 3, pp. 247-283, 2022