Can I read Rensets and Renaming-Based Recursion for Syntax with Bindings on EtoBox?

Rensets and Renaming-Based Recursion for Syntax with Bindings by Popescu, Andrei is a scholarly article available to read on EtoBox.

What is Rensets and Renaming-Based Recursion for Syntax with Bindings about?

I introduce renaming-enriched sets (rensets for short), which are algebraic structures axiomatizing fundamental properties of renaming (also known as variable-for-variable substitution) on syntax with bindings. Rensets compare favorably in some respects with the well-known foundation based on nominal sets. In particular, renaming is a more fundamental operator than the nominal swapping operator and enjoys a simpler, equationally expressed relationship with the variable freshness predicate. Together with some natural axioms matching properties of the syntactic constructors, rensets yield a truly minimalistic characterization of lambda-calculus terms as an abstract datatype -- one involving a recursively enumerable set of unconditional equations, referring only to the most fundamental term operators: the constructors and renaming. This characterization yields a recursion principle, which (similarly to the case of nominal sets) can be improved by incorporating Barendregt's variable convention. When interpreting syntax in semantic domains, my renaming-based recursor is easier to deploy than the nominal recursor. My results have been validated with the proof assistant Isabelle/HOL.

Author

Popescu, Andrei

Published

2022

Language

EN