[TYPES] Bounds on #steps for leftmost reduction?

[Vincent Danos]

Le 4 juil. 04, à 23:26, Peter Moller Neergaard a écrit :

> 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?)
>

Glad that you ask :)
Yes it is. it is called a perpetual strategy in Barendregt's book
and we proved in:
1990, Une équivalence sur les lambda-termes, paru dans TCS  126 (1994).
that is actually maximizing the number of reduction steps.

> However, results concerning standard leftmost outermost reduction path
> will be useful starting point.
>
>

There is that paper by Roel de Vrijer:
Exactly estimating functionals and strong normalization. Proceedings of 
the
Koninklijke Nederlandse Akademie van Wetenschappen, Series A, 
90(4):479-493, December 1987.