3
$\begingroup$

According to the answer sheet it is supposed to reduce to $p$, but I dont know how. This is what I do

$$(\lambda x. (\lambda y. x \ y) \ x) \ (\lambda z.p)$$

I replace $x$ with $(\lambda z.p)$

$$\rightarrow (\lambda y. (\lambda z.p) \ y) \ (\lambda z.p))$$

And now $y$ with $(\lambda z.p)$ to get:

$$\rightarrow (\lambda z.p) \ (\lambda z.p)$$

How do you reduce this to $p$? (If it is possible)

$\endgroup$
4
$\begingroup$

In general, $\beta$-reduction $\to_\beta$ is a binary relation on $\lambda$-terms defined as follows: \begin{align} (\lambda z.t)u \to_\beta t\{u/z\} \end{align} where $t \{u/z\}$ is the $\lambda$-term obtained from $t$ by substituting $u$ for each free occurrence of $z$ in $t$.

Now, in your last $\lambda$-term $(\lambda z. p) (\lambda z.p)$ I guess $p$ is either a closed term (i.e. without free variables) or a variable distinct from $z$. In both cases, according to the general definition of $\to_\beta$: \begin{align} (\lambda z.p) (\lambda z.p) \to_\beta p \{\lambda z.p\ /\,z\} = p. \end{align}

Note that the argument (i.e. the subterm on the right) $\lambda z.p$ of the application $(\lambda z.p)(\lambda z.p)$ is simply discarded after the $\beta$-step, because there are no free occurrences of $z$ in $p$.

$\endgroup$
  • $\begingroup$ Perfect, thanks $\endgroup$ – Amoz Mar 5 at 15:43
1
$\begingroup$

$(\lambda z. p) \alpha$ reduces to $p$ for any $\alpha$.

$\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.