Algoritmo para determinar a igualdade de funções no cálculo lambda simplesmente digitado?

Sabemos que a igualdade beta de termos lambda simplesmente digitados é decidível. Dado M, N: σ → τ, é decidível se para todos os X: σ, MX $≃_β$ NX?

Como eu disse no meu comentário, a resposta em geral é não.

O ponto importante a entender (digo isso para Viclib, que parece estar aprendendo sobre essas coisas) é que ter uma linguagem de programação / conjunto de máquinas em que todos os programas / computações terminam de forma alguma implica na igualdade de funções (ou seja, se dois programas / máquinas calculam a mesma função) é decidível. Um exemplo fácil: pegue o conjunto de máquinas de Turing com clock polinomial. Por definição, todas essas máquinas terminam em todas as entradas. Agora, dada qualquer máquina de Turing qualquer que seja , existe uma máquina de Turing que, dada na entrada da string , simulaetapas da computação de em uma entrada fixa (digamos, a sequência vazia) e aceita se termina no máximoM 0 x | x | M M | x | N M 0 N M 0 N $M$$M_0$$x$$|x|$$M$$M$$|x|$etapas ou rejeita o contrário. Se é uma máquina de Turing que sempre rejeita imediatamente, e são ambos (obviamente) com clock polinomialmente, e, no entanto, se pudéssemos decidir se e calculam a mesma função (ou, nesse caso, decidem o mesmo idioma), poderíamos decidir se (que, lembre-se, é uma máquina de Turing arbitrária) termina na string vazia.$N$$M_0$$N$$M_0$$N$$M$

No caso do -calculus simplesmente digitado (STLC), um argumento semelhante funciona, exceto que medir o poder expressivo do STLC não é tão trivial quanto no caso acima. Quando escrevi meu comentário, tinha em mente alguns artigos de Hillebrand, Kanellakis e Mairson, do início dos anos 90, que mostram que, usando tipos mais complexos que o tipo usual de número inteiro da Igreja, pode-se codificar no STLC suficientemente complexo cálculos para o argumento acima funcionar. Na verdade, vejo agora que o material necessário já está na prova simplificada de Mairson do teorema de Statman:$\lambda$

Harry G. Mairson, Uma simples prova de um teorema de Statman. Teórico Computer Science, 103 (2): 387-394, 1992. (Disponível online aqui ).

Nesse papel, Mairson mostra que, dado qualquer máquina de Turing , existe um tipo simples e um -termo que codifica a função de transição . (Isso não é óbvio a priori, se alguém tiver em mente o poder expressivo extremamente pobre do STLC sobre os inteiros da Igreja. De fato, a codificação de Mairson não é imediata). A partir disso, não é difícil construir um termoσ λ δ M : σ → σ $M$$\sigma$$\lambda$$\delta_M:\sigma\rightarrow\sigma$$M$

$t_M:\mathtt{nat}[\sigma]\rightarrow\mathtt{bool}$

(onde é a instanciação em do tipo de número inteiro da Igreja) de forma que reduza para se terminar em etapas no máximo quando alimentou a string vazia ou reduz para caso contrário. Como acima, se pudéssemos decidir que a função representada por é a função constante , teríamos decidido o término de na string vazia.σ t $\mathtt{nat}[\sigma]$$\sigma$1 _ Mn 0 _ t M 0 _$t_M\,\underline{n}$$\underline{1}$$M$$n$$\underline{0}$$t_M$$\underline{0}$$M$