113
правок
Изменения
→Неразрешимость задачи вывода типов в \lambda\Pi-исчислении
=Неразрешимость задачи вывода типов в <tex dpi="180">\lambda\Pi</tex>-исчислении=
Рассмотрим контекст
<tex>\Gamma=\left[T : \mathrm{Type}; a : T \rightarrow T; b : T \rightarrow T; c : T; d : T; P : T \rightarrow \mathrm{Type}; F : \Pi x : T.\left(\left(P x\right) \rightarrow T\right)\right]</tex>.
{{Определение|definition=Пусть <tex>\varphi</tex> {{---}} слово двухсимвольного алфавита <tex>\left\{A, B\right\}</tex>. Определим <tex>\hat{\varphi}</tex> и <tex>\tilde{\varphi}</tex> следующим образом:
* <tex>\hat{\varepsilon} = \lambda y : T . y</tex>;
* <tex>\hat{A\varphi} = \lambda y : T.\left(a \left(\hat{\varphi} y\right)\right)</tex>;
* <tex>\hat{B\varphi} = \lambda y : T.\left(b \left(\hat{\varphi} y\right)\right)</tex>;
* <tex>\tilde{\varphi}=\left|\hat{\varphi}\right|</tex>.}}
{{Утверждение|statement=Рассмотрим проблему соответствий Поста для списков слов над двухсимвольным алфавитом <tex>\left(\varphi_1, \ldots, \varphi_n\right)</tex> и <tex>\left(\psi_1, \ldots, \psi_n\right)</tex>. Непустая последовательность <tex>\left(i_1,\ldots,i_p\right)</tex> является её решением тогда и только тогда, когда <tex>(\hat{\varphi_{i_1}} (\ldots (\hat{\varphi_{i_p}} c)\ldots)) =_\beta (\hat{\psi_{i_1}} (\ldots (\hat{\psi_{i_p}} c)\ldots))</tex>.}}
{{Утверждение|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>.}}
