Email Gateway (Mar 02 2023 at 14:09): Email Gateway (Mar 02 2023 at 14:09):From: Lawrence Paulson <lp15@cam.ac.uk>
Happy to announce a new entry, by Andrei Popescu: Renaming-Enriched Sets:
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.
It is now on-line at https://www.isa-afp.org/entries/Rensets.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC