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.
- Popescu, A. (2022). Rensets and Renaming-Based Recursion for Syntax with Bindings. Lecture Notes in Computer Science, 618–639. https://doi.org/10.1007/978-3-031-10769-6_36