0
$\begingroup$

enter image description here

$$(\lambda x. x \text{ } x ) ( \lambda x . x \text{ } x )= (\lambda x. x \text{ } x) ( \lambda x . x \text{ } x)$$

Source

I am a bit confused on how this composition was done. When I do it, I get:

$$ \lambda x. (\lambda x. x \text{ } x) (\lambda x . x \text{ } x)$$

On what basis do I drop the exterior most $\lambda x.$?

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ It's not composition - it's application. $\endgroup$
    – Matthew Towers
    Feb 19 at 18:22
  • 1
    $\begingroup$ the point is that when you write a $\lambda$-term $M \ N$ the "meaning" - which can be evaluated using $\beta$-reduction - is what might be written $M(N)$ in conventional function notation, not $M \circ N$ as you've interpreted it. $\endgroup$
    – Matthew Towers
    Feb 19 at 21:55
  • $\begingroup$ All this might be a bit obscured by the overuse of variable name $x$. Perhaps there would be a bit less confusion if you wrote $(\lambda x. x x)(\lambda y. y y)$ instead? $\endgroup$
    – Stef
    Feb 20 at 12:30

1 Answer 1

Reset to default
4
$\begingroup$

You drop the $\lambda x$ because that's just how beta reduction is defined: $(\lambda v.M)(N) \triangleright_\beta M[v/N]$. In your example, $v$ is $x$, $M$ is $xx$, and $N$ is $\lambda x. xx$.

The intuition is that once you applied the function to an argument, then the slot is filled and no longer open for substitution with yet another argument ad infinitum. The "$\lambda x.$" is like the "$f(x) = $" in something like "$f(x) = x^2$". Once you apply the function, $f(2)$, the result is equivalent to $4$ (the part behind the equivalence sign with $2$ substituted for $x$), and not a new function of the form $f(x)$.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Or "$x \mapsto$" in "$f : x \mapsto x^2$" $\endgroup$
    – Stef
    Feb 20 at 12:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.