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

[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].

Типизируемость в [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(tt'\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]