Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version)

TL;DR

This work develops a nominal-algebraic approach to equational reasoning with binders modulo commutativity by using permutation fixed-point constraints in α-equivalence judgments, enabling reasoning without freshness constraints. It proves soundness and completeness with respect to nominal-set semantics and introduces a terminating, correct unification algorithm that yields a finitary set of solutions under commutativity. The framework supports structural induction over syntax with binders and commutative operators and has potential applications in formal verification, theorem proving, and programming language semantics, with an extended version providing full proofs in the appendix.

Abstract

Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and $α$-renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in $α$-equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the $π$-calculus.