113
правок
Изменения
→\lambda\Pi-исчисление
\frac{\Gamma \in \mathrm{WF}}{\Gamma \vdash \mathrm{Type} : \mathrm{Kind}} \text{,} \vspace{3mm} \\
\frac{\Gamma \in \mathrm{WF} \qquad x : T \in \Gamma}{\Gamma \vdash x : T} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash T : \mathrm{Type} \qquad \Gamma\left[x : T\right] \vdash T' : xs}{\Gamma \vdash \Pi x : T . T' : s} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash \Pi x : T . T' : s \qquad \Gamma\left[x : T\right] \vdash t : T'}{\Gamma \vdash \lambda x : T . t : \Pi x : T . T'} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash t : \Pi x : T . T' \qquad \Gamma \vdash t' : T}{\Gamma \vdash \left(t\ t'\right) : T'\left[x \leftarrow t'\right]} \text{,} \vspace{3mm} \\
{{Утверждение|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>.}}
