Exact Bounds for Lengths of Reductions in Typed $\lambda$-Calculus

Beckmann, Arnold

J. Symbolic Logic, Tome 66 (2001) no. 1, p. 1277-1285 / Harvested from Project Euclid

Résumé

We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed $\lambda$-calculus with $\beta-, \xi$- and $\eta$-conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.

Publié le : 2001-09-14
Classification:

@article{1183746559,
     author = {Beckmann, Arnold},
     title = {Exact Bounds for Lengths of Reductions in Typed $\lambda$-Calculus},
     journal = {J. Symbolic Logic},
     volume = {66},
     number = {1},
     year = {2001},
     pages = { 1277-1285},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183746559}
}

Beckmann, Arnold. Exact Bounds for Lengths of Reductions in Typed $\lambda$-Calculus. J. Symbolic Logic, Tome 66 (2001) no. 1, pp.  1277-1285. http://gdmltest.u-ga.fr/item/1183746559/