Upper Bounds for Standardizations and an Application
Xi, Hongwei
J. Symbolic Logic, Tome 64 (1999) no. 1, p. 291-303 / Harvested from Project Euclid
We present a new proof for the standardization theorem in $\lambda$-calculus, which is largely built upon a structural induction on $\lambda$-terms. We then extract some bounds for the number of $\beta$-reduction steps in the standard $\beta$-reduction sequence obtained from transforming a given $\beta$-reduction sequence, sharpening the standardization theorem. As an application, we establish a super exponential bound for the lengths of $\beta$-reduction sequences from any given simply typed $\lambda$-terms.
Publié le : 1999-03-14
Classification: 
@article{1183745706,
     author = {Xi, Hongwei},
     title = {Upper Bounds for Standardizations and an Application},
     journal = {J. Symbolic Logic},
     volume = {64},
     number = {1},
     year = {1999},
     pages = { 291-303},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745706}
}
Xi, Hongwei. Upper Bounds for Standardizations and an Application. J. Symbolic Logic, Tome 64 (1999) no. 1, pp.  291-303. http://gdmltest.u-ga.fr/item/1183745706/