Nominal syntax with atom substitutions

TY - JOUR

T1 - Nominal syntax with atom substitutions

AU - Domínguez, Jesús

AU - Fernández, Maribel

N1 - Funding Information: We thank James Cheney, Elliot Fairweather and Jordi Levy for helpful comments and useful pointers, and the anonymous reviewers of FCT 2019 for comments on a previous version of this paper. Publisher Copyright: © 2021 Elsevier Inc.

PY - 2021/8

Y1 - 2021/8

N2 - Nominal syntax is a generalisation of first-order syntax that includes names, a notion of name binding and an elegant axiomatisation of alpha-equivalence, based on nominal set theory. However, it does not take into account non-capturing atom substitution, which is not a primitive notion in nominal syntax. We consider an extension of nominal syntax with non-capturing atom substitutions and show that matching is decidable and finitary but unification is undecidable in general. The proof of undecidability of unification is obtained by reducing Hilbert's tenth problem to unification of extended nominal terms. We provide a general matching algorithm and characterise a class of problems for which matching is unitary, giving rise to expressive and efficient rewriting systems.

AB - Nominal syntax is a generalisation of first-order syntax that includes names, a notion of name binding and an elegant axiomatisation of alpha-equivalence, based on nominal set theory. However, it does not take into account non-capturing atom substitution, which is not a primitive notion in nominal syntax. We consider an extension of nominal syntax with non-capturing atom substitutions and show that matching is decidable and finitary but unification is undecidable in general. The proof of undecidability of unification is obtained by reducing Hilbert's tenth problem to unification of extended nominal terms. We provide a general matching algorithm and characterise a class of problems for which matching is unitary, giving rise to expressive and efficient rewriting systems.

KW - Matching

KW - Nominal syntax

KW - Non-capturing substitution

KW - Rewriting

KW - Unification

UR - http://www.scopus.com/inward/record.url?scp=85100806903&partnerID=8YFLogxK

U2 - 10.1016/j.jcss.2021.01.002

DO - 10.1016/j.jcss.2021.01.002

M3 - Article

AN - SCOPUS:85100806903

SN - 0022-0000

VL - 119

SP - 34

EP - 59

JO - JOURNAL OF COMPUTER AND SYSTEM SCIENCES

JF - JOURNAL OF COMPUTER AND SYSTEM SCIENCES

ER -