Doing alpha conversions and beta reductions, Lambda Calculus I am attempting to perform Lambda calculations. I have the following information.
T = $\lambda xy.x$
F = $\lambda xy.y$
A = $\lambda xy.xyF$
I attempted to perform Beta reduction and alpha conversion on ATF.
$\lambda xy.xyF (TF) $
=$[(\lambda xy.xy)(\lambda ab.b)](\lambda cd.c)(\lambda eg.g) $
=$[(\lambda cd.c)(\lambda ab.b)](\lambda eg.g) $
=$[(\lambda eg.g)(\lambda ab.b) $
=$[\lambda ab.b $
=F
Is what I am doing here correct in terms of the conversions and ructions? Is there a way of checking the final result of this after all the applications?
 A: You already made a mistake when you wrote
$$\lambda xy.xyF (TF) = [(\lambda xy.xy)(\lambda ab.b)](\lambda cd.c)(\lambda eg.g) $$
Your $[(\lambda xy.xy)(\lambda ab.b)]$ on the right-hand side is incorrect: that is not $A = \lambda xy.xyF$, but rather $(\lambda xy.xy)F$.  These are not at all the same, similar to how $(8-4)-1$ is not the same as $8-(4-1)$.  The first lambda-expression is a function which gets arguments $x$ and $y$, applies $x$ to $y$, and applies the result to $F$.  The second one takes the identity function $\lambda xy.xy$ and applies it to $F$.
You are supopsed to be evaluating $ATF$.  That is, you want to apply $A$ to $T$, then apply the result of that to $F$.  $ATF$ is shorthand for $(AT)F$.
Since $A=\lambda xy.xyF$, you want $$(AT)F = ((\lambda xy.xyF)T)F$$ which, substituting $T$ into the body of $A$ in place of $x$, reduces to $$(\lambda y.TyF)F.$$
Perhaps you can take it from there.
A: Here's my try:
$$
AT=((\lambda x y. x y F)T)
=(\lambda x y. x y F)(T=\lambda x y. x)
=(\lambda x y. x y F)(T=\lambda x. x)
=(\lambda y. TyF)
$$
Then
$$
ATF=((\lambda y. TyF)F)
=(\lambda y. TyF)(F=\lambda xy. y)
=(\lambda y. TyF)(F=\lambda y. y)
=TFF
$$
So $ATF=TFF$.
Please comment whether I'm right. Thanks!
