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!
cited_by cdi_FETCH-LOGICAL-c274t-3884fdfead8dae71b50e176443eb64f00566bd109e43c29264344890d5351b423
cites cdi_FETCH-LOGICAL-c274t-3884fdfead8dae71b50e176443eb64f00566bd109e43c29264344890d5351b423
container_end_page 31
container_issue 2
container_start_page 1
container_title ACM transactions on computational logic
container_volume 13
creator Levy, Jordi
Villaret, Mateu
description 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.
doi_str_mv 10.1145/2159531.2159532
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_miscellaneous_1671582868</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>1671582868</sourcerecordid><originalsourceid>FETCH-LOGICAL-c274t-3884fdfead8dae71b50e176443eb64f00566bd109e43c29264344890d5351b423</originalsourceid><addsrcrecordid>eNotkDtPwzAURi0EEqUws2ZkSevrd0ZUAUWqKAOV2CwnuQajvLBTJP49VMl0vuHoGw4ht0BXAEKuGchCclhNZGdkAVLqvBDy_fy0WZFzbeQluUrpi1JgmrMF4S99GzrXZIcu-FC5MfRd5mPfZi7bho9PjPk-1hizV4xpwGoMP3hNLrxrEt7MXJLD48PbZpvv9k_Pm_tdXjEtxpwbI3zt0dWmdqihlBRBKyE4lkp4SqVSZQ20QMErVjAluBCmoLXkEkrB-JLcTb9D7L-PmEbbhlRh07gO-2OyoDRIw4wy_-p6UqvYpxTR2yGG1sVfC9Se8tg5z0zG_wD6h1WO</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>1671582868</pqid></control><display><type>article</type><title>Nominal Unification from a Higher-Order Perspective</title><source>Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)</source><creator>Levy, Jordi ; Villaret, Mateu</creator><creatorcontrib>Levy, Jordi ; Villaret, Mateu</creatorcontrib><description>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.</description><identifier>ISSN: 1529-3785</identifier><identifier>EISSN: 1557-945X</identifier><identifier>DOI: 10.1145/2159531.2159532</identifier><language>eng</language><subject>Computation ; Fragmentation ; Logic ; Mathematical analysis ; Mathematical models ; Names ; Preserves ; Translations</subject><ispartof>ACM transactions on computational logic, 2012-04, Vol.13 (2), p.1-31</ispartof><lds50>peer_reviewed</lds50><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c274t-3884fdfead8dae71b50e176443eb64f00566bd109e43c29264344890d5351b423</citedby><cites>FETCH-LOGICAL-c274t-3884fdfead8dae71b50e176443eb64f00566bd109e43c29264344890d5351b423</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Levy, Jordi</creatorcontrib><creatorcontrib>Villaret, Mateu</creatorcontrib><title>Nominal Unification from a Higher-Order Perspective</title><title>ACM transactions on computational logic</title><description>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.</description><subject>Computation</subject><subject>Fragmentation</subject><subject>Logic</subject><subject>Mathematical analysis</subject><subject>Mathematical models</subject><subject>Names</subject><subject>Preserves</subject><subject>Translations</subject><issn>1529-3785</issn><issn>1557-945X</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2012</creationdate><recordtype>article</recordtype><recordid>eNotkDtPwzAURi0EEqUws2ZkSevrd0ZUAUWqKAOV2CwnuQajvLBTJP49VMl0vuHoGw4ht0BXAEKuGchCclhNZGdkAVLqvBDy_fy0WZFzbeQluUrpi1JgmrMF4S99GzrXZIcu-FC5MfRd5mPfZi7bho9PjPk-1hizV4xpwGoMP3hNLrxrEt7MXJLD48PbZpvv9k_Pm_tdXjEtxpwbI3zt0dWmdqihlBRBKyE4lkp4SqVSZQ20QMErVjAluBCmoLXkEkrB-JLcTb9D7L-PmEbbhlRh07gO-2OyoDRIw4wy_-p6UqvYpxTR2yGG1sVfC9Se8tg5z0zG_wD6h1WO</recordid><startdate>201204</startdate><enddate>201204</enddate><creator>Levy, Jordi</creator><creator>Villaret, Mateu</creator><scope>AAYXX</scope><scope>CITATION</scope><scope>7SC</scope><scope>8FD</scope><scope>JQ2</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope></search><sort><creationdate>201204</creationdate><title>Nominal Unification from a Higher-Order Perspective</title><author>Levy, Jordi ; Villaret, Mateu</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c274t-3884fdfead8dae71b50e176443eb64f00566bd109e43c29264344890d5351b423</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2012</creationdate><topic>Computation</topic><topic>Fragmentation</topic><topic>Logic</topic><topic>Mathematical analysis</topic><topic>Mathematical models</topic><topic>Names</topic><topic>Preserves</topic><topic>Translations</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Levy, Jordi</creatorcontrib><creatorcontrib>Villaret, Mateu</creatorcontrib><collection>CrossRef</collection><collection>Computer and Information Systems Abstracts</collection><collection>Technology Research Database</collection><collection>ProQuest Computer Science Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><jtitle>ACM transactions on computational logic</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Levy, Jordi</au><au>Villaret, Mateu</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Nominal Unification from a Higher-Order Perspective</atitle><jtitle>ACM transactions on computational logic</jtitle><date>2012-04</date><risdate>2012</risdate><volume>13</volume><issue>2</issue><spage>1</spage><epage>31</epage><pages>1-31</pages><issn>1529-3785</issn><eissn>1557-945X</eissn><abstract>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.</abstract><doi>10.1145/2159531.2159532</doi><tpages>31</tpages></addata></record>
fulltext fulltext
identifier ISSN: 1529-3785
ispartof ACM transactions on computational logic, 2012-04, Vol.13 (2), p.1-31
issn 1529-3785
1557-945X
language eng
recordid cdi_proquest_miscellaneous_1671582868
source Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)
subjects Computation
Fragmentation
Logic
Mathematical analysis
Mathematical models
Names
Preserves
Translations
title Nominal Unification from a Higher-Order Perspective
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-29T06%3A19%3A45IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Nominal%20Unification%20from%20a%20Higher-Order%20Perspective&rft.jtitle=ACM%20transactions%20on%20computational%20logic&rft.au=Levy,%20Jordi&rft.date=2012-04&rft.volume=13&rft.issue=2&rft.spage=1&rft.epage=31&rft.pages=1-31&rft.issn=1529-3785&rft.eissn=1557-945X&rft_id=info:doi/10.1145/2159531.2159532&rft_dat=%3Cproquest_cross%3E1671582868%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c274t-3884fdfead8dae71b50e176443eb64f00566bd109e43c29264344890d5351b423%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=1671582868&rft_id=info:pmid/&rfr_iscdi=true