Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion

I formalize the notion of renaming-enriched sets (rensets for short) and renaming-based recursion introduced in my IJCAR 2022 paper “Rensets and Renaming-Based Recursion for Syntax with Bindings”. Rensets are an algebraic axiomatization of renaming (variable-for-variable substitution). The formalization includes a connection with nominal sets, showing that any renset naturally gives rise to a nominal set. It also includes examples of deploying the renaming-based recursor: semantic interpretation, counting functions for free and bound occurrences, unary and parallel substitution, etc. Finally, it includes a variation of rensets that axiomatize term-for-variable substitution, called substitutive sets, which yields a corresponding recursion principle.