113
правок
Изменения
→\lambda\Pi-исчисление
Лямбда исчисление с зависимыми типами {{---}} расширение просто типизированного [[Лямбда-исчисление|лямбда-исчисления]], которое позволяет типам зависеть от значений. Например, в языке с таким исчислением функция может возвращать не просто пару чисел, а пару чисел, в которой первое число меньше второго, или если ваша функция принимает число <tex>n</tex> и возвращает массив длины <tex>n</tex>, то это можно будет выразить типом этой функции. Зависимые типы добавляют выразительности типовой системе, что приводит к лучшей проверке корректности программы на этапе компиляции. Однако, как будет показано далее, для этого придётся идти на определённые жертвы: почти всегда придётся явно указывать типы выражений, так как компилятор не сможет справиться с выводом типов для них. ==<tex dpi = "180150">\lambda\Pi</tex>-исчисление==
{{Определение|definition=Множество '''термов''' (англ. ''term'') рекурсивно определяется следующей грамматикой:
\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' : xs}{\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} \\
</tex>
где <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>) {{---}} это рекурсивно определённый чистый терм:
* <tex>\left|x\right| = x</tex>;
* <tex>\left|\lambda x : U . t\right| = \lambda x . \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> пустой, то типизация терма в нём будет являться присваиванием типов и связанным и свободным переменным.
{{Утверждение|statement=Задача вывода типов в пустом контексте разрешима в <tex>\lambda\Pi</tex>-исчислении.|proof=Типизируемые в пустом контексте чистые термы <tex>\lambda\Pi</tex> исчисления совпадают с типизируемыми выражениями просто типизированного <tex>\lambda</tex>-исчисления, а задача вывода типов в просто типизированном <tex>\lambda</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>.
|proof=Индукция по <tex>n</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
[[Категория: Теория формальных языков]]
[[Категория: Теория вычислимости]]
[[Категория: Примеры неразрешимых задач]]
