Superdevelopments fo rweak reduction

Eduardo Bonelli, Pablo Barenbaum

Research output: Contribution to journalConference articlepeer-review

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 languageEnglish
Pages (from-to)20-31
Number of pages12
JournalElectronic Notes in Theoretical Computer Science
DOIs
StatePublished - 2009
Event9th 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 200928 Jun 2009

Fingerprint

Dive into the research topics of 'Superdevelopments fo rweak reduction'. Together they form a unique fingerprint.

Cite this