Interprétation combinatoire du lambda calcul

Selon Peter Selinger , le Lambda Calculus est algébrique (PDF). Au début de cet article, il dit:

L'interprétation combinatoire du calcul lambda est connue pour être imparfaite, car elle ne satisfait pas à la règle $ξ$ : selon l'interprétation, $M = N$ n'implique pas $\lambda x.M = \lambda x.N$ (Barendregt, 1984).

Des questions:

• Quel genre d'équivalence veut-on dire ici?
• Compte tenu de cette définition de l'équivalence, qu'est-ce qu'un contre-exemple de l'implication?

L'équivalence est juste l'équivalence dans la théorie équationnelle en discussion. Dans ce cas, c'est la théorie décrite dans le tableau 1. Notez que cette théorie n'inclut pas : cela rendrait la théorie extensionnelle, et le fait est finalement que respecte l' intensionnalité de , alors que cela ferait CL partiellement extensionnel. Je ne sais pas pourquoi l'autre réponse mentionne .$\lambda$$\eta$$\xi$$\lambda$$\eta$

Notez que dans :$\lambda$

$$(M =_\beta N) \Longrightarrow (\lambda x.M =_\beta \lambda x.N) \tag{1}$$

Cela devrait être intuitivement évident: si est -convertible à quand il se tient par lui-même, alors il est -convertible à quand c'est un sous-terme de .$M$$\beta$$N$$\beta$$N$$\lambda x.M$

La règle , définie comme rend cette inférence directement possible lorsqu'elle fait partie d'une théorie . Son analogue CL serait: $\xi$

$$\begin{align} M &\;= N \\ \hline (\lambda x.M) &\;= (\lambda x.N) \tag{$\xi_\lambda$} \end{align}$$ $\lambda$ $$\begin{align} M &\;= N \\ \hline (\lambda^* x.M) &\;= (\lambda^* x.N) \tag{$\xi_{CL}$} \end{align}$$

Maintenant, le fait est qu'en CL, ce qui suit ne tient pas :

$$(M =_w N) \Longrightarrow (\lambda^* x.M =_w \lambda^*x.N) \tag{2}$$

En d'autres termes, si deux termes sont faiblement égaux, cela n'est pas nécessairement vrai pour leurs versions pseudo-abstraites.

Par conséquent, si nous ajoutons à une théorie CL, alors nous commençons à assimiler des termes qui ont différentes formes normales.$\xi_{CL}$

---

Remarque. Ici, dénote une faible égalité. Cela signifie que peut être converti en (et vice versa) par une série de contractions et (éventuellement aussi , si cela fait partie de la théorie). Comme vous le savez probablement, est l'analogue CL de .$M =_w N$$M$$N$$\mathsf{S}$$\mathsf{K}$$\mathsf{I}$$=_w$$=_\beta$

$\lambda^*$ est le pseudo-abstrait tel que défini à la page 5 de votre document. Il a la propriété suivante:

$$(\lambda^*x.M)N \rhd_w [N/x]M \tag{3}$$

Cette propriété facilite la recherche d'un analogue CL pour n'importe quel -term: il suffit de changer en et d'appliquer les traductions selon la définition de .$\lambda$$\lambda$$\lambda^*$$\lambda^*$

---

Pour être clair, le «contre-exemple» dans cette réponse n'est pas un contre-exemple à (2). Parce que si nous avons:

$$M = x \tag{4}$$ $$N = (\lambda^*z.z)x \tag{5}$$

Alors signifie vraiment (en appliquant les traductions de la page 5, et le fait que est défini comme à la fin de la page 4):$N$$\mathsf{I}$$\mathsf{SKK}$

$$N = (\lambda^*z.z)x = \mathsf{I}x = \mathsf{SKK}x \tag{6}$$

Depuis , nous avons en effet que . Cependant, s'il s'agit d'un contre-exemple, nous devrions alors avoir cela . Mais si nous traduisons, nous obtenons en fait:$\mathsf{SKK}x \rhd_w \mathsf{K}x(\mathsf{K}x) \rhd_w x$$M =_w N$$(\lambda^* y. M) \not=_w (\lambda^* y. N)$

$$(\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}$$

Et il est facile de vérifier que (7) et (8) sont encore faiblement égaux, pour:

$$\mathsf{K}(\mathsf{SKK}x) \rhd_w \mathsf{K}(\mathsf{K}x(\mathsf{K}x)) \rhd_w \mathsf{K}x \tag{9}$$

Maintenant, un contre-exemple approprié à (2) serait:

$$M = \mathsf{K}xy$$ $$N = x$$

Depuis , nous avons certainement que . Cependant, si vous traduisez soigneusement pour les versions abstraites, alors vous verrez que les deux sont des formes normales distinctes - et celles-ci ne peuvent pas être converties selon le théorème de Church-Rosser.$\mathsf{K}xy \rhd_w x$$M =_w N$

On vérifie d'abord :$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}$$ Ici, vous pouvez vérifier que est une forme normale. Ici, vous pouvez vérifier que , comme vous vous en si est censé se comporter comme un abstrait pour CL.$M'$$(\lambda^* x.Kxy)P \rhd_w P$$\lambda^*$

Maintenant, nous vérifions : $N'$

$$\begin{align} N' &= \lambda^*x.x \\ &= \mathsf{I} \\ &= \mathsf{SKK} \end{align}$$

Ce qui est évidemment une forme normale différente de , donc par le théorème de Church-Rosser. Notez également que , soit et « produisent la même sortie » pour les entrées arbitraires .$M'$$M' \not=_w N'$$N'P \rhd_w P$$M'$$N'$$P$

Nous avons maintenant prouvé que (2) ne tient pas dans CL, et qu'une théorie CL incorporant équivaudrait donc à des termes qui ne sont pas faiblement égaux. Mais pourquoi on s'en soucie?$\xi$

Eh bien, tout d'abord, cela rend imparfaite l' interprétation combinatoire de : apparemment, toutes les propriétés métathéorétiques ne se répercutent pas.$\lambda$

De plus, et peut-être plus important encore, bien qu'il existe des théories extensionnelles de et CL, elles sont à l'origine et communément maintenues intensionnelles. L'intensionnalité est une belle propriété parce que le calcul des modèles et CL en tant que processus, et de ce point de vue deux programmes différents (en particulier, des termes qui ont une forme normale différente) qui produisent toujours les mêmes résultats (avec des entrées égales) ne doivent pas être assimilés. respecte ce principe dans , et si nous voulons rendre l' extension , nous pourrions simplement ajouter par exemple . Mais l'introduction de$\lambda$$\lambda$$\xi$$\lambda$$\lambda$$\eta$$\xi$en CL ne le rendrait plus complètement intensionnel (en fait, seulement partiellement). Et c'est la raison de la «notoriété» de , comme le dit l'article.$\xi$

MODIFIER Cette réponse est incorrecte, comme l'a correctement signalé l'autre répondeur. J'ai utilisé la traduction en logique combinatoire d'Asperti & Longo, qui est subtilement différente de celle de Selinger.

En fait, cela illustre un point crucial: «l'interprétation combinatoire» du calcul lambda n'est pas une chose unique! Différents auteurs le font légèrement différemment.

Je laisse ma réponse ici pour la postérité, mais l'autre réponse est meilleure.

---

L'équivalence dans ce contexte est définie par les tableaux 1 et 2 de l'article de Selinger. Cependant, une axiomatisation légèrement différente peut rendre les choses un peu plus claires.

Ce que cela signifie vraiment, c'est que deux termes sont convertibles dans la théorie . On peut définir la "convertibilité" par les deux axiomes suivants:$\lambda$

• $\beta$ . , si libre pour dans$(\lambda x. M) N = [N/x]M$$x$$N$$M$
• $\eta$ . , si n'est pas libre dans$\lambda y. M y = M$$y$$M$

plus, bien sûr, les axiomes et les règles d'inférence habituels nécessaires pour faire une congruence. De cela, il devrait être évident que tout contre-exemple va s'appuyer sur la condition de variable libre sur la règle est brisée.$=$$\eta$

Je pense que c'est probablement le plus simple:

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

Vous pouvez vérifier par vous-même que , mais leurs interprétations combinatoires respectives ne sont pas égales selon les règles du tableau 2.$\lambda y. M = \lambda y. N$