King's College London

Research portal

Nominal Syntax with Atom Substitutions: Matching, Unification, Rewriting

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

Original languageEnglish
Title of host publicationFundamentals of Computation Theory - 22nd International Symposium, FCT 2019, Proceedings
EditorsLeszek Antoni Gąsieniec, Jesper Jansson, Christos Levcopoulos
PublisherSpringer Verlag
Number of pages16
ISBN (Print)9783030250263
Accepted/In press22 Jun 2019
E-pub ahead of print10 Jul 2019
Event22nd International Symposium on Fundamentals of Computation Theory, FCT 2019 - Copenhagen, Denmark
Duration: 12 Aug 201914 Aug 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11651 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference22nd International Symposium on Fundamentals of Computation Theory, FCT 2019


King's Authors


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.

Download statistics

No data available

View graph of relations

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