Tags:Isabelle/HOL, nominal logic, substitution and syntax with bindings

Abstract:

I introduce substitutive sets, which are algebraic structures axiomatizing fundamental properties of variable-for-variable substitution on syntax with bindings. Substitutive sets compare favorably in some respects with the well-known foundation based on nominal sets. In particular, substitution 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, substitutive sets yield a truly minimalistic characterization of lambda-calculus terms as an abstract datatype, hence a recursion principle -- the first one in the literature that involves only unconditional equations on the constructors and substitution. Similarly to the case of nominal sets, an improvement of this recursion principle is possible, incorporating Barendregt’s variable convention. When interpreting syntax in semantic domains, my substitution-based recursor is easier to deploy than the nominal recursor. My results have been validated with the proof assistant Isabelle/HOL.

Rensets and Renaming-Based Recursion for Syntax with Bindings