Изменения

Лямбда исчисление с зависимыми типами {{---}} расширение просто типизированного [[Лямбда-исчисление|лямбда-исчисления]], которое позволяет типам зависеть от значений. Например, в языке с таким исчислением функция может возвращать не просто пару чисел, а пару чисел, в которой первое число меньше второго, или если ваша функция принимает число <tex>n</tex> и возвращает массив длины <tex>n</tex>, то это можно будет выразить типом этой функции. Зависимые типы добавляют выразительности типовой системе, что приводит к лучшей проверке корректности программы на этапе компиляции. Однако, как будет показано далее, для этого придётся идти на определённые жертвы: почти всегда придётся явно указывать типы выражений, так как компилятор не сможет справиться с выводом типов для них. ==<tex dpi = "180150">\lambda\Pi</tex>-исчисление=={{Определение|definition=Множество '''термов''' (англ. ''term'') рекурсивно определяется следующей грамматикой:

* Термы <tex>\mathrm{Type}</tex> и <tex>\mathrm{Kind}</tex> называются '''сортами'''(англ. ''sorts''), * <tex>x</tex> {{---}} '''переменными'''(англ. ''variables''), * <tex>(t\ t')</tex> {{---}} '''применениями'''(англ. ''applications''), * <tex>\lambda x : t . t'</tex> {{---}} '''абстракциями'''(англ. ''abstractions''), * <tex>\Pi x : t . t'</tex> {{---}} '''произведениями'''(англ. ''products''). Обозначение <tex>t \rightarrow t'</tex> используется вместо <tex>\Pi x : t . t'</tex>, если <tex>x</tex> не входит свободно в <tex>t'</tex>.}}

{{Определение|definition='''Контекст''' (англ. ''context'') это список пар <tex>x : T</tex>, где <tex>x</tex> {{---}} переменная, <tex>T</tex> {{---}} терм.}}

\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} \\

где <tex>s ::= \mathrm{Type} \mid \mathrm{Kind}</tex>, а <tex>\mathrm{WF}</tex> {{---}} множество корректных грамматикконтекстов.

Терм <tex>t</tex> '''типизируется''' (англ. ''well-typed'') в контексте <tex>\Gamma</tex>, если существует такой терм <tex>T</tex>, что <tex>\Gamma \vdash t : T</tex>.}}

Согласимся '''первым символом''' (англ. ''head symbol'') <tex>t</tex> называть <tex>x</tex> в первом случае, и <tex>\Pi</tex> во втором. '''Первыми переменными''' (англ. ''top variables'') <tex>t</tex> будем называть переменные <tex>x_1, \ldots, x_n</tex>.}}

==Задача вывода типов в <tex dpi = "180150">\lambda\Pi</tex>-исчислении=={{Определение|definition=Терм <tex>t</tex> типа <tex>T</tex> в контексте <tex>G</tex> называется '''объектом''' (англ. ''object'') в <tex>\Gamma</tex>, если <tex>\Gamma \vdash T : \mathrm{Type}</tex>.}}

{{Определение|definition=Множество '''чистых термов''' (англ. ''pure terms'') определяется грамматикой <tex>T ::= x \mid \left(T\ T\right) \mid \lambda x . T</tex>.}}

{{Определение|definition=Пусть <tex>t</tex> {{---}} объект в контексте <tex>\Gamma</tex>. '''Содержимое''' (англ. ''content'') <tex>t</tex> (<tex>\left|t\right|</tex>) {{---}} это рекурсивно определённый чистый терм:

{{Определение|definition=Чистый терм <tex>t</tex> называется '''типизируемым''' (англ. ''typable'') в контексте <tex>\Gamma</tex>, если существует терм <tex>t'</tex>, типизируемый в неком <tex>\Gamma\Delta</tex>, являющимся расширением <tex>\Gamma</tex>, что <tex>t'</tex> является объектом в <tex>\Gamma\Delta</tex> и <tex>t=\left|t'\right|</tex>.}}

==Неразрешимость задачи вывода типов в <tex dpi="180150">\lambda\Pi</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>.

Тогда все переменные <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>(h\ (g \ \hat{\varphi_1} \ \ldots\ \hat{\varphi_n}))</tex> мы получаем, что тип переменной <tex>h</tex> имеет вид <tex>\Pi x : \gamma : \gamma'</tex>, и <tex>y =_\beta (\beta\ \hat{\varphi_1} \ \ldots\ \hat{\varphi_n})</tex>. Точно так же, из типизируемости терма <tex>(h\ (g \ \hat{\psi_1} \ \ldots\ \hat{\psi_n}))</tex> получаем, что <tex>y =_\beta (\beta\ \hat{\psi_1} \ \ldots\ \hat{\psi_n})</tex>, значит, <tex>(\beta\ \hat{\varphi_1} \ \ldots\ \hat{\varphi_n}) =_\beta (\beta\ \hat{\psi_1} \ \ldots\ \hat{\psi_n})</tex>. Из типизируемости терма <tex>(F\ c\ (g\ \lambda y : T.y\ldots \lambda y : T . y))</tex> получаем <tex>(\beta\ \lambda y:T.y \ldots \lambda y:T.y) =_\beta (P\ c)</tex>. Наконец, из типизируемости терма <tex>(F\ d\ (g\ \lambda y : T.d\ldots \lambda y : T . d))</tex> получаем <tex>(\beta\ \lambda y:T.d \ldots \lambda y:T.d) =_\beta (P\ d)</tex>. Поскольку терм <tex>\beta</tex> имеет тип <tex>(T \rightarrow T) \rightarrow \ldots \rightarrow (T \rightarrow T) \rightarrow \mathrm{Type}</tex>, первый символ нормальной формы терма <tex>\beta</tex> не может быть первой переменной <tex>\beta</tex>, значит, это переменная <tex>P</tex>, и мы получаем, что <tex>\beta =_\beta \lambda x_1 : T \rightarrow T \ldots \lambda x_n : T \rightarrow T.(P\ (\delta\ x_1 \ldots x_n))</tex>, где <tex>\delta</tex> {{---}} некий терм типа <tex>(T \rightarrow T) \rightarrow \ldots \rightarrow (T \rightarrow T) \rightarrow T</tex>. Получаем, что <tex>(\delta\ \hat{\varphi_1} \ldots \hat{\varphi_n}) =_\beta (\delta\ \hat{\psi_1} \ldots \hat{\psi_n})\text{,} \\(\delta\ \lambda y:T.y \ldots \lambda y:T.y) =_\beta c \text{,}\\(\delta\ \lambda y:T.d \ldots \lambda y:T.d) =_\beta d \text{.}</tex> Вторая эквивалентность показывает, что нормальная форма <tex>\delta</tex> имеет вид <tex>\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>p>0</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>, то есть последовательность <tex>i_1,\ldots,i_p</tex> является решением проблемы Поста. И наоборот, если предположить, что проблема Поста имеет решение <tex>i_1,\ldots,i_p</tex>, то можно задать типы переменным <tex>f</tex>, <tex>g</tex> и <tex>h</tex>: <tex>f : (P\ (a\ (\ldots(a\ c)\ldots))) \rightarrow T \rightarrow T \rightarrow T \rightarrow T \rightarrow T \text{,}\\g : \Pi x_1 : T \rightarrow T \ldots \Pi x_n : T \rightarrow T.(P\ (x_{i_1}\ (\ldots(x_{i_p}\ c)\ldots))) \text{,}\\h : (P\ (\hat{\varphi_{i_1}}\ (\ldots(\hat{\varphi_{i_p}}\ c)\ldots))) \rightarrow T \text{;}</tex> и тип <tex>T</tex> всем остальным переменным терма <tex>t</tex>, и получить такой типизируемый в <tex>\Gamma</tex> терм <tex>t'</tex>, который является объектом и <tex>t = \left|t'\right|</tex>.