es67

Entrambe calcolano la stessa funzione: il successore. 
Infatti, consideriamo il numerale di Church per il numero m : \gy.g(..-mvolte-..(g(y))...) 
Abbiamo che (\nfx.f(nfx))(\gy.g(..-mvolte-..(g(y))...)) -->> \fx.f(f(..-mvolte-..(f(x))...)) 
e vediamo che \fx.f(f(..-mvolte-..(f(x))...)) non e' altro che \fx.f(..-m+1volte-..(f(x))...)), 
cioe' il numerale di Church per il numero m+1. 
Per l'altro termine (\nfx.nf(fx))(\gy.g(..-mvolte-..(g(y))...)) -->> \fx.f(..-mvolte-..(f(f(x)))...) 
e vediamo che \fx.f(..-mvolte-..(f(f(x)))...) non e' altro che \fx.f(..-m+1volte-..(f(x))...)), 
cioe' il numerale di Church per il numero m+1. 
I due termini sono in forma normale e, non essendo identici (modulo alfa conversione) 
non possono essere beta convertibili per il teorema di Church-Rosser. 
Per far si che due termini che rappresentano la stessa funzione siano convertibili 
occorrerebbe aggiungere l'assioma di eta-conversione alla teoria della beta-conversione 
(occorrerebbe cioe' essere nella teoria delle beta-eta-conversione). 

Non e' comunque da ritenersi sconveniente la cosa perche' a noi puo' bastare benissimo 
una teoria che uguaglia i risultati dell'applicazione di argomenti a termini che rapresentano 
la stessa funzione matematica. 
La teoria della beta-conversione vuole essere una teoria di funzioni come algoritmi e 
non di funzioni in termini strettamente matematici. 

I nostri due termini quindi in tale teoria devono essere diversi poiche', 
pur calcolando la stessa funzione sono, come algoritmi, differenti 
(i due termini vengono solitamente chiamati successore destro e successore sinistro).