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