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

Andrei Popescu 📧

February 28, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Related publications

Session Rensets