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$$


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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.