Beta Reduction in Lambda Calculus

Question

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.

Answer 1

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 ^_^