Matching and alpha-equivalence check for nominal terms

摘要

Nominal terms generalise first-order terms by including abstraction and name swapping constructs, α-equivalence can be easily axiomatised using name swappings and a freshness relation, which makes the nominal approach well adapted to the specification of systems that involve binders. Nominal matching is matching modulo a-equivalence and has applications in programming languages, rewriting, and theorem proving. In this paper, we describe efficient algorithms to check the validity of equations involving binders and to solve matching problems modulo a-equivalence, using the nominal approach.