Skew confluence and the lambda calculus with letrec

DOI10.1016/S0168-0072(01)00104-XMaRDI QIDQ1849854zbMATH OpenFDO

Authors Zena M. Ariola, Stefan Blom

Publication date 2 December 2002

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0168-0072(01)00104-X

zbMATH Keywords

cycles infinite normal forms lambda calculus skew confluence

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Review text

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.

Recommendations

Cites work

Cited in

(19)

This page was built for publication: Skew confluence and the lambda calculus with letrec

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1849854)