The Permutative λ-Calculus

Abstract We introduce the permutative λ -calculus, an extension of λ -calculus with three equations and one reduction rule for permuting constructors, generalising many calculi in the literature, in particular Regnier’s sigma-equivalence and Moggi’s assoc-equivalence. We prove confluence modulo the equations and preservation of beta-strong normalisation (PSN) by means of an auxiliary substitution calculus. The proof of confluence relies on M-developments, a new notion of development for λ -terms.

Authors

• Beniamino Accattoli
• Delia Kesner

Keywords

No keywords are indexed for this paper.