[TYPES] questiuon about strong normalization in untyped lambda-calculus

[eduardo@sol.lifia.info.unlp.edu.ar]

>>
> As you pointed out, this is false; but the proof doesn't use this.
> It relies on the following general observation:
>
>   if M[x:=N] N1 ... Nk is SN   and   if N is SN
>   then (\x.M) N N1 ... Nk is also SN
>
> (This is true.)

You, of course, require x to occur free in M.

This is an example of a perpetual reduction step (contrapositive  
reading of the above):
1) M has an infinite reduction sequence
2) M -> N
implies
N has an infinite reduction sequence.

Perpetual strategies for arbitrary orthogonal higher-order rewrite  
systems (thus including beta) have been studied in:

Zurab Khasidashvili, Mizuhito Ogawa, and Vincent van Oostrom
Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems
Information and Computation, Volume 164, pp. 118 - 151, 2001

How to use perpetual strategies for inductively characterizing the set  
of SN terms has been given here:

Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen, Hongwei Xi:  
Perpetual Reductions in Lambda-Calculus. Inf. Comput. 149(2): 173-225  
(1999)

     Regards,
     E.

Disclaimer: These references are stated merely as starting points. You  
should consult the references they cite for further pointers.


----------------------------------------------------------------
Este mensaje ha sido enviado utilizando IMP desde LIFIA.