Неразрешимость задачи вывода типов в языке с зависимыми типами — различия между версиями
(→Неразрешимость задачи вывода типов в \lambda\Pi-исчислении) |
м (rollbackEdits.php mass rollback) |
||
(не показаны 23 промежуточные версии 3 участников) | |||
Строка 1: | Строка 1: | ||
− | + | Лямбда исчисление с зависимыми типами {{---}} расширение просто типизированного [[Лямбда-исчисление|лямбда-исчисления]], которое позволяет типам зависеть от значений. Например, в языке с таким исчислением функция может возвращать не просто пару чисел, а пару чисел, в которой первое число меньше второго, или если ваша функция принимает число <tex>n</tex> и возвращает массив длины <tex>n</tex>, то это можно будет выразить типом этой функции. Зависимые типы добавляют выразительности типовой системе, что приводит к лучшей проверке корректности программы на этапе компиляции. Однако, как будет показано далее, для этого придётся идти на определённые жертвы: почти всегда придётся явно указывать типы выражений, так как компилятор не сможет справиться с выводом типов для них. | |
− | |||
− | <tex> | + | ==<tex dpi = "150">\lambda\Pi</tex>-исчисление== |
+ | {{Определение|definition=Множество '''термов''' (англ. ''term'') рекурсивно определяется следующей грамматикой: | ||
− | Термы <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>\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> называются '''сортами''' (англ. ''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>.}} | ||
Пусть есть термы <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>-эквивалентны. | ||
− | {{Определение|definition='''Контекст''' это список пар <tex>x : T</tex>, где <tex>x</tex> {{---}} переменная, <tex>T</tex> {{---}} терм.}} | + | {{Определение|definition='''Контекст''' (англ. ''context'') это список пар <tex>x : T</tex>, где <tex>x</tex> {{---}} переменная, <tex>T</tex> {{---}} терм.}} |
{{Определение|definition=Правила вывода для нашего исчисления: | {{Определение|definition=Правила вывода для нашего исчисления: | ||
Строка 16: | Строка 23: | ||
\frac{\Gamma \in \mathrm{WF}}{\Gamma \vdash \mathrm{Type} : \mathrm{Kind}} \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 \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' : | + | \frac{\Gamma \vdash T : \mathrm{Type} \qquad \Gamma\left[x : T\right] \vdash T' : s}{\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> | ||
− | где <tex>s ::= \mathrm{Type} \mid \mathrm{Kind}</tex>, а <tex>\mathrm{WF}</tex> {{---}} множество корректных | + | где <tex>s ::= \mathrm{Type} \mid \mathrm{Kind}</tex>, а <tex>\mathrm{WF}</tex> {{---}} множество корректных контекстов. |
− | Терм <tex>t</tex> '''типизируется''' в контексте <tex>\Gamma</tex>, если существует такой терм <tex>T</tex>, что <tex>\Gamma \vdash t : T</tex>.}} | + | Терм <tex>t</tex> '''типизируется''' (англ. ''well-typed'') в контексте <tex>\Gamma</tex>, если существует такой терм <tex>T</tex>, что <tex>\Gamma \vdash t : T</tex>.}} |
Отношение редуцируемости на типизируемых термах сильно нормализуемо и обладает ромбовидным свойством. Каждый типизируемый терм имеет единственную нормальную форму, два терма эквивалентны, если у них одинаковая нормальная форма. | Отношение редуцируемости на типизируемых термах сильно нормализуемо и обладает ромбовидным свойством. Каждый типизируемый терм имеет единственную нормальную форму, два терма эквивалентны, если у них одинаковая нормальная форма. | ||
Строка 31: | Строка 38: | ||
{{Определение|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> это переменная или сорт, либо вид | ||
Строка 37: | Строка 44: | ||
<tex>\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \Pi x : P . Q\text{.}</tex> | <tex>\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \Pi x : P . Q\text{.}</tex> | ||
− | Согласимся '''первым символом''' <tex>t</tex> называть <tex>x</tex> в первом случае, и <tex>\Pi</tex> во втором. '''Первыми переменными''' <tex>t</tex> будем называть переменные <tex>x_1, \ldots, x_n</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 = " | + | ==Задача вывода типов в <tex dpi = "150">\lambda\Pi</tex>-исчислении== |
− | {{Определение|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> называется '''объектом''' (англ. ''object'') в <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=Множество '''чистых термов''' (англ. ''pure terms'') определяется грамматикой <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>. '''Содержимое''' (англ. ''content'') <tex>t</tex> (<tex>\left|t\right|</tex>) {{---}} это рекурсивно определённый чистый терм: |
* <tex>\left|x\right| = x</tex>; | * <tex>\left|x\right| = x</tex>; | ||
− | * <tex>\left|\left( | + | * <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>.}} | ||
− | {{Определение|definition=Чистый терм <tex>t</tex> называется '''типизируемым''' в контексте <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>.}} | + | {{Определение|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>\Gamma</tex> это присвоение типов связанным переменным и некоторым свободным переменным, типов которых нет в <tex>\Gamma</tex>. Если же контекст <tex>\Gamma</tex> пустой, то типизация терма в нём будет являться присваиванием типов и связанным и свободным переменным. | Типизация чистого терма в контексте <tex>\Gamma</tex> это присвоение типов связанным переменным и некоторым свободным переменным, типов которых нет в <tex>\Gamma</tex>. Если же контекст <tex>\Gamma</tex> пустой, то типизация терма в нём будет являться присваиванием типов и связанным и свободным переменным. | ||
Строка 58: | Строка 65: | ||
{{Утверждение|statement=Задача вывода типов в пустом контексте разрешима в <tex>\lambda\Pi</tex>-исчислении.|proof=Типизируемые в пустом контексте чистые термы <tex>\lambda\Pi</tex> исчисления совпадают с типизируемыми выражениями просто типизированного <tex>\lambda</tex>-исчисления, а задача вывода типов в просто типизированном <tex>\lambda</tex>-исчислении разрешима.}} | {{Утверждение|statement=Задача вывода типов в пустом контексте разрешима в <tex>\lambda\Pi</tex>-исчислении.|proof=Типизируемые в пустом контексте чистые термы <tex>\lambda\Pi</tex> исчисления совпадают с типизируемыми выражениями просто типизированного <tex>\lambda</tex>-исчисления, а задача вывода типов в просто типизированном <tex>\lambda</tex>-исчислении разрешима.}} | ||
− | =Неразрешимость задачи вывода типов в <tex dpi=" | + | ==Неразрешимость задачи вывода типов в <tex dpi="150">\lambda\Pi</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>. | + | <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: | Строка 93: | ||
<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>, тогда из типизируемости терма <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>. | ||
}} | }} | ||
+ | |||
+ | ==См. также== | ||
+ | * [[Лямбда-исчисление]] | ||
+ | * [[Примеры неразрешимых задач: проблема соответствий Поста]] | ||
+ | * [[Неразрешимость исчисления предикатов первого порядка]] | ||
+ | * [[Математическая логика]] | ||
+ | |||
+ | ==Источники информации== | ||
+ | * Gilles Dowek, The undecidability of typability in the Lambda-Pi-calculus | ||
+ | * [https://github.com/shd/logic2011 Д. Штукенберг. Лекции по математической логике] | ||
+ | * [https://github.com/artemohanjanyan/tt-conspect Конспект лекций по теории типов] | ||
+ | * Henk Barendregt, Introduction to generalized type systems | ||
+ | |||
+ | [[Категория: Теория формальных языков]] | ||
+ | [[Категория: Теория вычислимости]] | ||
+ | [[Категория: Примеры неразрешимых задач]] |
Текущая версия на 19:15, 4 сентября 2022
Лямбда исчисление с зависимыми типами — расширение просто типизированного лямбда-исчисления, которое позволяет типам зависеть от значений. Например, в языке с таким исчислением функция может возвращать не просто пару чисел, а пару чисел, в которой первое число меньше второго, или если ваша функция принимает число и возвращает массив длины , то это можно будет выразить типом этой функции. Зависимые типы добавляют выразительности типовой системе, что приводит к лучшей проверке корректности программы на этапе компиляции. Однако, как будет показано далее, для этого придётся идти на определённые жертвы: почти всегда придётся явно указывать типы выражений, так как компилятор не сможет справиться с выводом типов для них.
Содержание
-исчисление
Определение: |
Множество термов (англ. term) рекурсивно определяется следующей грамматикой:
.
|
Пусть есть термы и и переменная . Записью обозначается терм, полученный заменой на в . Запись означает, что термы и -эквивалентны.
Определение: |
Контекст (англ. context) это список пар | , где — переменная, — терм.
Определение: |
Правила вывода для нашего исчисления:
где Терм , а — множество корректных контекстов. типизируется (англ. well-typed) в контексте , если существует такой терм , что . |
Отношение редуцируемости на типизируемых термах сильно нормализуемо и обладает ромбовидным свойством. Каждый типизируемый терм имеет единственную нормальную форму, два терма эквивалентны, если у них одинаковая нормальная форма.
Типизируемый в контексте
терм имеет единственный тип с точностью до эквивалентности.Определение: |
Нормальный терм , где это переменная или сорт, либо видСогласимся первым символом (англ. head symbol) называть в первом случае, и во втором. Первыми переменными (англ. top variables) будем называть переменные . | , типизируемый в контекте , имеет либо вид
Задача вывода типов в -исчислении
Определение: |
Терм | типа в контексте называется объектом (англ. object) в , если .
Утверждение: |
Если терм является объёктом в контексте , то он является либо переменной, либо применением, либо абстракцией. Если он является применением , тогда оба терма и являются объектами в , если он является абстракцией , то тогда терм является объектом в контексте . |
Определение: |
Множество чистых термов (англ. pure terms) определяется грамматикой | .
Определение: |
Пусть
| — объект в контексте . Содержимое (англ. content) ( ) — это рекурсивно определённый чистый терм:
Определение: |
Чистый терм | называется типизируемым (англ. typable) в контексте , если существует терм , типизируемый в неком , являющимся расширением , что является объектом в и .
Типизация чистого терма в контексте это присвоение типов связанным переменным и некоторым свободным переменным, типов которых нет в . Если же контекст пустой, то типизация терма в нём будет являться присваиванием типов и связанным и свободным переменным.
Утверждение: |
Задача вывода типов в пустом контексте разрешима в -исчислении. |
Типизируемые в пустом контексте чистые термы | исчисления совпадают с типизируемыми выражениями просто типизированного -исчисления, а задача вывода типов в просто типизированном -исчислении разрешима.
Неразрешимость задачи вывода типов в -исчислении
Рассмотрим контекст
.
Определение: |
Пусть
| — слово двухсимвольного алфавита . Определим и следующим образом:
Утверждение: |
Рассмотрим проблему соответствий Поста для списков слов над двухсимвольным алфавитом и . Непустая последовательность является её решением тогда и только тогда, когда . |
Утверждение: |
Если это такой терм, что терм ( повторяется раз) типизируемый, и он является объектом в неком , то тогда терм типизируется в контексте , и его тип эквивалентен терму для какого-то терма типа в контексте . |
Индукция по | .
Утверждение: |
Пусть — такие нормальные термы, что — типизируемый терм, и его нормальная форма это . Тогда первый символ это либо первый символ , либо первая переменная . |
Пусть | — первый символ . Если не является первой переменной , то первый символ нормальной формы это тоже , значит, это первый символ .
Утверждение: |
Пусть — такой нормальный терм типа в контексте , что нормальная форма равна . Тогда терм является термом вида
для некой последовательности . |
Индукция по числу переменных в | .
Теорема: |
Задача проверки типизируемости чистого терма в заданном контексте неразрешима. |
Доказательство: |
Рассмотрим проблему соответствий Поста для списков слов над двухсимвольным алфавитом и . Построим такой чистый терм , что типизируем в тогда и только тогда, когда проблема соответствий поста имеет решение.
Предположим, что этот терм типизируем, и обозначим тип как . Терм типизируется и является объектом в , значит,, где это терм типа в .Тогда все переменные , связанные в термах , , и , имеют тип . Терм имеет тип , тогда из типизируемости терма мы получаем, что тип переменной имеет вид , и. Точно так же, из типизируемости терма получаем, что, значит, . Из типизируемости терма получаем. Наконец, из типизируемости терма получаем. Поскольку терм имеет тип , первый символ нормальной формы терма не может быть первой переменной , значит, это переменная , и мы получаем, что, где — некий терм типа . Получаем, что
Вторая эквивалентность показывает, что нормальная форма имеет вид
для некоторой последовательности . Третья эквивалентность показывает, что , и первая — что, то есть последовательность является решением проблемы Поста.И наоборот, если предположить, что проблема Поста имеет решение , то можно задать типы переменным , и :и тип всем остальным переменным терма , и получить такой типизируемый в терм , который является объектом и . |
См. также
- Лямбда-исчисление
- Примеры неразрешимых задач: проблема соответствий Поста
- Неразрешимость исчисления предикатов первого порядка
- Математическая логика
Источники информации
- Gilles Dowek, The undecidability of typability in the Lambda-Pi-calculus
- Д. Штукенберг. Лекции по математической логике
- Конспект лекций по теории типов
- Henk Barendregt, Introduction to generalized type systems