I have started learning lambda calculus from the book by Hindley and Seldin.

It brought up the concept with the function $x-y$, first as a function of $x$ and then as a function of $y$. In a way, it emphasized the difference between treating the expression as a function of $x$ and function of $y$, giving separate names to the functions.

$$f(x,y) = x-y \qquad\text{and}\qquad g(y,x) = x -y$$ and, in $\lambda$ notion, $$h = \lambda xy.x-y \qquad\text{and}\qquad g = \lambda yx. x-y\,.$$

If I am not wrong then it can be inferred that $f =\lambda x .(x-y)$ means that while computing the value of the expression the expression will vary only with $x$ and similarly when $\lambda$ is placed with $x$ the other variable $y$ will be kept as a constant.

But then it said that this can be denoted as, with $h$ being the common name of the function $$h = \lambda xy.(x-y)\qquad\text{and}\qquad h = \lambda yx.(x-y)\,.$$
Is it so that in the above expression the variable which is adjacent to $\lambda$ receives the value and the other one is constant? The above function is called a two-place function; what does that mean?

Then he introduces the following function in $\lambda$ notation calling it a one-point function: $$h^\star = \lambda x .(\lambda y . x−y)$$ and says that, for each number $a$, we have $h^\star(a)=\lambda y . a−y$. Here $a$ is being provided as an argument but $\lambda$ is placed near $y$. Why is this?

And then it deduces that $(h^\star(a))(b)=(\lambda y . a−y)(b) = a−b = h(a,b)$ and says $h^\star$ can be viewed as "representing" $h$. Is "representing" a technical term? How was $(\lambda y . a−y)(b) = a−b$ concluded?


1 Answer 1


If I am not wrong then it can be inferred that :

$f=\lambda x.(x−y)$ means that while computing the value of the expression the expression will vary only with "x" and similarly when "lambda " is placed with x the other variable y" will be kept as a constant .

Yes, intuitively that's how it works.

What you're looking is called Currying and it's explained fairly early in this book (in fact, I think it's the next section but I don't have a copy now to check). So when we want to work with functions with many arguments we often do it like this:

$$ f(x,y,z) = x\times y + z$$

But you can break this into simpler functions, $(x \times y)$ and $(+z)$. The multiplication can be broken into even simpler terms, first I provide $x$, then just multiply by $y$, that is, $f^{\star}(y) = x\times y$.

Defining some 1-argument functions:

$$ \begin{align*} plus_z &:= f^\prime(s) = s + z\\ times_y &:= f^\star(s) = s\times y \end{align*} $$

Combining these we can rewrite $f$ as:

$$ f(x,y,z) = f^\prime(f^\star(x)) = plus_z (times_y ~ x) $$

Writing this in using $\lambda$ we have:

$$ \lambda x y z. (x\times y + z) \equiv \lambda x.\bigg(\lambda y. \Big(\lambda z. (x\times y + z ) \Big) \bigg)$$

What the author has shown is that you can take a function with many arguments and transform it into many simpler functions with just one argument, the bigger function is just a composition of the simpler ones.

So just how the proof works? In your book the following functions are defined:

$$ \begin{align*} h^\star &= \lambda x . (\lambda y . x − y)\\ h(x,y) &= x-y \end{align*} $$

You want to show that $ h^\star = h$. To do that just take any two arguments $a$ and $b$. First evaluate $h^\star$ in $a$.

$$ h^\star(a) = (\lambda x. (\lambda y. x - y))(a) = \lambda y. a - y$$

This gives you a simpler one argument function $h^\prime = h^\star(a)$.

How was $(λy.a−y)(b)=a−b$ concluded

The same way $(\lambda x. (\lambda y. x - y))(a) = \lambda y. a - y$ was concluded. Just evaluate the function in $b$.

$$ h^\prime(b) = (h^\star(a))(b) = (\lambda y. a - y)(b) = a - b$$

Which is the same result computed by $h(a,b) = a - b$.

  • $\begingroup$ How in the last line h*(a)(b) = a-b concluded ? Could you elaborate this part ? $\endgroup$ Commented Feb 18, 2017 at 18:59
  • $\begingroup$ Sorry ..no .. how is (lambda*y .a -y)(b) = a -b ...?Any distribution rule ? $\endgroup$ Commented Feb 18, 2017 at 19:10
  • $\begingroup$ Beware, this is not a times (multiplication), it's like 'plugging' values in a function argument, so for now think it's something like a textual substitution. The argument is $y$ and the function is $a - y$, so $b$ applied to $\lambda y. a - y$ yields $a-b$ . $\endgroup$
    – Aristu
    Commented Feb 18, 2017 at 19:12
  • $\begingroup$ Not a times ? Even with textual substitution I cannot conclude how the last expression came out to be "a-b". $\endgroup$ Commented Feb 18, 2017 at 19:13
  • $\begingroup$ @AgniveshSingh Btw, if this answer is still not useful to you I can change it to address your problem. $\endgroup$
    – Aristu
    Commented Feb 20, 2017 at 20:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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