Accattoli, Beniamino; Kesner, Delia The permutative \(\lambda \)-calculus. (English) Zbl 1352.03019 Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 23-36 (2012). Summary: We introduce the permutative \(\lambda \)-calculus, an extension of \(\lambda \)-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 \(\lambda \)-terms.For the entire collection see [Zbl 1238.68012]. Cited in 4 Documents MSC: 03B40 Combinatory logic and lambda calculus PDF BibTeX XML Cite \textit{B. Accattoli} and \textit{D. Kesner}, Lect. Notes Comput. Sci. 7180, 23--36 (2012; Zbl 1352.03019) Full Text: DOI