113
правок
Изменения
→Неразрешимость задачи вывода типов в \lambda\Pi-исчислении
{{Теорема|statement=Задача проверки типизируемости чистого терма в заданном контексте неразрешима.
|proof=всего полторы страницыРассмотрим проблему соответствий Поста для списков слов над двухсимвольным алфавитом <tex>\left(\varphi_1, скоро будет\ldots, \varphi_n\right)</tex> и <tex>\left(\psi_1, \ldots, \psi_n\right)</tex>. Построим такой чистый терм <tex>t</tex>, что <tex>t</tex> типизируем в <tex>\Gamma</tex> тогда и только тогда, когда проблема соответствий поста имеет решение. <tex>\begin{aligned}t = \lambda f . \lambda g . \lambda h . (f&(g a \ldots a)\\&(h (g \tilde{\varphi_1} \ldots \tilde{\varphi_n}))\\&(h (g \tilde{\psi_1} \ldots \tilde{\psi_n}))\\&(F c (g \lambda y.y \ldots \lambda y.y))\\&(F d (g \lambda y.d \ldots \lambda y.d)))\text{.}\end{aligned}</tex> Предположим, что этот терм типизируем, и обозначим тип <tex>g</tex> как <tex>\alpha</tex>. Терм <tex>(g a \ldots a)</tex> типизируется и является объектом в <tex>\Gamma\Delta</tex>, значит, <tex>\alpha =_\beta \Pi x_1 : T \rightarrow T \ldots \Pi x_n : T \rightarrow T . (\beta x_1 \ldots x_n)</tex>, где <tex>\beta</tex> это терм типа <tex>(T \rightarrow T) \rightarrow \ldots \rightarrow (T \rightarrow T) \rightarrow \mathrm{Type}</tex> в <tex>\Gamma\Delta</tex>. Тогда все переменные <tex>y</tex>, связанные в термах <tex>\hat{\varphi_i}</tex>, <tex>\tilde{\psi_i}</tex>, <tex>\lambda y.y</tex> и <tex>\lambda y.d</tex>, имеют тип <tex>T</tex>. Терм <tex>(g \ \hat{\varphi_1} \ \ldots\ \hat{\varphi_n})</tex> имеет тип <tex>(\beta \ \hat{\varphi_1} \ \ldots\ \hat{\varphi_n})</tex>, тогда из типизируемости терма...}}
