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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Новая страница: «=Неразрешимость задачи вывода типов в языке с зависимыми типами=»)
 
(Определение исчисления)
Строка 1: Строка 1:
=Неразрешимость задачи вывода типов в языке с зависимыми типами=
+
=<math dpi = "180">\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] \text{ well-formed}} \text{,} \vspace{3mm} \\
 +
\frac{\Gamma \vdash T : s}{\Gamma\left[x : T\right] \text{ well-formed}} \text{,} \vspace{3mm} \\
 +
\frac{\Gamma \text{ well-formed}}{\Gamma \vdash \mathrm{Type} : \mathrm{Kind}} \text{,} \vspace{3mm} \\
 +
\frac{\Gamma \text{ well-formed} \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>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>.

Версия 18:35, 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] \text{ well-formed}} \text{,} \vspace{3mm} \\ \frac{\Gamma \vdash T : s}{\Gamma\left[x : T\right] \text{ well-formed}} \text{,} \vspace{3mm} \\ \frac{\Gamma \text{ well-formed}}{\Gamma \vdash \mathrm{Type} : \mathrm{Kind}} \text{,} \vspace{3mm} \\ \frac{\Gamma \text{ well-formed} \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]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].