Skew confluence and the lambda calculus with letrec

✍ Scribed by Zena M. Ariola; Stefan Blom

• Publisher: Elsevier Science
• Year: 2002
• Tongue: English
• Weight: 574 KB
• Volume: 117
• Category: Article
• ISSN: 0168-0072
• DOI: 10.1016/s0168-0072(01)00104-x

✦ Synopsis

We present an extension of the lambda calculus with the letrec construct. In contrast to current theories, which impose restrictions on where the rewriting can take place, our theory is very liberal, e.g., it allows rewriting under lambda abstractions and on cycles. As shown previously, the reduction theory is non-con uent. Thus, we searched for and found a new property that resembles con uence and that is equivalent to uniqueness of inÿnite normal forms: skew con uence. This notion is based on the intuition that some terms are better than others and that terms reduce to better terms. It states that if a term reduces to two other terms, the second of those terms can always be reduced to a term that is better than the ÿrst.

Using skew con uence we deÿne the inÿnite normal form of a term and show that the inÿnite normal form deÿnes a congruence on the set of terms. We relate the lambda calculus plus letrec to the plain lambda calculus and to one of the inÿnitary lambda calculi. We also present a variant of our calculus, which follows the tradition of the explicit substitution calculi.