Nominal Unification of Higher Order Expressions with Recursive Let
Programming Languages
2023-03-14 v1 Logic in Computer Science
Abstract
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine the complexity of corresponding unification problems.
Cite
@article{arxiv.1608.03771,
title = {Nominal Unification of Higher Order Expressions with Recursive Let},
author = {Manfred Schmidt-Schauß and Temur Kutsia and Jordi Levy and Mateu Villaret},
journal= {arXiv preprint arXiv:1608.03771},
year = {2023}
}
Comments
Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)