Meta-variables as infinite lists in nominal terms unification and rewriting
Murdoch J. Gabbay · Logic Journal of IGPL · 2012
We consider the theories of nominal unification and rewriting for a new and simplified presentation of nominal terms, based on modelling moderated nominal unknowns as infinite but decidable tuples of atoms. Nominal terms α-equivalence becomes a special case of ordinary α-equivalence, definitions and proofs come closer to those of traditional syntax, proofs are simplified, and some new properties are obtained.