King's College London

Research portal

Nominal Syntax with Atom Substitutions: Matching, Unification, Rewriting

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

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 proceedingConference paperpeer-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)).

Bibtex Download

@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 -

View graph of relations

© 2020 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454