Дисциплина типа перекрестка

В математической логике дисциплина типов пересечений — это раздел теории типов, охватывающий системы типов , использующие конструктор типов пересечений. $(\cap )$ для присвоения нескольких типов одному термину. ^[1]В частности, если термин $M$ может быть назначен как тип $\varphi _{1}$ и тип $\varphi _{2}$ , затем $M$ можно назначить тип пересечения $\varphi _{1}\cap \varphi _{2}$ (и наоборот).Следовательно, конструктор типа пересечения можно использовать для выражения конечного гетерогенного специального полиморфизма (в отличие от параметрического полиморфизма ).Например, λ-член $\lambda x.\!(x\;x)$ можно присвоить тип $((\alpha \to \beta )\cap \alpha )\to \beta$ в большинстве систем типа пересечения, принимая в качестве термина переменную $x$ оба типа функции $\alpha \to \beta$ и соответствующий тип аргумента $\alpha$ .

Известные системы типов пересечений включают систему присвоения типов Коппо-Дезани, ^[2] система присвоения типов Барендрегта-Коппо-Дезани, ^[3] и существенная система назначения типов перекрестков. ^[4]Самое поразительное, что системы типа пересечения тесно связаны (и часто точно характеризуют) со свойствами нормализации λ-термов при β-редукции .

В языках программирования, таких как TypeScript ^[5] и Скала, ^[6] Типы пересечений используются для выражения специального полиморфизма .

История

Дисциплина перекрестного типа была впервые разработана Марио Коппо, Марианджолой Дезани-Чианкаглини , Патриком Салле и Гаррелом Поттинджером. ^[2]^[7]^[8]Основной мотивацией было изучение семантических свойств (таких как нормализация ) λ-исчисления с помощью теории типов . ^[9]Хотя первоначальная работа Коппо и Дезани установила теоретико-типовую характеристику сильной нормализации для λI-исчисления, ^[2] Поттинджер распространил эту характеристику на λK-исчисление. ^[7]Кроме того, Салле ввёл понятие универсального типа. $\omega$ который можно приписать любому λ-терму, что соответствует пустому пересечению. ^[8]Использование универсального типа $\omega$ позволил провести детальный анализ нормализации головы, нормализации и сильной нормализации. ^[10]В сотрудничестве с Хенком Барендрегтом была предложена λ-модель фильтра для системы типов пересечений, еще более тесно связывающая типы пересечений с семантикой λ-исчисления.

Из-за соответствия с нормализацией типизация в известных системах типа пересечения (исключая универсальный тип) неразрешима .Кроме того, неразрешимость двойственной проблемы типового обитания в известных системах перекрестного типа. Павел Ужичин доказал ^[11]Позже этот результат был уточнен, показав экспоненциальную полноту пространства обитания типа пересечения 2-го ранга и неразрешимость обитания типа пересечения 3-го ранга. ^[12]Примечательно, что заселенность основного типа разрешима за полиномиальное время . ^[13]

Система присвоения типов Коппо-Дезани

Система присвоения типов Коппо-Дезани. $(\vdash _{\text{CD}})$ расширяет просто типизированное λ-исчисление , позволяя предполагать несколько типов для терминальной переменной. ^[2]

Термин язык

Термин «язык» $(\vdash _{\text{CD}})$ задается λ-термами (или лямбда-выражениями ):

{\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ where }}x{\text{ ranges over term variables}}\\\end{aligned}}

Введите язык

Типовой язык $(\vdash _{\text{CD}})$ индуктивно определяется следующей грамматикой:

{\begin{aligned}\varphi &::=\alpha \mid \sigma \to \varphi &&{\text{ where }}\alpha {\text{ ranges over type variables}}\\\sigma &::=\varphi _{1}\cap \cdots \cap \varphi _{n}&&{\text{ where }}n\geq 1\end{aligned}}

Конструктор типа пересечения ( $\cap$ ) берется по модулю ассоциативности, коммутативности и идемпотентности.

Правила набора текста

Правила набора текста $(\to \!\!{\text{I}})$ , $(\to \!\!{\text{E}})$ , $(\cap {\text{I}})$ , и $(\cap {\text{E}})$ из $(\vdash _{\text{CD}})$ являются:

{\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{CD}}M:\varphi }{\Gamma \vdash _{\text{CD}}\lambda x.\!M:\sigma \to \varphi }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{CD}}M:\sigma \to \varphi \quad \Gamma \vdash _{\text{CD}}N:\sigma }{\Gamma \vdash _{\text{CD}}M\;N:\varphi }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{CD}}M:\varphi _{1}\quad \ldots \quad \Gamma \vdash _{\text{CD}}M:\varphi _{n}}{\Gamma \vdash _{\text{CD}}M:\varphi _{1}\cap \cdots \cap \varphi _{n}}}(\cap {\text{I}})&{\dfrac {(1\leq i\leq n)}{\Gamma ,x:\varphi _{1}\cap \cdots \cap \varphi _{n}\vdash _{\text{CD}}x:\varphi _{i}}}(\cap {\text{E}})\end{array}}

Характеристики

Типизация и нормализация тесно связаны в $(\vdash _{\text{CD}})$ по следующим свойствам: ^[2]

Сокращение темы : Если $\Gamma \vdash _{\text{CD}}M:\sigma$ и $M\to _{\beta }N$ , затем $\Gamma \vdash _{\text{CD}}N:\sigma$ .
Нормализация : Если $\Gamma \vdash _{\text{CD}}M:\sigma$ , затем $M$ имеет β-нормальную форму .
Типизация сильно нормализующих λ-термов : Если $M$ , сильно нормализуется то $\Gamma \vdash _{\text{CD}}M:\sigma$ для некоторых $\Gamma$ и $\sigma$ .
Характеристика λI-нормализации : $M$ имеет нормальную форму в λI-исчислении тогда и только тогда, когда $\Gamma \vdash _{\text{CD}}M:\sigma$ для некоторых $\Gamma$ и $\sigma$ .

Если язык типов расширен и содержит пустое пересечение, т.е. $\sigma =\varphi _{1}\cap \cdots \cap \varphi _{n}{\text{ where }}n=0$ , затем $(\vdash _{\text{CD}})$ замкнут относительно β-равенства, корректен и полон для семантики вывода. ^[14]

Система присвоения типов Барендрегта – Коппо – Дезани

Система присвоения типов Барендрегта – Коппо – Дезани. $(\vdash _{\text{BCD}})$ расширяет систему присвоения типов Коппо-Дезани в следующих трех аспектах: ^[3]

$(\vdash _{\text{BCD}})$ вводит константу универсального типа $\omega$ (сродни пустому пересечению), которое можно приписать любому λ-терму.
$(\vdash _{\text{BCD}})$ позволяет использовать конструктор типа пересечения $(\cap )$ появляться в правой части конструктора типа стрелки $(\to )$ .
$(\vdash _{\text{BCD}})$ представляет подтип типа пересечения $(\leq )$ частичный порядок типов вместе с соответствующим правилом типизации.

Термин язык

Термин «язык» $(\vdash _{\text{BCD}})$ задается λ-термами (или лямбда-выражениями ):

{\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ where }}x{\text{ ranges over term variables}}\\\end{aligned}}

Введите язык

Типовой язык $(\vdash _{\text{BCD}})$ индуктивно определяется следующей грамматикой:

{\begin{aligned}\sigma ,\tau &::=\alpha \mid \omega \mid \sigma \to \tau \mid \sigma \cap \tau &&{\text{ where }}\alpha {\text{ ranges over type variables}}\end{aligned}}

Подтип типа перекрестка

Подтип типа перекрестка $(\leq )$ определяется как наименьший предварительный порядок ( рефлексивное и транзитивное отношение) над типами пересечений, удовлетворяющий следующим свойствам:

{\begin{aligned}&\sigma \leq \omega ,\quad \omega \leq \omega \to \omega ,\quad \sigma \cap \tau \leq \sigma ,\quad \sigma \cap \tau \leq \tau ,\\&(\sigma \to \tau _{1})\cap (\sigma \to \tau _{2})\leq \sigma \to \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma \leq \tau _{1}{\text{ and }}\sigma \leq \tau _{2}{\text{, then }}\sigma \leq \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma _{2}\leq \sigma _{1}{\text{ and }}\tau _{1}\leq \tau _{2}{\text{, then }}\sigma _{1}\to \tau _{1}\leq \sigma _{2}\to \tau _{2}\end{aligned}}

Подтипы типов пересечений разрешимы за квадратичное время. ^[15]

Правила набора текста

Правила набора текста $(\to \!\!{\text{I}})$ , $(\to \!\!{\text{E}})$ , $(\cap {\text{I}})$ , $(\leq )$ , $({\text{A}})$ , и $(\omega )$ из $(\vdash _{\text{BCD}})$ являются:

{\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}\lambda x.\!M:\sigma \to \tau }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \to \tau \quad \Gamma \vdash _{\text{BCD}}N:\sigma }{\Gamma \vdash _{\text{BCD}}M\;N:\tau }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad \Gamma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}M:\sigma \cap \tau }}(\cap {\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad (\sigma \leq \tau )}{\Gamma \vdash _{\text{BCD}}M:\tau }}(\leq )\\\\{\dfrac {}{\Gamma ,x:\sigma \vdash _{\text{BCD}}x:\sigma }}({\text{A}})&{\dfrac {}{\Gamma \vdash _{\text{BCD}}M:\omega }}(\omega )\end{array}}

Характеристики

Семантика : $(\vdash _{\text{BCD}})$ является надежным и полным. λ-модель фильтра, в которой интерпретация λ-терма совпадает с набором типов, которые ему можно присвоить. ^[3]
Сокращение темы : Если $\Gamma \vdash _{\text{BCD}}M:\sigma$ и $M\to _{\beta }N$ , затем $\Gamma \vdash _{\text{BCD}}N:\sigma$ . ^[3]
Расширение темы : Если $\Gamma \vdash _{\text{BCD}}N:\sigma$ и $M\to _{\beta }N$ , затем $\Gamma \vdash _{\text{BCD}}M:\sigma$ . ^[3]
Характеристика сильной нормализации : $M$ сильно нормализует относительно. β-редукция тогда и только тогда, когда $\Gamma \vdash _{\text{BCD}}M:\sigma$ выводится без правила $(\omega )$ для некоторых $\Gamma$ и $\sigma$ . ^[16]
Основные пары : Если $M$ сильно нормализуется, то существует главная пара $(\Gamma ,\sigma )$ такой, что при любом наборе текста $\Gamma '\vdash _{\text{BCD}}M:\sigma '$ пара $(\Gamma ',\sigma ')$ можно получить из главной пары $(\Gamma ,\sigma )$ посредством расширения, поднятия и замены типов. ^[17]

Ссылки

^ Хенк Барендрегт; Уил Деккерс; Ричард Стэтман (20 июня 2013 г.). Лямбда-исчисление с типами . Издательство Кембриджского университета. стр. 1–. ISBN 978-0-521-76614-2 .
^ Перейти обратно: ^а ^б ^с ^д ^и Коппо, Марио; Дезани-Чианкаглини, Марианджола (1980). «Расширение базовой теории функциональности для λ-исчисления» . Журнал формальной логики Нотр-Дама . 21 (4): 685–693. дои : 10.1305/ndjfl/1093883253 . S2CID 29748788 .
^ Перейти обратно: ^а ^б ^с ^д ^и Барендрегт, Хенк; Коппо, Марио; Дезани-Чианкаглини, Марианджола (1983). «Фильтр лямбда-модели и полнота присвоения типа». Журнал символической логики . 48 (4): 931–940. дои : 10.2307/2273659 . JSTOR 2273659 . S2CID 45660117 .
^ ван Бакель, Штеффен (2011). «Строгие типы пересечений для лямбда-исчисления». Обзоры вычислительной техники ACM . 43 (3): 20:1–20:49. CiteSeerX 10.1.1.310.2166 . дои : 10.1145/1922649.1922657 . S2CID 5537689 .
^ «Типы пересечений в TypeScript» . Проверено 1 августа 2019 г.
^ «Составные типы в Scala» . Проверено 1 августа 2019 г.
^ Перейти обратно: ^а ^б Поттинджер, Г. (1980). Присвоение типа сильно нормализуемых λ-термов. Х.Б. Карри: эссе по комбинаторной логике, лямбда-исчислению и формализму, 561–577.
^ Перейти обратно: ^а ^б Коппо, Марио; Дезани-Чианкаглини, Марианджола; Салле, Патрик (1979). «Функциональная характеристика некоторых семантических равенств внутри лямбда-исчисления». В Германе А. Маурере (ред.). Автоматы, языки и программирование, 6-й коллоквиум, Грац, Австрия, 16-20 июля 1979 г., Труды . Том. 71. Спрингер. стр. 133–146. дои : 10.1007/3-540-09510-1_11 . ISBN 3-540-09510-1 .
^ Коппо, Марио; Дезани-Чианкаглини, Марианджола (1978). «Новое присвоение типа для λ-термов». Архив математической логики и фундаментальных исследований . 19 (1): 139–156. дои : 10.1007/BF02011875 . S2CID 206809924 .
^ Коппо, Марио; Дезани-Чианкаглини, Марианджола; Веннери, Бетти (1981). «Функциональные характеры разрешимых термов». Математическая логика Ежеквартальный журнал . 27 (2–6): 45–58. дои : 10.1002/malq.19810270205 .
^ Уржичин, Павел (1999). «Проблема пустоты для типов пересечений». Журнал символической логики . 64 (3): 1195–1215. дои : 10.2307/2586625 . JSTOR 2586625 . S2CID 36979036 .
^ Уржичин, Павел (2009). «Заселение перекрестков низкого ранга». Международная конференция по типизированным лямбда-исчислениям и их приложениям . TLCA 2009. Том. 5608. Спрингер. стр. 356–370. дои : 10.1007/978-3-642-02273-9_26 . ISBN 978-3-642-02272-2 .
^ Дуденхефнер, Андрей; Рехоф, Якоб (2019). «Принципальность и приближение в рамках размерной границы». Труды ACM по языкам программирования . ПОПЛ 2019. Том. 3. АКМ. стр. 8:1–8:29. дои : 10.1145/3290321 . ISSN 2475-1421 .
^ Ван Бакель, Штеффен (1992). «Полные ограничения дисциплины типа перекрестка». Теоретическая информатика . 102 (1): 135–163. CiteSeerX 10.1.1.310.903 . дои : 10.1016/0304-3975(92)90297-С .
^ Дуденхефнер, Андрей; Мартенс, Мориц; Рехоф, Якоб (2017). «Алгебраическая задача объединения типов пересечений». Логические методы в информатике . 13 (3). дои : 10.23638/LMCS-13(3:9)2017 . S2CID 31640337 .
^ Гилезан, Сильвия (1996). «Сильная нормализация и типизация с типами пересечений» . Журнал формальной логики Нотр-Дама . 37 (1): 44–52. дои : 10.1305/ndjfl/1040067315 .
^ Рончи Делла Рокка, Симона; Веннери, Бетти (1983). «Основные схемы типов расширенной теории типов» . Теоретическая информатика . 28 ((1-2)): 151–169. дои : 10.1016/0304-3975(83)90069-5 .

[BDS13-1] Хенк Барендрегт; Уил Деккерс; Ричард Стэтман (20 июня 2013 г.). Лямбда-исчисление с типами . Издательство Кембриджского университета. стр. 1–. ISBN 978-0-521-76614-2 .

[CD80-2] Перейти обратно: ^а ^б ^с ^д ^и Коппо, Марио; Дезани-Чианкаглини, Марианджола (1980). «Расширение базовой теории функциональности для λ-исчисления» . Журнал формальной логики Нотр-Дама . 21 (4): 685–693. дои : 10.1305/ndjfl/1093883253 . S2CID 29748788 .

[BCD83-3] Перейти обратно: ^а ^б ^с ^д ^и Барендрегт, Хенк; Коппо, Марио; Дезани-Чианкаглини, Марианджола (1983). «Фильтр лямбда-модели и полнота присвоения типа». Журнал символической логики . 48 (4): 931–940. дои : 10.2307/2273659 . JSTOR 2273659 . S2CID 45660117 .

[B11-4] ван Бакель, Штеффен (2011). «Строгие типы пересечений для лямбда-исчисления». Обзоры вычислительной техники ACM . 43 (3): 20:1–20:49. CiteSeerX 10.1.1.310.2166 . дои : 10.1145/1922649.1922657 . S2CID 5537689 .

[TS-5] «Типы пересечений в TypeScript» . Проверено 1 августа 2019 г.

[6] «Составные типы в Scala» . Проверено 1 августа 2019 г.

[P80-7] Перейти обратно: ^а ^б Поттинджер, Г. (1980). Присвоение типа сильно нормализуемых λ-термов. Х.Б. Карри: эссе по комбинаторной логике, лямбда-исчислению и формализму, 561–577.

[CDS79-8] Перейти обратно: ^а ^б Коппо, Марио; Дезани-Чианкаглини, Марианджола; Салле, Патрик (1979). «Функциональная характеристика некоторых семантических равенств внутри лямбда-исчисления». В Германе А. Маурере (ред.). Автоматы, языки и программирование, 6-й коллоквиум, Грац, Австрия, 16-20 июля 1979 г., Труды . Том. 71. Спрингер. стр. 133–146. дои : 10.1007/3-540-09510-1_11 . ISBN 3-540-09510-1 .

[CD78-9] Коппо, Марио; Дезани-Чианкаглини, Марианджола (1978). «Новое присвоение типа для λ-термов». Архив математической логики и фундаментальных исследований . 19 (1): 139–156. дои : 10.1007/BF02011875 . S2CID 206809924 .

[CDV81-10] Коппо, Марио; Дезани-Чианкаглини, Марианджола; Веннери, Бетти (1981). «Функциональные характеры разрешимых термов». Математическая логика Ежеквартальный журнал . 27 (2–6): 45–58. дои : 10.1002/malq.19810270205 .

[U99-11] Уржичин, Павел (1999). «Проблема пустоты для типов пересечений». Журнал символической логики . 64 (3): 1195–1215. дои : 10.2307/2586625 . JSTOR 2586625 . S2CID 36979036 .

[U09-12] Уржичин, Павел (2009). «Заселение перекрестков низкого ранга». Международная конференция по типизированным лямбда-исчислениям и их приложениям . TLCA 2009. Том. 5608. Спрингер. стр. 356–370. дои : 10.1007/978-3-642-02273-9_26 . ISBN 978-3-642-02272-2 .

[DR19-13] Дуденхефнер, Андрей; Рехоф, Якоб (2019). «Принципальность и приближение в рамках размерной границы». Труды ACM по языкам программирования . ПОПЛ 2019. Том. 3. АКМ. стр. 8:1–8:29. дои : 10.1145/3290321 . ISSN 2475-1421 .

[VB92-14] Ван Бакель, Штеффен (1992). «Полные ограничения дисциплины типа перекрестка». Теоретическая информатика . 102 (1): 135–163. CiteSeerX 10.1.1.310.903 . дои : 10.1016/0304-3975(92)90297-С .

[DMR17-15] Дуденхефнер, Андрей; Мартенс, Мориц; Рехоф, Якоб (2017). «Алгебраическая задача объединения типов пересечений». Логические методы в информатике . 13 (3). дои : 10.23638/LMCS-13(3:9)2017 . S2CID 31640337 .

[G96-16] Гилезан, Сильвия (1996). «Сильная нормализация и типизация с типами пересечений» . Журнал формальной логики Нотр-Дама . 37 (1): 44–52. дои : 10.1305/ndjfl/1040067315 .

[RDRV83-17] Рончи Делла Рокка, Симона; Веннери, Бетти (1983). «Основные схемы типов расширенной теории типов» . Теоретическая информатика . 28 ((1-2)): 151–169. дои : 10.1016/0304-3975(83)90069-5 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]