  I introduce renaming-enriched sets (rensets for short), which are algebraic
structures axiomatizing fundamental properties of renaming (also known as
variable-for-variable substitution) on syntax with bindings. Rensets compare
favorably in some respects with the well-known foundation based on nominal
sets. In particular, renaming is a more fundamental operator than the nominal
swapping operator and enjoys a simpler, equationally expressed relationship
with the variable freshness predicate. Together with some natural axioms
matching properties of the syntactic constructors, rensets yield a truly
minimalistic characterization of lambda-calculus terms as an abstract datatype
-- one involving a recursively enumerable set of unconditional equations,
referring only to the most fundamental term operators: the constructors and
renaming. This characterization yields a recursion principle, which (similarly
to the case of nominal sets) can be improved by incorporating Barendregt's
variable convention. When interpreting syntax in semantic domains, my
renaming-based recursor is easier to deploy than the nominal recursor. My
results have been validated with the proof assistant Isabelle/HOL.
