Lambda calculus' syntax disambiguation

120 Views Asked by At

I've got a few questions about $\lambda$ calculus' syntax and how to interpret it.
Most of these questions sparked from reading this notes.

First thing first, an application 's syntax is defined as the juxtaposition of two $\lambda$ terms : $M N$.

A $\beta$ - reduction occurs when we have a $\lambda$ - abstraction followed by a $\lambda$ - term.

That said how should I interpret the following expression?

$$\lambda f.\lambda x.f\,\,(f x)$$
The notes suggest $(f x)$ is part of the function's body, conveying to the expression the meaning of a function of two arguments, $f\text{ and }x$, that applies the first one to the second one twice.

Yet, since it is not compulsory to have unique names in expressions, what prevents us by interpreting it as the application of a function of two arguments, $f \text{ and the unused } x$, (i.e. $\lambda f.\lambda x.f$) to the result of the application of some other term f to x?(i.e. $(f x)$)

On a similar note, in the expression :
$$ x(\lambda y.y)z $$
$(\lambda y.y)z$ are said to be arguments to x. Why can't we consider $(\lambda y.y)z$ as an application yielding :
$$ x \,\,z $$

Thanks a lot to anyone reading this, let me know if edits are necessary!