Superdevelopments for Weak Reduction
Logic in Computer Science
2010-01-26 v1
Abstract
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.
Cite
@article{arxiv.1001.4429,
title = {Superdevelopments for Weak Reduction},
author = {Eduardo Bonelli and Pablo Barenbaum},
journal= {arXiv preprint arXiv:1001.4429},
year = {2010}
}