I am studying Lambda Calculus. Could someone help with this reduction?
(λa.((aλb.λc.c)λd.λe.d))(λf.λg.f)
The actual result is λb.λc.c. But i need the steps to solve it
I have done these steps but i got stuck:
(λa.((aλb.λc.c)λd.λe.d))(λf.λg.f)
(λa.(aλb.λd.λe.d))(λf.λg.f)
(λf.λg.f)(λb.λd.λe.d)
(λg.λb.λd.λe.d)
Am i doing the steps wrong? Is there any rule I don't know?
visual evaluation
It can be challenging to build a visual model of steps using text alone. As the other answer notes, your () are used in a strange way. I hope this answer helps -
fix parens:
(λa.((a λb.λc.c) λd.λe.d)) (λf.λg.f)
eval:
(λa.a (λb.λc.c) (λd.λe.d)) (λf.λg.f)
=========
__________________________/
/
(λa.a (λb.λc.c) (λd.λe.d))
= \ \
| \ \
| \ \
(λf.λg.f) (λb.λc.c) (λd.λe.d)
========= /
_________/ ______/
/ /
(λf.λg.f) (λd.λe.d)
= \__
| \
(λg.(λb.λc.c)) (λd.λe.d)
=========
_______________/
/
(λg.λb.λc.c)
=======
/
/
λb.λc.c
higher intuition
Incidentally λb.λc.c is equivalent to Church's FALSE, λa.λb.b. Going back to your original program, given Church's booleans -
true := λa.λb.a
false := λa.λb.b
Take the original expression -
(λa.a (λb.λc.c) (λd.λe.d)) (λf.λg.f)
Rewrite using true and false -
(λa.a false true) true
Evaluates to -
true false true
Evaluates to -
false
We've leaned that (λa.a false true) gives us the inverse of a boolean. We can name it not -
true := λa.λb.a
false := λa.λb.b
not := λp.p false true
It works like this -
not true //=> false
not false //=> true