I have a problem with lambda-calculus, that is, I just don't get the formalism at all.

So, I found in a previous question a lot of resources to study it from the scratch, and I was focusing on the notes by Selinger. Thus, at page 8, concerning the translation of $f \mapsto f \circ f$ in lambda notation we read:

In the lambda calculus, $f \circ f$ is written as $\lambda x.f (f (x))$...

This is something I really do not get. How to read this expression?
[I see why we don't have something like $\lambda f . f(f)$.]

Thus, is this what you do when you define extensionally a function in this language that should work with functions always intensionally? You basically declare that there is a function, whose domain is $x$ (whatever $x$ is) and you are interested in the composition of this function with itself?

... and the operation that maps $f$ to $f \circ f$ is written as $\lambda f. \lambda x.f(f(x))$.

Now, no matter which problems I had before, I am fine with this, since I basically read it as $\lambda f. A$, where $A$ is an expression (not sure this is the right term for such an object) where there is $f$ and that tells us something about the behavior of $f$.
[In other words, this is not that different from something like $\lambda x. x^2$, thus, again, that's fine]

Then the author goes on writing:

The evaluation of higher-order functions can get somewhat complex; as an example, consider the following expression: $$(\lambda f. \lambda x.f (f (x)))(\lambda y.y^2 )􏰂 (5)$$

Convince yourself that this evaluates to $625$.

Could you please help me to convince myself that this is evaluates at $625$?

I read this as, say , $(A) (B) (5)$. So, I suspect what this expression wants to tell me is, take a function $f$ and let it maps to the $f \circ f$, moreover, incidentally, let $f$ be defined as $f(y) := y^2$. Then, if you evaluate at $5$ the composition with itself of such function compose, you get $625$. Fair enough. Still, I really don't get the syntax.

Is this all about saying the following: in expression $(A)$ we say what we want to do with a function (defined extensionally), but still - since we work with functions only intesionally, we still need to know what this function really looks like, which comes from $(B)$.

Any feedback is most appreciated.
Thank you for your time.


As far as I'm concerned, the lambda calculus operates only extensionally: it defines functions by telling you, for every $x$, what the function does to $x$.

For your expression, $$(\lambda f.\lambda x.f(f(x)))(\lambda y. y^2)(5)$$ first consider the first part, $(\lambda f.\lambda x.f(f(x)))(\lambda y. y^2)$. By $\beta$-reduction, this is $$\lambda x.[(\lambda y.y^2).(\lambda y.y^2)(x)] = \lambda x.(\lambda y.y^2)(x^2) = \lambda x.x^4$$

So it just remains to find $(\lambda x.x^4)(5)$, which is 625 by $\beta$-reduction.

The process of evaluating something in the lambda calculus without fixed-point combinators is totally mechanical: just apply the reduction rules until you get the answer.

I read the expression $\lambda x. f(f(x))$ as "the function mapping $x$ to $f(f(x))$".

Digression on "is $f$ a function?"

Note that one can use the lambda calculus in such a way that everything is a function. One can define the Church numerals as specific functions that stand for natural numbers, and one can define the predicates "TRUE" and "FALSE" as specific functions, and one can define the expression "if $\mathrm{TRUE}(a)$ then $b$ else $c$" as a function which takes arguments $a, b, c$. [Strictly speaking, there are no multi-place functions; either you must curry, or you must encode a pair as a single object somehow.]

So your worry about "is $f$ even a function?" is misplaced in this context, because every term is a function by default. The number $5$, even, is shorthand for a function.

However, this is a level of detail one rarely works with; much like one rarely cares about the implementation of the ordered pair in set theory, but simply works with them directly.

  • $\begingroup$ Thanks a lot for your – enlightening – answer (since it shows how to reason in lambda calculus). Two points: the first is a comment, the second a question. (1) Thus, I would say that it looks a rather odd decision on the side of the Selinger to introduce such a formula before talking about $\beta$-reduction (I just finished to look what this is all about). Indeed, if – as you write – you approach it by thinking in terms of $\beta$-reduction, how should we suppose to convince ourselves that expression ends up being $625$ without knowing about $\beta$-reduction? $\endgroup$ – Kolmin Oct 13 '17 at 10:06
  • $\begingroup$ (2) You write at the end that you read $\lambda x. f (f(x))$ as "the function mapping $x$ to $f(f(x))$", thus it is a rule. However, what is $f$? Could you clarify this point? I suspect that the expression alone $\lambda x. f (f(x))$ does not make sense, since we don't know anything about $f$, and not just because it is free, but because – it looks like strictly speaking we don't even know it is actually a function. (I am afraid I am missing something crucial) $\endgroup$ – Kolmin Oct 13 '17 at 10:12
  • 1
    $\begingroup$ @Kolmin In the context of (2), I think of $f$ as a lambda-term which has been defined somewhere else, but with which I'm currently reasoning without needing to know its definition. (Yes, indeed, $\lambda x. f(f(x))$ makes no sense in a vacuum; as a $\lambda$-term it only makes sense if it's within something that defines $f$.) It's like saying I read $x \mapsto f(f(x))$ as "the function mapping $x$ to $f(f(x))$"; that makes no sense for exactly the same reason, but if it's read in the context of something that's defined $f$ already, then it will make sense. I will, however, flesh out my answer. $\endgroup$ – Patrick Stevens Oct 13 '17 at 11:38
  • $\begingroup$ Thus, just to calibrate the edit, the way in which you define $f$ is actually via the expression $\lambda y. y^2$ in that specific example, otherwise even $\lambda f. \lambda x. f(f(x))$ does not make any sense in a vacuum, right? $\endgroup$ – Kolmin Oct 13 '17 at 11:43
  • 1
    $\begingroup$ @Kolmin I added a final section. $\lambda f. \lambda x. f(f(x))$ does make sense in a vacuum. It's a $\lambda$-term which corresponds to a function, that takes two arguments (a function $f$ and a term $x$) and outputs $f(f(x))$. [Or, strictly, it corresponds to a function that takes one argument (a function $f$), and outputs a function which takes one argument (a term $x$) and outputs $f(f(x))$.] $\endgroup$ – Patrick Stevens Oct 13 '17 at 11:46

The lambda calculus is a syntactic formalism. The (abstract) syntax of lambda terms is as follows. Given a collection of symbols $V$ elements of which we'll call variables, a lambda term is then either a variable (i.e. element of $V$), a pair of lambda terms, $M$ and $N$, which we'll call an application and write $M(N)$, or a pair of a variable, call it $x$, and a lambda term, $M$, which we'll call a lambda abstraction and write $(\lambda x.M)$.

So what is $f$ in $\lambda x.f(f(x))$? It's a lambda term as that's all it can be if the whole expression is a lambda term. Furthermore, it is a variable as it clearly isn't an application or a lambda abstraction. And that's it. $f$ is not a function. A variable, in this context, is just a symbol. It doesn't refer to anything, nor do we need it to to perform calculations.

However, the point of the lambda calculus is to provide a syntactical formalization of informal notations such as $x\mapsto f(f(x))$. This will be done, but on this, the second page of the first chapter titled "Introduction" of a 120 page document, Selinger is simply providing context and a rough outline of what this is all about and, in that example, is relying upon informal intuitions you may (or may not) have. The formal definitions don't begin until a few pages later, page 11, at the beginning of Chapter 2, The Untyped Lambda Calculus. Ultimately, the goal is build up notions such as "variables referring to things" and "functions", starting from, roughly speaking, just letters on a page. If you found that example confusing, simply proceed further since the point of the remainder of the notes is to flesh out and formally articulate the topics touched upon in the introduction.

  • $\begingroup$ Thanks a lot for your reply! In particular I liked a lot your explicit mentioning of the fact that I should see certain objects simply as symbols. Concerning your point on Selinger's notes, I went on and I think they are quite nice. I just had found – and still find – odd that en explicit exercise (i.e., Exercise 1) asks you something concerning an intuition that at that point of the notes, as you pointed out, you can or you cannot have, while usually exercises are used to test a 'concrete' intutition. But, anyway, that's the choice of the author. $\endgroup$ – Kolmin Oct 14 '17 at 7:56

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.