I am very new to the concept of lambda calculus. My question is mainly about the first bracketed term in the below expression.

The first term is supposed to flip the next two terms but I feel uneasy about using different letters.

The whole aim of this term is to reduce to B. When I write it out by hand I do get B but it wouldn't work in an interpreter so I feel like it might be wrong. Any help would be appreciated. Thanks

$ (\lambda s.\lambda t . ts )(\lambda x .\lambda y . \lambda z.y) (\lambda p . p A B C) $

  • $\begingroup$ What do you mean by 'using different letters'? $\endgroup$
    – Couchy
    Apr 22, 2018 at 19:26

1 Answer 1


I don't know what you mean with "using different letters". The first term represents a function that given two arguments ($s$ and $t$), applies the second argument ($t$) to the first argument ($s$). This should be the reduction:

(λs.λt.ts)(λx.λy.λz.y)(λp.pABC) $\rightarrow_\beta$

(λp.pABC)(λx.λy.λz.y) $\rightarrow_\beta$

(λx.λy.λz.y)ABC $\rightarrow_\beta$



You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .