# Nominal Unification and Matching of Higher Order Expressions with Recursive Let

arXiv: https://arxiv.org/abs/2102.08146 · HTML: https://mlsanity.com/paper/2102.08146/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 50 references that are in the map.
- First posted on arXiv 16 Feb 2021.

## Builds on (most cited first, 2 of 2)

- [Nominal Unification of Higher Order Expressions with Recursive Let](https://mlsanity.com/paper/1608.03771/) (2016)
- [Nominal C-Unification](https://mlsanity.com/paper/1709.05384/) (2017)

## Abstract (arXiv)

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.