es81 (By N. Fazio)

Scriviamo preliminarmente la definizione ricorsiva del prodotto in \-calcolo: 

mult == \xy.if (iszero x) 0 (add y (mult (pre x) y)).

dove add è un \-termine che rappresenta la somma curryficata. 

Lambda-astraendo dalla definizione ricorsiva, otteniamo il funzionale:
 
F == \fxy.if (iszero x) 0 (add y (f (pre x) y)).

Per ottenere la rappresentazione eslicita di mult, basta applicare l'operatore di punto fisso:
 
Y == \f.((\x.f(xx))(\x.f(xx)))

ottenendo: 

Y F == (\f.((\x.f(xx))(\x.f(xx)))) (\fxy.if (iszero x) 0 (add y (f (pre x) y))).

Sfruttando la beta-equivalenza che caratterizza gli operatori di punto fisso: 

Y F =b F(Y F)

otteniamo: 

Y F =b F(Y F) == ( \fxy.if (iszero x) 0 (add y (f (pre x) y)))(Y F) -> 
-> (\xy.if (iszero x) 0 (add y ((Y F) (pre x) y))).

Questa è in una forma migliore, perché possiamo subito "applicare i due argomenti".