Eta abstraction dans le lambda calcul

Question

Eta Abstraction dans le calcul de lambda signifie suivre.

A function `f` can be written as `\x -> f x` 

est l'abstraction Eta de toute utilisation tout en réduisant les expressions lambda? Est-ce seulement une manière alternative d'écrire certaines expressions?

Answer 1

La réduction eta/expansion est juste une conséquence de la loi qui dit que, compte tenu

f = g 

il doit être, que pour tout x

f x = g x 

et vice versa.

Par conséquent donné:

f x = (\y -> f y) x 

nous obtenons, en réduisant la bêta côté droit

f x = f x 

qui doit être vrai. Nous pouvons donc conclure

f = \y -> f y