Система чистого типа

Нерешенная проблема в информатике :

Докажите или опровергните гипотезу Барендрегта – Гёверса – Клопа.

(больше нерешенных проблем в информатике)

В отраслях математической логики , известной как доказательство теории и теории типов , в чистом типа системы ( PTS ), ранее известный как обобщенный тип системы ( ГТС ), является формой типизированного лямбда - исчисления , что позволяет произвольное количество видов и зависимостей между любой из этих. Рамки можно рассматривать как обобщение Барендрегт «s лямбда - куба , в том смысле , что все углы куба могут быть представлены в виде экземпляров ВТС с только два рода. ^[1]^[2] Фактически, Барендрегт (1991) построил свой куб именно в этом контексте.^[3] Системы чистых типов могут скрывать различие между типами и терминами и разрушать иерархию типов , как в случае с исчислением конструкций , но это обычно не так, например, просто типизированное лямбда-исчисление позволяет только термам зависеть от термины.

Системы чистых типов были независимо введены Стефано Берарди (1988) и Яном Терлоу (1989). ^[1]^[2] Барендрегт подробно обсуждал их в своих последующих статьях. ^[4] В своей докторской диссертации ^[5] Берарди определил куб конструктивных логик, родственных лямбда-кубу (эти спецификации не зависят друг от друга). Модификация этого куба была позже названа Гёверсом L-кубом, который в своей докторской диссертации расширил соответствие Карри – Ховарда на этот параметр. ^[6] Основываясь на этих идеях, Барт и другие определили классические системы чистых типов ( CPTS ), добавив оператор двойного отрицания . ^[7] Точно так же в 1998 году Tijn Borghuis представила модальные системы чистого типа ( MPTS ). ^[8] Рурда обсуждал применение систем чистых типов к функциональному программированию ; и Рорда и Джеуринг предложили язык программирования, основанный на системах чистых типов. ^[9]

Все системы из лямбда-куба сильно нормализуют . Системы чистых типов вообще не обязательно должны быть, например Система U из парадокса Жирара - нет. (Грубо говоря, Жирар нашел чистые системы, в которых можно выразить предложение «типы образуют тип».) Более того, все известные примеры чистых систем типов, которые не являются строго нормализующими, даже (слабо) нормализуют : они содержат выражения, которые не имеют нормальных форм , как и нетипизированное лямбда-исчисление ^{[ необходима ссылка ]}. Это большая открытая проблема в данной области, всегда ли это так, т.е. всегда ли (слабо) нормализующий PTS обладает свойством сильной нормализации. Это известно как гипотеза Барендрегта – Гёверса – Клопа ^[10] (названная в честь Хенка Барендрегта , Германа Гёверса и Яна Виллема Клопа ).

Определение [ править ]

Система чистых типов определяется тройкой, где - набор сортов, - набор аксиом и - набор правил. Набор текста в системах чистых типов определяется следующими правилами, где любой вид: ^[4] ${\textstyle ({\mathcal {S}},{\mathcal {A}},{\mathcal {R}})}$ ${\textstyle {\mathcal {S}}}$ ${\textstyle {\mathcal {A}}\subseteq {\mathcal {S}}^{2}}$ ${\textstyle {\mathcal {R}}\subseteq {\mathcal {S}}^{3}}$ ${\textstyle s}$

${\frac {(s_{1},s_{2})\in {\mathcal {A}}}{\vdash s_{1}:s_{2}}}\quad {\text{(axiom)}}$

${\frac {\Gamma \vdash A:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:A\vdash x:A}}\quad {\text{(start)}}$

${\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:C\vdash A:B}}\quad {\text{(weakening)}}$

${\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad (s_{1},s_{2},s_{3})\in {\mathcal {R}}}{\Gamma \vdash \Pi x:A.B:s_{3}}}\quad {\text{(product)}}$

${\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[x:=a]}}\quad {\text{(application)}}$

${\frac {\Gamma ,x:A\vdash b:B\quad \Gamma \vdash \Pi x:A.B:s}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(abstraction)}}$

${\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(conversion)}}$

Реализации [ править ]

Следующие языки программирования имеют системы чистых типов: ^{[ необходима цитата ]}

МУДРЕЦ ^[11]
Тысячелистник ^[12]
Хенк 2000 ^[13]

См. Также [ править ]

Система U - пример противоречивой PTS
λμ-исчисление использует другой подход к контролю, чем CPTS

Заметки [ править ]

^ a b Пирс, Бенджамин (2002). Типы и языки программирования . MIT Press. п. 466 . ISBN 0-262-16209-1.
^ a b Kamareddine, Fairouz D .; Лаан, Тван; Недерпелт, Роб П. (2004). «Раздел 4c: Системы чистых типов». Современный взгляд на теорию типов: от истоков до наших дней . Springer. п. 116. ISBN 1-4020-2334-0.
^ Barendregt, HP (1991). «Введение в системы обобщенных типов» . Журнал функционального программирования . 1 (2): 125–154. DOI : 10.1017 / s0956796800020025 . ЛВП : 2066/17240 .
^ a b Барендрегт, Х. (1992). «Лямбда-исчисления с типами» . По Абрамскому, С .; Gabbay, D .; Майбаум, Т. (ред.). Справочник по логике в компьютерных науках . Оксфордские научные публикации .
^ Берарди, С. (1990). Типовая зависимость и конструктивная математика (кандидатская диссертация). Университет Турина.
^ Geuvers, H. (1993). Логика и системы типов (кандидатская диссертация). Университет Неймегена. CiteSeerX 10.1.1.56.7045 .
^ Barthe, G .; Hatcliff, J .; Соренсен, MH (1997). «Понятие классической системы чистых типов». Электронные заметки по теоретической информатике . 6 : 4–59. CiteSeerX 10.1.1.32.1371 . DOI : 10.1016 / S1571-0661 (05) 80170-7 .
^ Borghuis, Tijn (1998). «Модальные системы чистого типа». Журнал логики, языка и информации . 7 (3): 265–296. DOI : 10,1023 / A: 1008254612284 . S2CID 5067584 .
^ Ян-Виллем Рурда; Йохан Джеуринг. «Системы чистого типа для функционального программирования» . Архивировано из оригинала на 2011-10-02 . Проверено 29 августа 2010 . Магистерская диссертация Рурды (ссылка на цитируемую страницу) также содержит общее введение в системы чистых типов.
^ Соренсен, Мортен Гейне; Уржичин, Павел (2006). «Системы чистых типов и лямбда-куб § 14.7» . Лекции об изоморфизме Карри – Ховарда . Эльзевир. п. 358. ISBN 0-444-52077-5.
^ МУДРЕЦ
^ Тысячелистник
^ Хенк 2000

Ссылки [ править ]

Берарди, Стефано (1988). К математическому анализу исчисления конструкций Кокана – Хюэ и других систем в кубе Барендрегта (Технический отчет). Департамент компьютерных наук, CMU, и Dipartimento Matematica, Universita di Torino. CMU-CS-88-131.
Терлоу, Дж. (1989). "Een nadere bewijstheoretische analysis van GSTTs" (на голландском языке). Нидерланды: Университет Неймегена. Cite journal requires |journal= (help)

Дальнейшее чтение [ править ]

Шмидт, Дэвид А. (1994). «§ 8.3 Системы обобщенных типов» . Структура типизированных языков программирования . MIT Press. С. 255–8. ISBN 0-262-19349-3.

Внешние ссылки [ править ]

Система чистых типов в nLab
Джонс, Роджер Бишоп (1999). «Обзор систем чистого типа» .

[pierce2002-1] Пирс, Бенджамин (2002). Типы и языки программирования . MIT Press. п. 466 . ISBN 0-262-16209-1.

[k116-2] Kamareddine, Fairouz D .; Лаан, Тван; Недерпелт, Роб П. (2004). «Раздел 4c: Системы чистых типов». Современный взгляд на теорию типов: от истоков до наших дней . Springer. п. 116. ISBN 1-4020-2334-0.

[3] Barendregt, HP (1991). «Введение в системы обобщенных типов» . Журнал функционального программирования . 1 (2): 125–154. DOI : 10.1017 / s0956796800020025 . ЛВП : 2066/17240 .

[Barendregt92-4] Барендрегт, Х. (1992). «Лямбда-исчисления с типами» . По Абрамскому, С .; Gabbay, D .; Майбаум, Т. (ред.). Справочник по логике в компьютерных науках . Оксфордские научные публикации .

[:0-5] Берарди, С. (1990). Типовая зависимость и конструктивная математика (кандидатская диссертация). Университет Турина.

[6] Geuvers, H. (1993). Логика и системы типов (кандидатская диссертация). Университет Неймегена. CiteSeerX 10.1.1.56.7045 .

[7] Barthe, G .; Hatcliff, J .; Соренсен, MH (1997). «Понятие классической системы чистых типов». Электронные заметки по теоретической информатике . 6 : 4–59. CiteSeerX 10.1.1.32.1371 . DOI : 10.1016 / S1571-0661 (05) 80170-7 .

[8] Borghuis, Tijn (1998). «Модальные системы чистого типа». Журнал логики, языка и информации . 7 (3): 265–296. DOI : 10,1023 / A: 1008254612284 . S2CID 5067584 .

[9] Ян-Виллем Рурда; Йохан Джеуринг. «Системы чистого типа для функционального программирования» . Архивировано из оригинала на 2011-10-02 . Проверено 29 августа 2010 . Магистерская диссертация Рурды (ссылка на цитируемую страницу) также содержит общее введение в системы чистых типов.

[10] Соренсен, Мортен Гейне; Уржичин, Павел (2006). «Системы чистых типов и лямбда-куб § 14.7» . Лекции об изоморфизме Карри – Ховарда . Эльзевир. п. 358. ISBN 0-444-52077-5.

[sage-11] МУДРЕЦ

[yarrow-12] Тысячелистник

[henk2000-13] Хенк 2000

[1]