É possível decidir a equivalência

Eu sei que é impossível decidir equivalência para o cálculo lambda sem tipo. Citando Barendregt, HP O cálculo Lambda: sua sintaxe e semântica. Holanda do Norte, Amsterdã (1984). :$\beta$

Se A e B são disjuntos, conjuntos não vazios de termos lambda que são fechados em igualdade, então A e B são recursivamente inseparáveis. Daqui resulta que, se A é um conjunto não trivial de termos lambda fechado em igualdade, então A não é recursivo. Portanto, não podemos decidir o problema "M = x?" para qualquer M. em particular. Da mesma forma, o Lambda não possui modelos recursivos.

Se temos um sistema de normalização, como o Sistema F, podemos decidir equivalência "externa", reduzindo os dois termos fornecidos e comparando se suas formas normais são iguais ou não. No entanto, podemos fazê-lo "de dentro"? Existe um combinador System-F tal que, para dois combinadores e , tenhamos se e tiverem a mesma forma normal e ? Ou isso pode ser feito pelo menos para alguns ? Para construir um combinador forma que seja verdadeiro seE M N E M N = verdadeiro M N E M N = falso M E M E M N N ≡ β$\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$? Se não, por que?

Não, não é possível. Considere os dois habitantes a seguir do tipo .$(A \to B) \to (A \to B)$

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

Essas são formas normais distintas , mas não podem ser distinguidas por um termo lambda, uma vez que N é uma expansão η de M , e a expansão η preserva a equivalência observacional em um cálculo lambda de tipo puro.$\beta$$N$$\eta$$M$$\eta$

Cody perguntou o que acontece se modificarmos também pela equivalência . A resposta ainda é negativa, devido à parametridade. Considere os dois termos a seguir no tipo ( ∀ α $\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}$$

Eles são distintos na forma normal, η- longa, mas são observacionalmente equivalentes. De fato, todas as funções deste tipo são equivalentes, desde ∀ α $\beta$$\eta$ é a codificação do tipo de unidade e, portanto, todas as funções do tipo ( ∀ α $\forall \alpha.\;\alpha \to \alpha$ deve ser extensionalmente equivalente.$(\forall \alpha.\;\alpha \to \alpha) \to (\forall \alpha.\;\alpha \to \alpha)$

Outra resposta possível para um perfeitamente correta de Neel: Suponha que há é um combinator , bem digitado no sistema de F tal que a condição acima detém. O tipo de E é:$E$$E$

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

Acontece que existe um teorema de graça que expressa que esse termo é necessariamente constante :

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

$E$