Est-il possible de décider de l' équivalence

Je sais qu'il est impossible de décider de l' équivalence pour le calcul lambda non typé. Citant Barendregt, HP Le calcul lambda: sa syntaxe et sa sémantique. Hollande du Nord, Amsterdam (1984). :$\beta$

Si A et B sont des ensembles de termes lambda disjoints et non vides qui sont fermés sous l'égalité, alors A et B sont récursivement inséparables. Il s'ensuit que si A est un ensemble non trivial de termes lambda fermés sous égalité, alors A n'est pas récursif. Donc, nous ne pouvons pas décider du problème "M = x?" pour tout M. particulier, il s'ensuit que Lambda n'a pas de modèles récursifs.

Si nous avons un système de normalisation, tel que le système F, alors nous pouvons décider de l' équivalence "de l'extérieur" en réduisant les deux termes donnés et en comparant si leurs formes normales sont identiques ou non. Cependant, pouvons-nous le faire "de l'intérieur"? Existe-t-il un combinateur System-F tel que pour deux combinateurs et nous ayons si et ont la même forme normale, et sinon? Ou cela peut-il être fait au moins pour certains ? Construire un combinateur tel que soit vrai si$\beta$$E$$M$$N$$E M N = \mbox{true}$$M$$N$$E M N = \mbox{false}$$M$$E_M$$E_M N$$N\equiv_\beta M$? Sinon, pourquoi?

Non, ce n'est pas possible. Considérons les deux habitants suivants du type .$(A \to B) \to (A \to B)$

$$\begin{array}{l} M = \lambda f.\;f \\ N = \lambda f.\;\lambda a.\; f\;a \end{array}$$

Ce sont des formes normales distinctes , mais ne peuvent pas être distinguées par un terme lambda, car N est une expansion η de M , et l' expansion η préserve l'équivalence observationnelle dans un calcul lambda typé pur.$\beta$$N$$\eta$$M$$\eta$

Cody a demandé ce qui se passe si nous modifions également par -équivalence. La réponse est toujours négative, en raison de la paramétrie. Considérez les deux termes suivants au type ( ∀ α $\eta$ :$(\forall \alpha.\;\alpha \to \alpha) \to (\forall \alpha.\;\alpha \to \alpha)$

$$\begin{array}{lcl} M & = & \lambda f:(\forall \alpha.\;\alpha \to \alpha).\;\Lambda \alpha.\lambda x:\alpha.\;f \;[\forall \alpha.\;\alpha \to \alpha]\;(\Lambda \beta.\lambda y:\beta.\;y)\;[\alpha]\;x\\ N & = & \lambda f:(\forall \alpha.\;\alpha \to \alpha).\;\Lambda \alpha.\lambda x:\alpha.\;f\;[\alpha]\;x \end{array}$$

Ils sont distincts de forme normale, η- longue, mais sont équivalents sur le plan de l'observation. En fait, toutes les fonctions de ce type sont équivalentes, puisque ∀ α $\beta$$\eta$ est le codage du type d'unité, et donc toutes les fonctions du type ( ∀ α $\forall \alpha.\;\alpha \to \alpha$ doit être extensionnellement équivalent.$(\forall \alpha.\;\alpha \to \alpha) \to (\forall \alpha.\;\alpha \to \alpha)$

Une autre réponse possible à un parfaitement correct de Neel: Supposons qu'il y est un combinateur système, bien typé dans F tel que la condition ci - dessus tient. Le type de E est:$E$$E$

$$E : \forall \alpha.\alpha\rightarrow \alpha\rightarrow {\bf bool}$$

Il s'avère qu'il existe un théorème gratuit qui exprime qu'un tel terme est nécessairement constant :

$$\forall T,\ t,u,t',u':T,\ E\ T\ t\ u = E\ T\ t'\ u'$$

En particulier, est la fonction constamment vraie ou la fonction constamment fausse , et ne peut éventuellement pas être un "décideur d'égalité".$E$