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$

2 Answers 2

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$
0
1
$\begingroup$

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .