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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Manfred Schmidt-SchaußORCiDGND, 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
Parent Title (German):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 62
Series (Serial Number):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (62)
Publisher:Research group for Artificial Intelligence and Software Technology Institut für Informatik, Fachbereich Informatik und Mathematik, Johann Wolfgang Goethe-Universität
Place of publication:Frankfurt am Main
Document Type:Working Paper
Language:English
Year of Completion:2019
Date of first Publication:2019/10/23
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2021/11/23
Issue:October 23, 2019
Page Number:24
First Page:1
Last Page:24
Institutes:Informatik und Mathematik / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License LogoDeutsches Urheberrecht