Простое доказательство того, что разрешимость типизируемости в системе F (

9

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

существует σ такой, что M:σ

эквивалентно

(λxy.y)M:(αα)

(Это потому, что если термин может быть типизирован в Системе F, то все его подтермы являются.)

Есть ли простое доказательство наоборот? То есть доказательство того, что типизация подразумевает проверку типов в Системе F?

Петр Пудлак
источник

Ответы:

5

Насколько я знаю, показ того, что это направление - трудная часть доказательства Уэллса! По крайней мере, это то, что Павел (Уржичин) объяснил мне несколько лет назад.

Очевидно, нетрудно показать, что проверка типов неразрешима; трудная часть показывает, что это подразумевает неразрешимость восстановления типа! Действительно, есть некоторые случаи, когда первое неразрешимо, а второе разрешимо: см., Например, Dowek 1993.

Коди
источник