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$
  • $\begingroup$ I think you are missing an $a$ somewhere in the first statement. $\endgroup$ – Yuval Filmus Jan 14 '17 at 16:29
  • $\begingroup$ @YuvalFilmus: You're correct. I just fixed it. $\endgroup$ – George Jan 14 '17 at 16:30
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, privacy policy and cookie policy

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