Nominal unification of higher order expressions with recursive let

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.

Metadaten
Verfasserangaben:	Manfred Schmidt-Schauß ORCiD GND, Temur Kutsia, Jordi Levy, Mateu Villaret, Yunus Kutz
URN:	urn:nbn:de:hebis:30:3-620007
URL:	https://www2.ki.informatik.uni-frankfurt.de/papers/frank/frank-62.pdf
Titel des übergeordneten Werkes (Deutsch):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 62
Schriftenreihe (Bandnummer):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (62)
Verlag:	Research group for Artificial Intelligence and Software Technology Institut für Informatik, Fachbereich Informatik und Mathematik, Johann Wolfgang Goethe-Universität
Verlagsort:	Frankfurt am Main
Dokumentart:	Arbeitspapier
Sprache:	Englisch
Jahr der Fertigstellung:	2019
Datum der Erstveröffentlichung:	23.10.2019
Veröffentlichende Institution:	Universitätsbibliothek Johann Christian Senckenberg
Datum der Freischaltung:	23.11.2021
Ausgabe / Heft:	October 23, 2019
Seitenzahl:	24
Erste Seite:	1
Letzte Seite:	24
Institute:	Informatik und Mathematik / Informatik
DDC-Klassifikation:	0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Sammlungen:	Universitätspublikationen
Lizenz (Deutsch):	Deutsches Urheberrecht

Open Access