Superdevelopments for Weak Reduction

Eduardo Bonelli
(CONICET and Universidad Nacional de Quilmes, Argentina)
Pablo Barenbaum
(Universidad de Buenos Aires, Argentina)

We study superdevelopments in the weak lambda calculus of Cagman 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.

In Maribel Fernández: Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2009), Brasilia, Brazil, 28th June 2009, Electronic Proceedings in Theoretical Computer Science 15, pp. 20–31.
Published: 26th January 2010.

ArXived at: https://dx.doi.org/10.4204/EPTCS.15.2 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org