question about lambda calculus

201 Views Asked by At

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

1

There are 1 best solutions below

7
On

What you wrote is not correct. You have a fundamental misunderstanding.

The idea of the lambda calculus is that a lambda expression, say

$$\lambda x.\sin(2x)$$

is a function that takes an argument, called $x$, and returns $\sin(2x)$. For example, if the argument is $\frac{3\pi}2$, then the result is $\sin(2\cdot\frac{3\pi}2)$:

$$(\lambda x.\sin(2x)) \left(\frac{3\pi}2\right) \Longrightarrow \sin\left(2\cdot\frac{3\pi}2\right)$$

Notice that the $x$ has disappeared, because it is replaced with $\frac{3\pi}2$, and so has the $\lambda$ prefix, because the result is not a function.

The result of reducing $(λa.abc)(x)(y) $ is not what you said, it is $(xbc)(y)$. It cannot be reduced further. The $\lambda a.abc$ is like a function that takes a single argument $a$ and then applies the value of $a$ to the value of $b$ and then applies the result to $c$. The application $(λa.abc)(x)$ gives $x$ to the function as its argument $a$, so it yields $(xbc)$, which says that $x$ should be applied to whatever $b$ is and then the result to $c$.

I hope this clears up some of your confusion. Can you understand your $(λ abc.b(abc)) (λ sz.z)$ example now?