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

[Pierre Hyvernat]

Hello.


Someone else is bound to have answered before my message gets through,
but here we go:


> I think this proof is invalid.  The inference
>
> > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).  Hence
> > (\x.xx)T_1 T_2 ... T_n is strongly normalizing.
>
> seems to use the inference
>
> If M reduces to N and N is SN, so is M.
>
>
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.)



Pierre
-- 
Real programmers don't comment their code.  It was hard
to write, it should be hard to understand.