Manfred Schmidt-Schauß ; Temur Kutsia ; Jordi Levy ; Mateu Villaret ; Yunus Kutz - Nominal Unification and Matching of Higher Order Expressions with Recursive Let

fi:7191 - Fundamenta Informaticae, May 6, 2022, Volume 185, Issue 3
Nominal Unification and Matching of Higher Order Expressions with Recursive LetArticle

Authors: Manfred Schmidt-Schauß ; Temur Kutsia ; Jordi Levy ; Mateu Villaret ; Yunus Kutz

    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.


    Volume: Volume 185, Issue 3
    Published on: May 6, 2022
    Accepted on: April 21, 2022
    Submitted on: February 17, 2021
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,I.2.3

    Consultation statistics

    This page has been seen 203 times.
    This article's PDF has been downloaded 197 times.