Standard
Nominal Syntax with Atom Substitutions : Matching, Unification, Rewriting. / Domínguez, Jesús; Fernández, Maribel.
Fundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings. ed. / Leszek Antoni Gąsieniec; Jesper Jansson; Christos Levcopoulos. Springer Verlag, 2019. p. 64-79 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11651 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review
Harvard
Domínguez, J & Fernández, M 2019,
Nominal Syntax with Atom Substitutions: Matching, Unification, Rewriting. in LA Gąsieniec, J Jansson & C Levcopoulos (eds),
Fundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11651 LNCS, Springer Verlag, pp. 64-79, 22nd International Symposium on Fundamentals of Computation Theory, FCT 2019, Copenhagen, Denmark,
12/08/2019.
https://doi.org/10.1007/978-3-030-25027-0_5
APA
Domínguez, J., & Fernández, M. (2019).
Nominal Syntax with Atom Substitutions: Matching, Unification, Rewriting. In L. A. Gąsieniec, J. Jansson, & C. Levcopoulos (Eds.),
Fundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings (pp. 64-79). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11651 LNCS). Springer Verlag.
https://doi.org/10.1007/978-3-030-25027-0_5
Vancouver
Domínguez J, Fernández M.
Nominal Syntax with Atom Substitutions: Matching, Unification, Rewriting. In Gąsieniec LA, Jansson J, Levcopoulos C, editors, Fundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings. Springer Verlag. 2019. p. 64-79. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
https://doi.org/10.1007/978-3-030-25027-0_5
Author
Domínguez, Jesús ; Fernández, Maribel. / Nominal Syntax with Atom Substitutions : Matching, Unification, Rewriting. Fundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings. editor / Leszek Antoni Gąsieniec ; Jesper Jansson ; Christos Levcopoulos. Springer Verlag, 2019. pp. 64-79 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inbook{8cabb964b7f14aee92302d82cf83192a,
title = "Nominal Syntax with Atom Substitutions: Matching, Unification, Rewriting",
abstract = "Unification and matching algorithms are essential components of logic and functional programming languages and theorem provers. Nominal extensions have been developed to deal with syntax involving binding operators: nominal unification takes into account α-equivalence; however, it does not take into account non-capturing substitutions, which are not primitive in nominal syntax. We consider an extension of nominal syntax with non-capturing substitutions and show that matching is decidable and finitary but unification is undecidable. We provide a matching algorithm and characterise problems for which matching is unitary, giving rise to expressive and efficient rewriting systems.",
keywords = "Nominal syntax, Non-capturing substitution, Rewriting, Unification",
author = "Jes{\'u}s Dom{\'i}nguez and Maribel Fern{\'a}ndez",
year = "2019",
month = jul,
day = "10",
doi = "10.1007/978-3-030-25027-0_5",
language = "English",
isbn = "9783030250263",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "64--79",
editor = "G{\c a}sieniec, {Leszek Antoni} and Jesper Jansson and Christos Levcopoulos",
booktitle = "Fundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings",
address = "Germany",
note = "22nd International Symposium on Fundamentals of Computation Theory, FCT 2019 ; Conference date: 12-08-2019 Through 14-08-2019",
}
RIS (suitable for import to EndNote) Download
TY - CHAP
T1 - Nominal Syntax with Atom Substitutions
T2 - 22nd International Symposium on Fundamentals of Computation Theory, FCT 2019
AU - Domínguez, Jesús
AU - Fernández, Maribel
PY - 2019/7/10
Y1 - 2019/7/10
N2 - Unification and matching algorithms are essential components of logic and functional programming languages and theorem provers. Nominal extensions have been developed to deal with syntax involving binding operators: nominal unification takes into account α-equivalence; however, it does not take into account non-capturing substitutions, which are not primitive in nominal syntax. We consider an extension of nominal syntax with non-capturing substitutions and show that matching is decidable and finitary but unification is undecidable. We provide a matching algorithm and characterise problems for which matching is unitary, giving rise to expressive and efficient rewriting systems.
AB - Unification and matching algorithms are essential components of logic and functional programming languages and theorem provers. Nominal extensions have been developed to deal with syntax involving binding operators: nominal unification takes into account α-equivalence; however, it does not take into account non-capturing substitutions, which are not primitive in nominal syntax. We consider an extension of nominal syntax with non-capturing substitutions and show that matching is decidable and finitary but unification is undecidable. We provide a matching algorithm and characterise problems for which matching is unitary, giving rise to expressive and efficient rewriting systems.
KW - Nominal syntax
KW - Non-capturing substitution
KW - Rewriting
KW - Unification
UR - http://www.scopus.com/inward/record.url?scp=85070582688&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-25027-0_5
DO - 10.1007/978-3-030-25027-0_5
M3 - Conference paper
AN - SCOPUS:85070582688
SN - 9783030250263
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 64
EP - 79
BT - Fundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings
A2 - Gąsieniec, Leszek Antoni
A2 - Jansson, Jesper
A2 - Levcopoulos, Christos
PB - Springer Verlag
Y2 - 12 August 2019 through 14 August 2019
ER -