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.