10
$\begingroup$

According to Peter Selinger, The Lambda Calculus is Algebraic (PDF). Early in this article he says:

The combinatory interpretation of the lambda calculus is known to be imperfect, because it does not satisfy the $ξ$-rule: under the interpretation, $M = N$ does not imply $\lambda x.M = \lambda x.N$ (Barendregt, 1984).

Questions:

  • What kind of equivalence is meant here?
  • Given this definition of equivalence, what is a counter-example of the implication?
$\endgroup$
7
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I can't comment on quality because I know little of the subject, but this looks like a bit of work. Appreciated, thanks! $\endgroup$ – Raphael Jul 23 '14 at 17:20
  • $\begingroup$ Indeed, the post ended up longer than I had anticipated. Thanks for your comment. :) $\endgroup$ – Roy O. Jul 23 '14 at 18:12
  • 2
    $\begingroup$ Oh, that. Happens. Regularly. $\endgroup$ – Raphael Jul 23 '14 at 18:24
3
$\begingroup$

EDIT This answer is incorrect, as the other answerer correctly pointed out. I used the translation into combinatory logic from Asperti & Longo, which is subtly different from the one in Selinger.

In fact, this illustrates a crucial point: "the combinatory interpretation" of lambda calculus is not a single thing! Different authors do it slightly differently.

I'm leaving my answer here for posterity, but the other answer is better.


Equivalence in this context is defined by Tables 1 and 2 in Selinger's paper. However, a slightly different axiomatisation may make things a little more clear.

What it really means is that two terms are convertible in the $\lambda$ theory. We can define "convertibility" by the following two axioms:

  • $\beta$. $(\lambda x. M) N = [N/x]M$, if $x$ free for $N$ in $M$
  • $\eta$. $\lambda y. M y = M$, if $y$ not free in $M$

plus, of course, the usual axioms and inference rules needed to make $=$ a congruence. From this, it should be obvious that any counter-example is going to rely on the free variable condition on the $\eta$ rule being broken.

I think this is probably the simplest:

$$M = x$$ $$N = (\lambda z. z) x$$

You can verify for yourself that $\lambda y. M = \lambda y. N$, but their respective combinatorial interpretations are not equal under the rules in Table 2.

$\endgroup$
  • $\begingroup$ What I don't understand about your answer: 1) why mention $\eta$, while the theory in Table 1 does not include it and is clearly intensional? 2) How are the combinatory interpretations of $\lambda y.M$ and $\lambda y. N$ not equal? The derivation in my answer shows that they are. 3) The $\xi$-rule is not addressed, while that is the culprit in the issue. $\endgroup$ – Roy O. Jul 24 '14 at 0:17

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.