[TYPES] Bounds on #steps for leftmost reduction?

[Marina Lenisa]

A semantical analysis of Barendregt F_\infty perpetual strategy and of
perpetual strategies in general is carried out in

F. Honsell, M. Lenisa,=20
"Semantical Analysis of Perpetual Strategies in lambda-calculus",
Theoretical Computer Science, vol.
212, 1999, pp. 183-209.=20



On Mon, 5 Jul 2004, Vincent Danos wrote:

> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list=
]
>=20
>=20
> Le 4 juil. 04, =E0 23:26, Peter Moller Neergaard a =E9crit :
>=20
> > I am actually considering a slightly modified reduction strategy which
> > completely reduces the argument of a K-redex before taking the
> > reduction.  In other words, a beta redex where the binding variable is
> > not free in the body of the abstraction is not reduced until the
> > discarded argument is in normal form.  (Is this the maximal strategy?)
> >
>=20
> Glad that you ask :)
> Yes it is. it is called a perpetual strategy in Barendregt's book
> and we proved in:
> 1990, Une =E9quivalence sur les lambda-termes, paru dans TCS  126 (1994).
> that is actually maximizing the number of reduction steps.
>=20
> > However, results concerning standard leftmost outermost reduction path
> > will be useful starting point.
> >
> >
>=20
> There is that paper by Roel de Vrijer:
> Exactly estimating functionals and strong normalization. Proceedings of=
=20
> the
> Koninklijke Nederlandse Akademie van Wetenschappen, Series A,=20
> 90(4):479-493, December 1987.=20
>=20
>=20
>=20