2
$\begingroup$

From page 15 of Lambda Calculus and Combinators an Introduction:

Note 1.34 If $M \equiv aM_1 \ldots M_n$ where $a$ is an atom, and $M \triangleright_\beta N$, then $N$ must have form

$$ N \equiv a N_1 \ldots N_n $$

where $M_i \triangleright_\beta N_i$ for $i = 1, \ldots, n$. To see this, note that $M$ is really

$$ (( \ldots ((aM_1)M_2) \ldots)M_n) $$

when its parentheses are fully shown; hence each $\beta$-redex in $M$ must be in $M_i$. Also the same holds for each subterm $\lambda x. P$ whose bound variable might be changed in the reduction of$M$.

Question: Why is the following not a counter-example?

First let $M_1 = m_1 m_2 m_3$ for atomic constants $m_1$, $m_2$, $m_3$. Then let $N_1 = m_1$ and $N_2 = m_2 m_3$. Then:

$$ aM_1 \equiv a (m_1 m_2 m_3) \equiv (((am_1)m_2)m_3) \equiv ((a m_1)m_2 m_3) \triangleright_\beta a N_1 N_2 $$

Here, if I am correct, then we have a case where

$$ a M_1 \triangleright_\beta a N_1 N_2 $$

which seems to contradict the note.

$\endgroup$
2
  • $\begingroup$ I think you are missing an $a$ somewhere in the first statement. $\endgroup$ Commented Jan 14, 2017 at 16:29
  • $\begingroup$ @YuvalFilmus: You're correct. I just fixed it. $\endgroup$
    – George
    Commented Jan 14, 2017 at 16:30

1 Answer 1

3
$\begingroup$

Application in the lambda calculus is not associative. $m_1 m_2 m_3$ means $(m_1 m_2) m_3$ and is not equal to $m_1 (m_2 m_3)$. So the second equality you state doesn't hold. $$a(m_1 m_2 m_3) \neq ((a m_1) m_2) m_3$$ Further $$a N_1 N_2 = (a m_1)(m_2 m_3) \neq (a m_1) m_2 m_3 = ((a m_1) m_2) m_3$$

$\endgroup$

Your Answer

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

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