Prosty dowód, że rozstrzygalność typowalności w systemie F ( ) implikuje rozstrzygalność sprawdzania typu?

Załóżmy, że nie znamy wyniku Joe B. Wellsa z 1994 roku, że zarówno typowość, jak i sprawdzanie typów są nierozstrzygalne w Systemie F (AKA ). W rachunku Lambda z typami Barendregta (1992) znalazłem dowód z powodu Maleckiego 1989, że sprawdzanie typów implikuje typowość. To dlatego, że$\lambda 2$

istnieje taki, że$\sigma$$M:\sigma$

jest równa

$(\lambda xy.y)M : (\alpha\rightarrow\alpha)$

(Dzieje się tak, ponieważ jeśli w Systemie F można wpisać dany termin, wówczas wszystkie jego podtermale są).

Czy istnieje prosty dowód na odwrót? Czy to dowód, że typowanie oznacza sprawdzanie typu w Systemie F?

O ile wiem, pokazanie, że ten kierunek jest trudną częścią dowodu Wellsa! Przynajmniej tak wyjaśnił mi kilka lat temu Paweł (Urzyczyn).

Najwyraźniej nie jest trudno wykazać, że sprawdzanie typu jest nierozstrzygalne; trudna część pokazuje, że oznacza to nierozstrzygalność rekonstrukcji typu! Rzeczywiście istnieją pewne przypadki, w których pierwszy jest nierozstrzygalny, a drugi rozstrzygalny: patrz np. Dowek 1993.