0
$\begingroup$

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

$\endgroup$
  • $\begingroup$ What do you mean by 'using different letters'? $\endgroup$ – Couchy311 Apr 22 '18 at 19:26
0
$\begingroup$

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

$\endgroup$

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.