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.