Beta Reduction in Lambda Calculus

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.

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

• So a rule of thumb would be : Apply $N$ to the first bound variable after the first parenthesis encountered ? Jan 7 '21 at 20:45
• At a glance, that sounds right, yes ^_^ Jan 7 '21 at 20:47