Неразрешимость задачи вывода типов в языке с зависимыми типами — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Неразрешимость задачи вывода типов в \lambda\Pi-исчислении)
(Добавил пробелов в применения)
Строка 2: Строка 2:
 
{{Определение|definition=Множество '''термов''' рекурсивно определяется следующей грамматикой:
 
{{Определение|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>\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>\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>-эквивалентны.
 
Пусть есть термы <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>-эквивалентны.
Строка 18: Строка 18:
 
\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 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 \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 : \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{;}
 
\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>
 
</tex>
Строка 31: Строка 31:
 
{{Определение|definition=Нормальный терм <tex>t</tex>, типизируемый в контекте <tex>\Gamma</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>\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> это переменная или сорт, либо вид
 
где <tex>x</tex> это переменная или сорт, либо вид
Строка 42: Строка 42:
 
{{Определение|definition=Терм <tex>t</tex> типа <tex>T</tex> в контексте <tex>G</tex> называется '''объектом''' в <tex>\Gamma</tex>, если <tex>\Gamma \vdash T : \mathrm{Type}</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>.}}
+
{{Утверждение|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 ::= 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>) {{---}} это рекурсивно определённый чистый терм:
 
{{Определение|definition=Пусть <tex>t</tex> {{---}} объект в контексте <tex>\Gamma</tex>. '''Содержимое''' <tex>t</tex> (<tex>\left|t\right|</tex>) {{---}} это рекурсивно определённый чистый терм:
  
 
* <tex>\left|x\right| = x</tex>;
 
* <tex>\left|x\right| = x</tex>;
* <tex>\left|\left(tt'\right)\right| = \left(\left|t\right|\left|t'\right|\right) </tex>;
+
* <tex>\left|\left(t\ 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>\left|\lambda x : U . t\right| = \lambda x . \left|t\right|</tex>.}}
  
Строка 61: Строка 61:
  
 
Рассмотрим контекст
 
Рассмотрим контекст
<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>.
+
<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> следующим образом:
 
{{Определение|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{\varepsilon} = \lambda y : T . y</tex>;
* <tex>\hat{A\varphi} = \lambda y : T.\left(a \left(\hat{\varphi} y\right)\right)</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>\hat{B\ \varphi} = \lambda y : T.\left(b\ \left(\hat{\varphi}\ y\right)\right)</tex>;
 
* <tex>\tilde{\varphi}=\left|\hat{\varphi}\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>\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>.
 
{{Утверждение|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>.}}
 
|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>.
+
{{Утверждение|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>.}}
+
|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> является термом вида
+
{{Утверждение|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>.
+
<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>.}}
 
|proof=Индукция по числу переменных в <tex>t</tex>.}}
  
Строка 86: Строка 86:
 
<tex>
 
<tex>
 
\begin{aligned}
 
\begin{aligned}
t = \lambda f . \lambda g . \lambda h . (f
+
t = \lambda f . \lambda g . \lambda h . (f\
&(g a \ldots a)\\
+
&(g\ a \ldots a)\\
&(h (g \tilde{\varphi_1} \ldots \tilde{\varphi_n}))\\
+
&(h\ (g\ \tilde{\varphi_1} \ldots \tilde{\varphi_n}))\\
&(h (g \tilde{\psi_1} \ldots \tilde{\psi_n}))\\
+
&(h\ (g\ \tilde{\psi_1} \ldots \tilde{\psi_n}))\\
&(F c (g \lambda y.y \ldots \lambda y.y))\\
+
&(F\ c\ (g\ \lambda y.y \ldots \lambda y.y))\\
&(F d (g \lambda y.d \ldots \lambda y.d)))\text{.}
+
&(F\ d\ (g\ \lambda y.d \ldots \lambda y.d)))\text{.}
 
\end{aligned}
 
\end{aligned}
 
</tex>
 
</tex>
  
Предположим, что этот терм типизируем, и обозначим тип <tex>g</tex> как <tex>\alpha</tex>. Терм <tex>(g a \ldots a)</tex> типизируется и является объектом в <tex>\Gamma\Delta</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>\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>\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>, тогда из типизируемости терма...
+
Тогда все переменные <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>, тогда из типизируемости терма...
 
}}
 
}}

Версия 20:58, 17 января 2017

[math]\lambda\Pi[/math]-исчисление

Определение:
Множество термов рекурсивно определяется следующей грамматикой:

[math]\displaystyle T ::= \mathrm{Type} \mid \mathrm{Kind} \mid x \mid \left(T\ T\right) \mid \lambda x : T . T \mid \Pi x : T . T[/math].

Термы [math]\mathrm{Type}[/math] и [math]\mathrm{Kind}[/math] называются сортами, [math]x[/math]переменными, [math](t\ t')[/math]применениями, [math]\lambda x : t . t'[/math]абстракциями, [math]\Pi x : t . t'[/math]произведениями. Обозначение [math]t \rightarrow t'[/math] используется вместо [math]\Pi x : t . t'[/math], если [math]x[/math] не входит свободно в [math]t'[/math].


Пусть есть термы [math]t[/math] и [math]t'[/math] и переменная [math]x[/math]. Записью [math]t\left[x \leftarrow t'\right][/math] обозначается терм, полученный заменой [math]t'[/math] на [math]t[/math] в [math]x[/math]. Запись [math]t =_\beta t'[/math] означает, что термы [math]t[/math] и [math]t'[/math] [math]\beta[/math]-эквивалентны.

Определение:
Контекст это список пар [math]x : T[/math], где [math]x[/math] — переменная, [math]T[/math] — терм.


Определение:
Правила вывода для нашего исчисления:

[math] \displaystyle \frac{}{\left[ \right] \in \mathrm{WF}} \text{,} \vspace{3mm} \\ \frac{\Gamma \vdash T : s}{\Gamma\left[x : T\right] \in \mathrm{WF}} \text{,} \vspace{3mm} \\ \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' : 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{;} [/math]

где [math]s ::= \mathrm{Type} \mid \mathrm{Kind}[/math], а [math]\mathrm{WF}[/math] — множество корректных грамматик.

Терм [math]t[/math] типизируется в контексте [math]\Gamma[/math], если существует такой терм [math]T[/math], что [math]\Gamma \vdash t : T[/math].


Отношение редуцируемости на типизируемых термах сильно нормализуемо и обладает ромбовидным свойством. Каждый типизируемый терм имеет единственную нормальную форму, два терма эквивалентны, если у них одинаковая нормальная форма.

Типизируемый в контексте [math]\Gamma[/math] терм [math]t[/math] имеет единственный тип с точностью до эквивалентности.

Определение:
Нормальный терм [math]t[/math], типизируемый в контекте [math]\Gamma[/math], имеет либо вид

[math]\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \left(x\ c_1\ \ldots\ c_n\right)[/math],

где [math]x[/math] это переменная или сорт, либо вид

[math]\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \Pi x : P . Q\text{.}[/math]

Согласимся первым символом [math]t[/math] называть [math]x[/math] в первом случае, и [math]\Pi[/math] во втором. Первыми переменными [math]t[/math] будем называть переменные [math]x_1, \ldots, x_n[/math].


Задача вывода типов в [math]\lambda\Pi[/math]-исчислении

Определение:
Терм [math]t[/math] типа [math]T[/math] в контексте [math]G[/math] называется объектом в [math]\Gamma[/math], если [math]\Gamma \vdash T : \mathrm{Type}[/math]


Утверждение:
Если терм [math]t[/math] является объёктом в контексте [math]\Gamma[/math], то он является либо переменной, либо применением, либо абстракцией. Если он является применением [math]t=(u\ v)[/math], тогда оба терма [math]u[/math] и [math]v[/math] являются объектами в [math]\Gamma[/math], если он является абстракцией [math]t=\lambda x : U . u[/math], то тогда терм [math]u[/math] является объектом в контексте [math]\Gamma\left[x : U\right][/math].


Определение:
Множество чистых термов определяется грамматикой [math]T ::= x \mid \left(T\ T\right) \mid \lambda x . T[/math].


Определение:
Пусть [math]t[/math] — объект в контексте [math]\Gamma[/math]. Содержимое [math]t[/math] ([math]\left|t\right|[/math]) — это рекурсивно определённый чистый терм:
  • [math]\left|x\right| = x[/math];
  • [math]\left|\left(t\ t'\right)\right| = \left(\left|t\right|\left|t'\right|\right) [/math];
  • [math]\left|\lambda x : U . t\right| = \lambda x . \left|t\right|[/math].


Определение:
Чистый терм [math]t[/math] называется типизируемым в контексте [math]\Gamma[/math], если существует терм [math]t'[/math], типизируемый в неком [math]\Gamma\Delta[/math], являющимся расширением [math]\Gamma[/math], что [math]t'[/math] является объектом в [math]\Gamma\Delta[/math] и [math]t=\left|t'\right|[/math].


Типизация чистого терма в контексте [math]\Gamma[/math] это присвоение типов связанным переменным и некоторым свободным переменным, типов которых нет в [math]\Gamma[/math]. Если же контекст [math]\Gamma[/math] пустой, то типизация терма в нём будет являться присваиванием типов и связанным и свободным переменным.

Утверждение:
Задача вывода типов в пустом контексте разрешима в [math]\lambda\Pi[/math]-исчислении.
[math]\triangleright[/math]
Типизируемые в пустом контексте чистые термы [math]\lambda\Pi[/math] исчисления совпадают с типизируемыми выражениями просто типизированного [math]\lambda[/math]-исчисления, а задача вывода типов в просто типизированном [math]\lambda[/math]-исчислении разрешима.
[math]\triangleleft[/math]

Неразрешимость задачи вывода типов в [math]\lambda\Pi[/math]-исчислении

Рассмотрим контекст [math]\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][/math].


Определение:
Пусть [math]\varphi[/math] — слово двухсимвольного алфавита [math]\left\{A, B\right\}[/math]. Определим [math]\hat{\varphi}[/math] и [math]\tilde{\varphi}[/math] следующим образом:
  • [math]\hat{\varepsilon} = \lambda y : T . y[/math];
  • [math]\hat{A\ \varphi} = \lambda y : T.\left(a\ \left(\hat{\varphi}\ y\right)\right)[/math];
  • [math]\hat{B\ \varphi} = \lambda y : T.\left(b\ \left(\hat{\varphi}\ y\right)\right)[/math];
  • [math]\tilde{\varphi}=\left|\hat{\varphi}\right|[/math].


Утверждение:
Рассмотрим проблему соответствий Поста для списков слов над двухсимвольным алфавитом [math]\left(\varphi_1, \ldots, \varphi_n\right)[/math] и [math]\left(\psi_1, \ldots, \psi_n\right)[/math]. Непустая последовательность [math]\left(i_1,\ldots,i_p\right)[/math] является её решением тогда и только тогда, когда [math](\hat{\varphi_{i_1}}\ (\ldots (\hat{\varphi_{i_p}}\ c)\ldots)) =_\beta (\hat{\psi_{i_1}}\ (\ldots (\hat{\psi_{i_p}}\ c)\ldots))[/math].
Утверждение:
Если [math]g[/math] это такой терм, что терм [math](g a \ldots a)[/math] ([math]a[/math] повторяется [math]n[/math] раз) типизируемый, и он является объектом в неком [math]\Gamma\Delta[/math], то тогда терм [math]g[/math] типизируется в контексте [math]\Gamma\Delta[/math], и его тип эквивалентен терму [math]\Pi x_1 : T \rightarrow T \ldots \Pi x_n : T \rightarrow T . (\beta x_1 \ldots x_n)[/math] для какого-то терма [math]\beta[/math] типа [math](T \rightarrow T) \rightarrow \ldots \rightarrow (T \rightarrow T) \rightarrow \mathrm{Type}[/math] в контексте [math]\Gamma\Delta[/math].
[math]\triangleright[/math]
Индукция по [math]n[/math].
[math]\triangleleft[/math]
Утверждение:
Пусть [math]t,u_1,\ldots,u_n,v[/math] — такие нормальные термы, что [math](t\ u_1\ldots u_n)[/math] — типизируемый терм, и его нормальная форма это [math]v[/math]. Тогда первый символ [math]t[/math] это либо первый символ [math]v[/math], либо первая переменная [math]t[/math].
[math]\triangleright[/math]
Пусть [math]x[/math] — первый символ [math]t[/math]. Если [math]x[/math] не является первой переменной [math]t[/math], то первый символ нормальной формы [math](t\ u_1 \ldots u_n)[/math] это тоже [math]x[/math], значит, [math]x[/math] это первый символ [math]v[/math].
[math]\triangleleft[/math]
Утверждение:
Пусть [math]t[/math] — такой нормальный терм типа [math](T \rightarrow T) \rightarrow \ldots \rightarrow (T \rightarrow T) \rightarrow T[/math] в контексте [math]\Gamma[/math], что нормальная форма [math](t\ \lambda y : T.y \ldots \lambda y : T.y)[/math] равна [math]c[/math]. Тогда терм [math]t[/math] является термом вида [math]t=\lambda x_1 : T \rightarrow T \ldots \lambda x_n : T \rightarrow T . (x_{i_1}\ (\ldots (x_{i_p}\ c)\ldots))[/math] для некой последовательности [math]i_1,\ldots,i_p[/math].
[math]\triangleright[/math]
Индукция по числу переменных в [math]t[/math].
[math]\triangleleft[/math]
Теорема:
Задача проверки типизируемости чистого терма в заданном контексте неразрешима.
Доказательство:
[math]\triangleright[/math]

Рассмотрим проблему соответствий Поста для списков слов над двухсимвольным алфавитом [math]\left(\varphi_1, \ldots, \varphi_n\right)[/math] и [math]\left(\psi_1, \ldots, \psi_n\right)[/math]. Построим такой чистый терм [math]t[/math], что [math]t[/math] типизируем в [math]\Gamma[/math] тогда и только тогда, когда проблема соответствий поста имеет решение.

[math] \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} [/math]

Предположим, что этот терм типизируем, и обозначим тип [math]g[/math] как [math]\alpha[/math]. Терм [math](g\ a \ldots a)[/math] типизируется и является объектом в [math]\Gamma\Delta[/math], значит,

[math]\alpha =_\beta \Pi x_1 : T \rightarrow T \ldots \Pi x_n : T \rightarrow T . (\beta\ x_1 \ldots x_n)[/math],

где [math]\beta[/math] это терм типа [math](T \rightarrow T) \rightarrow \ldots \rightarrow (T \rightarrow T) \rightarrow \mathrm{Type}[/math] в [math]\Gamma\Delta[/math].

Тогда все переменные [math]y[/math], связанные в термах [math]\hat{\varphi_i}[/math], [math]\tilde{\psi_i}[/math], [math]\lambda y.y[/math] и [math]\lambda y.d[/math], имеют тип [math]T[/math]. Терм [math](g \ \hat{\varphi_1} \ \ldots\ \hat{\varphi_n})[/math] имеет тип [math](\beta\ \hat{\varphi_1} \ \ldots\ \hat{\varphi_n})[/math], тогда из типизируемости терма...
[math]\triangleleft[/math]