On a corollary of the Church-Rosser Theorem

127 Views Asked by At

In the proof of Corollary 1.41.5 from Hindley-Seldin, $\lambda$-Calculus and Combinators - An Introduction,

If $a$ and $b$ are atoms and $aM_1...M_m =_\beta bN_1...N_n$ then $a = b$ and $m = n$ and $M_i =_\beta N_i$ for all $i$ $\le m$ ,

the authors use the claim that both $M$ and $N$ reduce to some $T$ but assume that $T$ is of the form $T_1...T_m$ and that also $M_i$ reduces to $T_i$. I am not sure how it is a definite possibility, that there are $m$ terms (it could be lesser, too, right?) and how is $M_i$ $\beta$ reduces to $T_i$ it might be that $M_i$ $M_{i+1}$ reduce to say $T_j$ or something like that. Why is it not the case? Can someone explain this?

1

There are 1 best solutions below

0
On BEST ANSWER

This is explained in Note 1.34: You have to be aware that $a M_1\dots M_m$ is shorthand for $$(\ddagger)\quad\quad(\dots ((a M_1) M_2)\dots M_{m-1}) M_m $$ (in particular, $M_i M_{i+1}$ is not a sub-$\lambda$-term) and that therefore the $\beta$-redexes in this $\lambda$-term are precisely those coming from one of the $M_i$. Moreover, $\beta$-reduction at such a redex preserves the form $(\ddagger)$, so that you can conclude that any $\beta$-descendant of $(\ddagger)$ is of the form $(\dots ((a M^{\prime}_1) M^{\prime}_2)\dots M^{\prime}_{m-1}) M^{\prime}_m$ with $M_i\stackrel{\beta}{\to} M^{\prime}_i$.