1
$\begingroup$

I'm still trying to get the hang of lambda calculus:
I completed simplified some of these already but am lost on the last two. I did so far: \begin{align*} (\lambda x.x)y &\to y\\ (\lambda x.y)x &\to x \end{align*}

However, I'm not sure how to simplify these two:

\begin{gather*} (\lambda x.x y)(\lambda y.y z)\\ (\lambda x.x y)(\lambda a.a b) p \end{gather*} They are a little bit similar, but I'm not sure how to simplify these expressions.

$\endgroup$
  • 1
    $\begingroup$ $(\lambda x.y) \to x$ is not correct. A $\beta$ reduction would immediately result in $y$. not $x$. $\endgroup$ – Jay Mar 31 '16 at 15:58
3
$\begingroup$

Just follow the rules of $\beta$-reduction and remember that function application associates to the left, i.e. $f g h$ is just syntactic sugar for $(f g) h$.

I'll show the steps for $(\lambda x.x y)(\lambda y.y z)$.

  1. Strip off $\lambda$ from $(\lambda x.x y)$. You get the abstraction body $x\ y$, where $x$ is free now.
  2. Substitute the argument $(\lambda y.y z)$ for $x$ into $x\ y$: $(\lambda y.y z)$ y. Notice that I didn't do anything with $y$ during this step.
  3. Observe that the current $\lambda$-term is an application that can be reduced further. Again stripping off $\lambda$ we get $y\ z$ and substituting $y$ for $y$ results in the same term $y\ z$.

Here is the sequence of $\beta$-reductions without the intermediate steps: $$(\lambda x.x\ y)(\lambda y.y\ z) \rightarrow_\beta (\lambda y.y\ z) y \rightarrow_\beta y\ z.$$

The second problem can be dealt with in the same way.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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