How should $\lambda x. \lambda y. f z x y \stackrel{\eta}{=} \lambda x. f z x$ be read? I'm currently learning untyped $\lambda$-calculus and especially the $\eta$-reduction.

The professor hat the following in his slides:

$$\lambda x. \lambda y. f~z~x~y \stackrel{\eta}{=} \lambda x. f~z~x$$

I don't know how to read and understand this. Could you please explain it to me?

My try

On the left side and the right side is a function and they are $\eta$-equivalent.

The right side seems simpler, so I start with that.

It is a $\lambda$ function with one bound parameter $x$ and two unbound parameters $f$ and $z$. But here start my problems: What does $f~z~x$ mean? Is this a triple? Is it a function $f$ and a function $z$ and a function $x$?

I think in $\lambda$-calculus everything can be viewed as a $\lambda$-function, so $f$, $z$ and $x$ are functions. So the right side is the same as

$$\lambda(x) = f(z(x))$$

correct?

Applying the same logic on the left side, I get:

\begin{align}
\lambda x. \lambda y. f~z~x~y &amp;= \lambda(x)\\
&amp;= f(z(x(y)))
\end{align}

As $y$ is not in $\lambda(x)$ it is not bound. So we can simply remove it. Correct?

I think this could work. But I still don't know how to read it. I guess it will be something like:

"The lambda-function with the parameter $x$ that is a lambda function with a parameter y is f applied to z applied to x applied to y is eta-equivalent to the lambda function with the paramter x that is f applied to z applied to x".
Applications in Lambda calculus are assumed to be left associative, this means that $f~z~x~y$ is the same as $((f~(z))~(x))~(y)$.

With this is mind eta-conversion makes more sense. Wikipedia says:


  Eta-conversion expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments. Eta-conversion converts between λx.(f x) and f whenever x does not appear free in f.


This means that $\lambda x. \lambda y. f~z~x~y \stackrel{\eta}{=} \lambda x. f~z~x$ is assumed to be true because $y$ does not change the result of the application $f~z~x$, its value is applied after $f~z~x$ is already evaluated.

You can find out more about eta-conversion by playing with it in the Haskell REPL:

Prelude&gt; let z = 1
Prelude&gt; let f x y = (+) ((+) z x) y
Prelude&gt; :t f
f :: Integer -&gt; Integer -&gt; Integer
Prelude&gt; f 1 1
3
Prelude&gt; let f x = (+) ((+) z x)
Prelude&gt; :t f
f :: Integer -&gt; Integer -&gt; Integer
Prelude&gt; f 1 1
3


As you can se, it is easily possible to leave out a the parameter y without changing the meaning of your program.