113
правок
Изменения
→Неразрешимость задачи вывода типов в \lambda\Pi-исчислении: Всё кроме доказательства теоремы
{{Утверждение|statement=Если <tex>g</tex> это такой терм, что терм <tex>(g a \ldots a)</tex> (<tex>a</tex> повторяется <tex>n</tex> раз) типизируемый, и он является объектом в неком <tex>\Gamma\Delta</tex>, то тогда терм <tex>g</tex> типизируется в контексте <tex>\Gamma\Delta</tex>, и его тип эквивалентен терму <tex>\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>.
|proof=Индукция по <tex>n</tex>.}}
{{Утверждение|statement=Пусть <tex>t,u_1,\ldots,u_n,v</tex> {{---}} такие нормальные термы, что <tex>(t u_1\ldots u_n)</tex> {{---}} типизируемый терм, и его нормальная форма это <tex>v</tex>. Тогда первый символ <tex>t</tex> это либо первый символ <tex>v</tex>, либо первая переменная <tex>t</tex>.
|proof=Пусть <tex>x</tex> {{---}} первый символ <tex>t</tex>. Если <tex>x</tex> не является первой переменной <tex>t</tex>, то первый символ нормальной формы <tex>(t u_1 \ldots u_n)</tex> это тоже <tex>x</tex>, значит, <tex>x</tex> это первый символ <tex>v</tex>.}}
{{Утверждение|statement=Пусть <tex>t</tex> {{---}} такой нормальный терм типа <tex>(T \rightarrow T) \rightarrow \ldots \rightarrow (T \rightarrow T) \rightarrow T</tex> в контексте <tex>\Gamma</tex>, что нормальная форма <tex>(t \lambda y : T.y \ldots \lambda y : T.y)</tex> равна <tex>c</tex>. Тогда терм <tex>t</tex> является термом вида
<tex>t=\lambda x_1 : T \rightarrow T \ldots \lambda x_n : T \rightarrow T . (x_{i_1} (\ldots (x_{i_p} c)\ldots))</tex> для некой последовательности <tex>i_1,\ldots,i_p</tex>.
|proof=Индукция по числу переменных в <tex>t</tex>.}}
{{Теорема|statement=Задача проверки типизируемости чистого терма в заданном контексте неразрешима.
|proof=всего полторы страницы, скоро будет}}
