Filtern
Erscheinungsjahr
- 2019 (1)
Dokumenttyp
- Arbeitspapier (1)
Sprache
- Englisch (1)
Volltext vorhanden
- ja (1)
Gehört zur Bibliographie
- nein (1)
Institut
- Informatik (1)
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 expressions, for DAGs, and for garbage-free expressions and determine their complexity. As extension a nominal unification algorithm for higher-order expressions with recursive let and atom-variables is constructed, where we show that it also runs in non-deterministic polynomial time.