0

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

jack_the_beast
  • 101

1 Answers1

2

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?

MJD
  • 65,394
  • 39
  • 298
  • 580
  • ok, so I have to substitute the first argument variable of the function with the first expression after the function and so on? still don't understand what b(abc) in (λ abc.b(abc)) (λ sz.z) means – jack_the_beast Apr 26 '15 at 07:57
  • $b(abc)$ means that sometime later, if you find out what the values of $a, b$ and $c$ are, you're going to take the value $abc$ (which is a shorthand for $(a(bc))$_ give it as an argument to $b$. – MJD Apr 26 '15 at 08:00
  • @MDJ so a,b,c are actually function theirself? but if that is true, for example a(bc) written as a function λa.bc looks like a constant to me – jack_the_beast Apr 26 '15 at 08:05
  • Everything in lambda calculus is a function. $a(bc)$ does not mean the same as $\lambda a.bc$, which is the function which takes an argument $a$, ignores it, and always returns $bc$. – MJD Apr 26 '15 at 08:19
  • and what does it means then? – jack_the_beast Apr 26 '15 at 08:25
  • $a(bc)$ means you give $c$ as an argument to $b$, then take the result and give it as an argument to $a$. You're asking basic questions that should be on the first page of your book. Please go read the book. – MJD Apr 26 '15 at 08:43
  • but what do you mean with "give c as an argument to b"? as far a I know variables as b or c are just function alway themselves, something like λx.c am I right? – jack_the_beast Apr 26 '15 at 08:50