Предположим, что нам не известен результат Джо Б. Уэллса от 1994 года о том, что в System F (AKA неразрешимы и типизация, и проверка типов) ). В лямбда-исчислении Барендрегта с типами (1992) я нашел доказательство Малецки 1989 года, что проверка типов подразумевает типизацию. Это потому что
существует такой, что
эквивалентно
(Это потому, что если термин может быть типизирован в Системе F, то все его подтермы являются.)
Есть ли простое доказательство наоборот? То есть доказательство того, что типизация подразумевает проверку типов в Системе F?