Rensets and Renaming-Based Recursion for Syntax with Bindings

TL;DR

This paper introduces renaming-enriched sets (rensets), an algebraic framework for syntax with bindings, providing a minimalistic, recursive characterization of lambda calculus terms that simplifies semantic interpretation and proof automation.

Contribution

The paper presents rensets, a novel algebraic structure that offers a simpler, more fundamental approach to variable renaming in syntax with bindings, improving upon nominal set foundations.

Findings

Rensets provide a minimalistic algebraic characterization of lambda calculus.

The renaming-based recursion principle is easier to implement than nominal recursors.

Validated with Isabelle/HOL proof assistant.

Abstract

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.