1
$\begingroup$

In the book of Haskell Programming by C. Allen, at page 39, it is given the following lambda expression

$$(𝜆𝑥𝑦.𝑥𝑥𝑦)(𝜆𝑥.𝑥𝑦)(𝜆𝑥.𝑥𝑧)$$

According to me, this equals to by applying the left two expression as an input for the rightmost expression

$$(𝜆𝑥.𝑥𝑦)(𝜆𝑥.𝑥𝑦)(𝜆𝑥.𝑥𝑧) = (𝜆𝑥.𝑥𝑦)(𝜆𝑥.𝑥𝑧)y = (𝜆𝑥.𝑥𝑦)yz = yzy,$$

and if we read the main expression as

However, the book the result is (I did not understand the argument they provide) $$𝜆𝑧.𝑧,$$

so which one of us is correct ?

Edit:

Now, after reviewing my calculation, I have

\begin{align} (𝜆𝑥𝑦.𝑥𝑥𝑦)(𝜆𝑥.𝑥𝑦)(𝜆𝑥.𝑥𝑧) &= [(𝜆x(𝜆y.xxy))(𝜆a.ab)](𝜆c.cd) \\ &= (𝜆y.(𝜆a.ab)(𝜆a.ab)y)(𝜆c.cd) \\ &= (𝜆a.ab)(𝜆a.ab)(𝜆c.cd) \\ &= [(𝜆a.ab)(𝜆a.ab)](𝜆c.cd) \\ &= [(𝜆a.ab)b](𝜆c.cd) = bb(𝜆c.cd) \end{align}

however, this result does not make any sense, so where is the mistake that I'm doing in here ?

Edit 2:

enter image description here

$\endgroup$
  • 1
    $\begingroup$ I see your mistake but my result does not coincide with the answer given in your book. Are you sure that the starting term and the result in the book are exactly as you wrote in the OP? Be careful of parentheses and names of variables. $\endgroup$ – Taroccoesbrocco Mar 18 '18 at 20:00
  • 1
    $\begingroup$ Are you sure you wrote the expression correctly? The result I am getting is 11(λ12) (in De Bruijn indices, so that alpha conversions are unnecessary). Can you post the book's explanation? $\endgroup$ – ljedrz Mar 18 '18 at 20:02
  • $\begingroup$ Why woudln't your result make sense? It's the correct one. $\endgroup$ – ljedrz Mar 18 '18 at 20:06
  • $\begingroup$ @ljedrz I guess I was not expecting to get such a result, and when I got it, I did not think on it too much :) You are right, it is totally a valid result to get. $\endgroup$ – onurcanbektas Mar 18 '18 at 20:08
  • 1
    $\begingroup$ @onurcanbektas - Pay attention that in your answer after your edit you are allowed to rename bound variables but your are not allowed to rename free variables. So, your answer should be $(yy)\lambda c.cz$, since $y$ and $z$ are free variables and you can't rename them. $\endgroup$ – Taroccoesbrocco Mar 18 '18 at 20:12
2
$\begingroup$

Your error (in the OP before your edit) is that $xxy$ stands for $(xx)y$, since application is left-associative. So, when in $xxy$ you substitute $\lambda x.xy$ for $x$, and $\lambda x. xz$ for $y$, what you get is \begin{align}\tag{1} \big((\lambda x.xy)(\lambda x.xy)\big)\lambda x.xz \end{align} which cannot be reduced to $(\lambda x.xy)(\lambda x.xz)y$. On the contrary, $(1)$ reduces in the following way: \begin{align} \big((\lambda x.xy)(\lambda x.xy)\big)\lambda x.xz =_\beta \big((\lambda x.xy)y\big)\lambda x.xz =_\beta (yy)\lambda x. xz \end{align}

In the book, the term $\lambda z.z$ is the result of the evaluation of the term $(\lambda xyz.xz(yz))(\lambda mn.m)(\lambda p.p)$, which has nothing to do with the term $(\lambda xy.xxy)(\lambda x.xy)(\lambda x.xz)$, it is just a different and completely unrelated example.

$\endgroup$
1
$\begingroup$

It appears that the book first presents one example and then just moves to another one, as $(λxy.xxy)(λx.xy)(λx.xz)$ is not equivalent to $(λxyz.xz(yz))(λmn.m)(λp.p)$.

In order to not get confused with clashing variable names I prefer to use De Bruijn indices; the initial expression would then be:

$(λλ221)(λ12)(λ12)$

and it would reduce (with normal order) as follows:

$(λ(λ13)(λ13)1)(λ12)$

$(λ12)(λ12)(λ12)$

$(λ12)1(λ12)$

$11(λ12)$ - equivalent to your result, $bb(λc.cd)$

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