Supongamos que no conocemos el resultado de Joe B. Wells de 1994 de que tanto la tipificación como la verificación de tipo son indecidibles en el Sistema F (AKA ). En los cálculos Lambda con tipos de Barendregt (1992) encontré una prueba debido a Malecki 1989 de que la verificación de tipos implica tipificación. Esto es porque
existe tal que M : σ
es equivalente a
(Esto se debe a que si un término se puede escribir en el Sistema F, entonces todos sus subterms lo son).
¿Hay una prueba simple al revés? Es decir, ¿ una prueba de que la tipificación implica la verificación de tipos en el Sistema F?
fuente