English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/134595
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:


Nominal unification from a higher-order perspective

AuthorsLevy, Jordi ; Villaret, Mateu
KeywordsNominal unification
Higher-order pattern unification
Issue Date2012
PublisherAssociation for Computing Machinery
CitationACM Transactions on Computational Logic 13 (2), art. 10 (2012)
AbstractNominal logic is an extension of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to lambda-terms, in nominal terms, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of the lambda-calculus. Despite these differences, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be quadratically reduced to a particular fragment of higher-order unification problems: higher-order pattern unification. We also prove that the translation preserves most generality of unifiers. © 2012 ACM 1529-3785/2012/04-ART10 $10.00.
Identifiersdoi: 10.1145/2159531.2159532
issn: 1529-3785
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
Show full item record
Review this work

Related articles:

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.