113
правок
Изменения
Добавил пробелов в применения
{{Определение|definition=Множество '''термов''' рекурсивно определяется следующей грамматикой:
<tex>\displaystyle T ::= \mathrm{Type} \mid \mathrm{Kind} \mid x \mid \left(T \ T\right) \mid \lambda x : T . T \mid \Pi x : T . T</tex>.
Термы <tex>\mathrm{Type}</tex> и <tex>\mathrm{Kind}</tex> называются '''сортами''', <tex>x</tex> {{---}} '''переменными''', <tex>(t \ t')</tex> {{---}} '''применениями''', <tex>\lambda x : t . t'</tex> {{---}} '''абстракциями''', <tex>\Pi x : t . t'</tex> {{---}} '''произведениями'''. Обозначение <tex>t \rightarrow t'</tex> используется вместо <tex>\Pi x : t . t'</tex>, если <tex>x</tex> не входит свободно в <tex>t'</tex>.}}
Пусть есть термы <tex>t</tex> и <tex>t'</tex> и переменная <tex>x</tex>. Записью <tex>t\left[x \leftarrow t'\right]</tex> обозначается терм, полученный заменой <tex>t'</tex> на <tex>t</tex> в <tex>x</tex>. Запись <tex>t =_\beta t'</tex> означает, что термы <tex>t</tex> и <tex>t'</tex> <tex>\beta</tex>-эквивалентны.
\frac{\Gamma \vdash T : \mathrm{Type} \qquad \Gamma\left[x : T\right] \vdash T' : x}{\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} \\
\frac{\Gamma \vdash T : s \qquad \Gamma \vdash T' : s \qquad \Gamma \vdash t : T \qquad T =_\beta T'}{\Gamma \vdash t : T'} \text{;}
</tex>
{{Определение|definition=Нормальный терм <tex>t</tex>, типизируемый в контекте <tex>\Gamma</tex>, имеет либо вид
<tex>\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \left(x \ c_1 \ \ldots \ c_n\right)</tex>,
где <tex>x</tex> это переменная или сорт, либо вид
{{Определение|definition=Терм <tex>t</tex> типа <tex>T</tex> в контексте <tex>G</tex> называется '''объектом''' в <tex>\Gamma</tex>, если <tex>\Gamma \vdash T : \mathrm{Type}</tex>}}
{{Утверждение|statement=Если терм <tex>t</tex> является объёктом в контексте <tex>\Gamma</tex>, то он является либо переменной, либо применением, либо абстракцией. Если он является применением <tex>t=(u \ v)</tex>, тогда оба терма <tex>u</tex> и <tex>v</tex> являются объектами в <tex>\Gamma</tex>, если он является абстракцией <tex>t=\lambda x : U . u</tex>, то тогда терм <tex>u</tex> является объектом в контексте <tex>\Gamma\left[x : U\right]</tex>.}}
{{Определение|definition=Множество '''чистых термов''' определяется грамматикой <tex>T ::= x \mid \left(T \ T\right) \mid \lambda x . T</tex>.}}
{{Определение|definition=Пусть <tex>t</tex> {{---}} объект в контексте <tex>\Gamma</tex>. '''Содержимое''' <tex>t</tex> (<tex>\left|t\right|</tex>) {{---}} это рекурсивно определённый чистый терм:
* <tex>\left|x\right| = x</tex>;
* <tex>\left|\left(ttt\ t'\right)\right| = \left(\left|t\right|\left|t'\right|\right) </tex>;
* <tex>\left|\lambda x : U . t\right| = \lambda x . \left|t\right|</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>.}}
{{Утверждение|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>.}}
<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>, тогда из типизируемости терма...
}}
