2
$\begingroup$

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 &= \lambda(x)\\ &= 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".

$\endgroup$
  • $\begingroup$ Much of what you write does not make sense to me. What is "λ(x)" supposed to be? Is that a legitimate syntax for a λ-expression? Whatever the theory, if you write something that is not syntactically correct, it does not mean anything, both in a formal and in an informal sense. - - - Also what do you mean by "As y is not in λ(x) it is not bound."? See answer. $\endgroup$ – babou Mar 3 '14 at 7:10
2
$\begingroup$

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> let z = 1
Prelude> let f x y = (+) ((+) z x) y
Prelude> :t f
f :: Integer -> Integer -> Integer
Prelude> f 1 1
3
Prelude> let f x = (+) ((+) z x)
Prelude> :t f
f :: Integer -> Integer -> Integer
Prelude> 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.

$\endgroup$
1
$\begingroup$

You do not have to try to interpret each side of the equality. This may be far too complicated in some cases, and $\lambda$-calculus is a formal calculus to begin with. It is better to know the calculus rules and apply them.

This said, you still have to read the expressions correctly:

$\lambda x.fzx$ is to be read as $\lambda x.((fz)x)$, that is a function that takes an argument $x$ and then returns the result from applying the function $f$ to $z$, and then applying the resulting function to $x$.

By definition of $\eta$-conversion you have: $\lambda x.fx \stackrel{\eta}{=} f$ whenever $x$ does not occur free in $f$

Though $\lambda$-calculus is a formal calculus, which can be analyzed without interpretation, you can try to understand intuitively the intent of such a rule. Essentially it says that if you have a function $f$ and you build from it a function $g=\lambda x.fx$ which takes one argument (here called $x$) and applies $f$ to it, then $g$ is equal to $f$. The idea is that $f$ and $g$ will both give the same result when applied to any argument.

Of course, in this definition, $f$ stands for any lambda expression.

There is however the requirement that no free variable named $x$ appear in $f$. The reason is that a free variable names something in the outer environment where $f$ is used. But, if $g$ replaces $f$, such an occurence of $x$ in $g$ would refer to the "parameter" $x$ in the definition of $g$, hence no longer to whatever it named in the outer environment.

But much of this explanation is for your intuition. The lambda game is formal, even though it does have interpretations.

Hence, if you apply this definition to the $\lambda$-expression $fzx$ , you get: $\lambda y.fzxy \stackrel{\eta}{=} fzx$ since the variable y does not appear free in $fzx$

Being equal, they can be substituted for each other in any context (precisely because of the restriction on free variables).

Hence $\lambda x.\lambda y.fzxy \stackrel{\eta}{=} \lambda x.fzx$

All this is of course remindful of scope rules in many programming languages, and that is not due to chance.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.