Skew confluence and the lambda calculus with letrec (Q1849854)

This paper studies the cyclic lambda calculus that is an extension of the lambda calculus with the letrec construct. Cyclic lambda terms are represented by systems of recursive equations of the type \(\langle M \mid x_1 = M_1,\dots,x_n = M_n\rangle\), which is another notation for the construct \(\text{letrec} x_1 = M_1,\dots,x_n = M_n\;\text{in} M\). When lambda abstraction and cycles are admitted, confluence is lost. To obtain confluence, current formulations of cycles either impose restrictions to reductions or adopt a framework based on interaction nets. The authors introduce an alternative way of guaranteeing the consistency of the calculus without restriction. Since the terms contain cycles, it is useful to abandon normal forms in favor of infinite normal forms. The authors introduce skew confluence to guarantee the unicity of infinite normal forms, by combining rewriting with a quasi-order \(\leq\). Skew confluence states that if a term \(M\) reduces to two other terms, \(M_1\) and \(M_2\), then the second term \(M_2\) can always be reduced to a term \(Q\) that is better than the first one (i.e., \(Q \geq M_1\)). The main result of the paper is that cyclic lambda calculus is skew confluent, so that it has unique infinite normal forms. For the terms of plain lambda calculus, the infinite normal forms of cyclic lambda calculus correspond to Lévy-Longo trees. A cyclic explicit substitution calculus is introduced in the final part of the paper, where it is shown that the explicit calculus produces the same infinite normal forms as the cyclic lambda calculus. Finally, cyclic lambda calculus is shown sound and finitely complete with respect to the infinitary lambda calculus.