[Solved]: Combinatory interpretation of lambda calculus

The equivalence is just equivalence in the equational $lambda$-theory under discussion. In this case, it’s the theory outlined in Table 1. Note that this theory does not include $eta$: doing so would make the theory extensional, and the point is eventually that $xi$ respects $lambda$’s intensionality, while it would make CL partially extensional. I am not sure why the other answer mentions $eta$. Note that in $lambda$: $$(M =_beta N) Longrightarrow (lambda x.M =_beta lambda x.N) tag{1}$$ This should be intuitively obvious: if $M$ is $beta$-convertible to $N$ when it stands by itself, then it is also $beta$-convertible to $N$ when it is a subterm of $lambda x.M$. The $xi$-rule, defined as begin{align} M &;= N hline (lambda x.M) &;= (lambda x.N) tag{$xi_lambda$} end{align} makes this inference directly possible when it is part of a $lambda$-theory. Its CL analogue would be: begin{align} M &;= N hline (lambda^* x.M) &;= (lambda^* x.N) tag{$xi_{CL}$} end{align} Now, the point is that in CL, the following does not hold: $$(M =_w N) Longrightarrow (lambda^* x.M =_w lambda^*x.N) tag{2}$$ In other words, if two terms are weakly equal, then this is not necessarily true for their pseudo-abstracted versions. Consequently, if we add $xi_{CL}$ to a CL theory, then we start equating terms which have different normal forms. Note. Here, $M =_w N$ denotes weak equality. It means that $M$ can be converted into $N$ (and vice versa) by a series of $mathsf{S}$ and $mathsf{K}$ contractions (possibly also $mathsf{I}$, if it is part of the theory). As you probably know, $=_w$ is the CL analogue of $=_beta$. $lambda^*$ is the pseudo-abstractor as defined on page 5 of your document. It has the following property: $$(lambda^*x.M)N rhd_w [N/x]M tag{3}$$ This property makes it easy to find a CL analogue for any $lambda$-term: just change $lambda$ to $lambda^*$ and apply the translations according to the definition of $lambda^*$. To be clear, the ‘counter-example’ in this answer is not a counter-example to (2). Because if we have: $$M = x tag{4}$$ $$N = (lambda^*z.z)x tag{5}$$ Then $N$ really denotes (applying the translations of page 5, and the fact that $mathsf{I}$ is defined as $mathsf{SKK}$ at the end of page 4): $$N = (lambda^*z.z)x = mathsf{I}x = mathsf{SKK}x tag{6}$$ Since $mathsf{SKK}x rhd_w mathsf{K}x(mathsf{K}x) rhd_w x$, we indeed have that $M =_w N$. However, if it is a counter-example, we should then have that $(lambda^* y. M) not=_w (lambda^* y. N)$. But if we translate, we actually get: $$(lambda^* y. M) = (lambda^* y. x) = mathsf{K}x tag{7}$$ $$(lambda^* y. N) = (lambda^* y. mathsf{SKK}x) = mathsf{K}(mathsf{SKK}x)tag{8}$$ And is easy to verify that (7) and (8) are still weakly equal, for: $$mathsf{K}(mathsf{SKK}x) rhd_w mathsf{K}(mathsf{K}x(mathsf{K}x)) rhd_w mathsf{K}x tag{9}$$ Now, a proper counter-example to (2) would be: $$M = mathsf{K}xy$$ $$N = x$$ Since $mathsf{K}xy rhd_w x$, we definitely have that $M =_w N$. However, if you translate carefully for the abstracted versions, then you will see that both are distinct normal forms – and these cannot be convertible according to the Church-Rosser theorem. First we check $M’$: begin{align} M’ &= lambda^* x.mathsf{K}xy &= mathsf{S}(lambda^* x.mathsf{K}x)(lambda^* x.y) &= mathsf{S}(lambda^* x.mathsf{K}x)(mathsf{K}y) &= mathsf{S}(mathsf{S}(lambda^* x.mathsf{K})(lambda^* x.x))(mathsf{K}y) &= mathsf{S}(mathsf{S}(lambda^* x.mathsf{K})(mathsf{I}))(mathsf{K}y) &= mathsf{S}(mathsf{S}(lambda^* x.mathsf{K})(mathsf{SKK}))(mathsf{K}y) &= mathsf{S}(mathsf{S}(mathsf{KK})(mathsf{SKK}))(mathsf{K}y) end{align} Here you can verify that $M’$ is a normal form. Here you can check that $(lambda^* x.Kxy)P rhd_w P$, as you should expect if $lambda^*$ is supposed to behave like an abstractor for CL. (Click the blue links to perform weak contractions.) Now we check $N’$: begin{align} N’ &= lambda^*x.x &= mathsf{I} &= mathsf{SKK} end{align} Which is obviously a normal form different from $M’$, so $M’ not=_w N’$ by the Church-Rosser theorem. Note also that $N’P rhd_w P$, i.e. $M’$ and $N’$ ‘produce the same output’ for arbitrary inputs $P$. We have now proven that (2) does not hold in CL, and that a CL theory incorporating $xi$ would therefore equate terms that are not weakly equal. But why do we care? Well, first of all, it makes the combinatory interpretation of $lambda$ imperfect: apparently not all metatheoretic properties carry over. In addition, and perhaps more importantly, while there exist extensional theories of $lambda$ and CL, they are originally and commonly kept intensional. Intensionality is a nice property because $lambda$ and CL model computation as process, and from this perspective two different programs (specifically, terms that have a different normal form) that always produce the same results (given equal inputs) are not to be equated. $xi$ respects this principle in $lambda$, and if we want to make $lambda$ extensional, we could just add e.g. $eta$. But the introduction of $xi$ in CL would no longer make it completely intensional (in fact, only partially so). And this is the reason for $xi$’s ‘notoriety’, as the article puts it.