[TYPES] Bounds on #steps for leftmost reduction?

[Eduardo Bonelli]

Quoting Vincent Danos <Vincent.Danos at pps.jussieu.fr>:

> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 
> 
> 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.
> 

Another proof of this fact (together with other related goodies) is
given in:

Perpetual Reductions in Lambda Calculus .
Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen and Hongwei Xi .
Information and Computation, Vol. 149(2), March 1999.

Perhaps I can take this opportunity to ask whether anyone has seen
maximal strategies for lambda calculi with explicit substitutions.
Note that reducing a K-redex only when the argument is in normal
form seems not to be required since BETA creates a closure. However,
when to allow propagation of a substitution past an application seems
not to be obvious. 

Any pointers are welcome!

Regards,
E.




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.