es87

Il termine \xy.((\yx.x(yy))z(\z.zz)) non e' in head-normal form, 
pero' possiede una head-normal form: \xy.zz(zz). 
Un lambda termine puo' avere piu' di una head-normal form. 
Per esempio per il termine \x.(Ix)(Ia)(Ib) \x.x(Ia)(Ib) e' una head-normal, come anche \x.x(Ia)b. 
Ovviamente le prime astrazioni e la variabile di testa sono le stesse per tutte le head-normal forms 
di un termine che possiede head-normal form e questo si dimostra utilizzando il teorema di Church-Rosser 
e osservando che in un termine in head-normal form le possibili riduzioni che possiamo 
fare su di esso non altereranno mai ne' le prime astrazioni, ne' la variabile di testa.