Basic problem with lambda-calculus syntax

Question

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.

Answer 1

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.

Answer 2

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.