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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.15.2 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |