I came across the definition of beta reduction in Lambda Calculus which is :
$$(λx.M)N \rightarrow_β Μ[\space x:= N \space]$$ under the constraint that the $FV(N)$ are still free after the substitution.
I also came across three examples and the third one confuses me :
1st example : $$(λx.zx)w \rightarrow_β zw $$
2nd example : $$(λy.zy(λx.xy))w \rightarrow_β zw(λx.xw) $$
3rd example : $$λz.(λf .λx. f z x) (λy.y) \\ \rightarrow_β \\ λz.λx.(λy.y) z x \\ \rightarrow_β \\ λz.λx.z x \\$$
At first I thought that the left most bound variable gets substituted but in the 3rd example this does not seem to be the case.
Then I thought that given the fact that $N = (λy.y)$ is an abstraction maybe the $λf$ notation implies that it's argument will be an abstraction and so the bound variable $z$ will be "skipped".
Is my process here right and if that's the case why does the bound $z$ variable gets "skipped"? $z$ could be a notation for an abstraction as well.
Edit : Changed the word function to abstraction because as far as I understand everything can be represented via a function in $λ$-calculus.
Best Answer
Traditionally $\lambda$-abstraction "associates right", while function evaluation "associates left". That is, if we see $\lambda x. \text{stuff}$, then we assume $x$ is bound for the entirety of "stuff". If we want to explicitly show where the scope of the $\lambda x$ ends, we wrap the term in parentheses.
For example:
$$(\lambda f. \lambda x . f x) w \to_\beta \lambda x . w x$$
While
$$\lambda f . ((\lambda x . f x) w) \to_\beta \lambda f . f w$$
If there aren't any parentheses, then (by convention) we assume we're in the second case. Which agrees with the example in your question. Notice in examples $1$ and $2$, the author explicitly wraps the left $\lambda$-term in parentheses so that we know to apply it.
I hope this helps ^_^