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

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.