Nominal Unification from a Higher-Order Perspective

Nominal 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 capturabl...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on computational logic 2012-04, Vol.13 (2), p.1-31
Main Authors: Levy, Jordi, Villaret, Mateu
Format: Article
Language:English
Subjects:
Computation
Fragmentation
Logic
Mathematical analysis
Mathematical models
Names
Preserves
Translations
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Nominal 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.
ISSN:1529-3785
1557-945X
DOI:10.1145/2159531.2159532