I'm triyng to understanding lambda calculus but I have some difficulty espacially when websites or books I search starts to make things a bit more complicated.
what I've understood by now is: given (λa.abc)(x)(y) we "solve" it substituting the first variable of the body with the first expression after the function, the second with the second and so on. resulting in: (λx.xyc)
I hope that's correct. but when things do a step further I get lost, for example, given the following:
(λ abc.b(abc)) (λ sz.z)
I don't understand what happens. the webpage I'm reading says that it becomes this:
λ bc.b((λ sz.z) bc)
but why? i understand the substitution, what I don't understand is: 1.why the first 'a' disappears 2.why the body of the function it's written like b(abc), what's the difference with babc?
can someone help me? even suggesting resources would be appreciated