Lambda Calculus Function Reduction steps

Question

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?

What have you tried? Where did you get stuck? Show us your own effort! — lemontree
I got lost in parenteses ;) just fixed an error in assume part. Now it should be correct. Oh and if my post answers your question, feel free to also upvote it ;) — rsm
@Pater The correction rsm made on the bracketing of your term is wrong, the starting term with the bracketing as you put it is correct. (The reduction series rsm showed is also correct.) — lemontree

Mulan Mulan · Accepted Answer · 2019-09-07T19:06:41

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

Lambda Calculus Function Reduction steps

1 Answers