[TYPES] Bounds on #steps for leftmost reduction?

[Peter Moller Neergaard]

Consider the simply typed lambda calculus (or another typed lambda
calculus). Does anybody know results concerning the upper bounds on
the length of the leftmost outermost beta reduction path?  For
instance, a result relating the length to the rank of the type.

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?)
However, results concerning standard leftmost outermost reduction path
will be useful starting point.

Thanks in advance for any pointers.
Best regards

Peter M{\o}ller Neergaard
-- 
http://www.linearity.org/turtle/contact.html 
``If we're an arrogant nation, they'll resent us.
If we're a humble nation but strong, they'll welcome us.''--George W. Bush