### Abstract

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.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Related publications

- 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

### Session Rensets

- Lambda_Terms
- Rensets
- Nominal_Sets
- Rensets_to_Nominal_Sets
- FRBCE_Rensets
- Substitutive_Sets
- Examples
- All

## Cite

×

Rensets-AFP

    @article{Rensets-AFP,
      author  = {Andrei Popescu},
      title   = {Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Rensets.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Mar 2, 2023 : Isabelle2022