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.
翻译:描述高顺序表达式的名义统一, 并显示在非决定性的多元时间运行。 我们还探索了表达式、 DAGs 和无垃圾表达式的名义乳胶配比等专业, 并确定其复杂性。 我们还为循环性表达式和原子可变性表示式的较高顺序表达式提供了一种名义统一算法, 我们在这里显示它也在非决定性的多元时间运行。 此外, 我们还证明, 有一种假设策略, 一种与无脑和原子可变的名义统一战略, 这是指数增长和非非决定性主义之间的权衡。 NP 中也显示, 与部分白细胞环境的变量的名词匹配 。