The permutative \(\lambda \)-calculus. (English) Zbl 1352.03019

Accattoli, Beniamino; Kesner, Delia

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].

MSC:

03B40

Combinatory logic and lambda calculus