Abstract
We study superdevelopments in the weak lambda calculus of Çaǧman and Hindley, a confluent variant of the standard weak lambda calculus in which reduction below lambdas is forbidden. In contrast to developments, a superdevelopment from a term M allows not only residuals of redexes in M to be reduced but also some newly created ones. In the lambda calculus there are three ways new redexes may be created; in the weak lambda calculus a new form of redex creation is possible. We present labeled and simultaneous reduction formulations of superdevelopments for the weak lambda calculus and prove them equivalent.
Original language | English |
---|---|
Pages (from-to) | 20-31 |
Number of pages | 12 |
Journal | Electronic Notes in Theoretical Computer Science |
DOIs | |
State | Published - 2009 |
Event | 9th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2009, associated to 20th International Conference on Rewriting Techniques and Applications, RTA 2009, and was a part of the Federated Conference on RDP 2009 - Brasilia, Brazil Duration: 28 Jun 2009 → 28 Jun 2009 |