Doing alpha conversions and beta reductions, Lambda Calculus

Question

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?

Answer 1

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.

Answer 2

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!