Система чистого типа - Pure type system - Wikipedia

Нерешенная проблема в информатике: Докажите или опровергните гипотезу Барендрегта – Гёверса – Клопа. (больше нерешенных проблем в информатике)

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

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

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

Определение

Система чистого типа определяется тройкой ${\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}$ любой^[4]:

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

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

${\displaystyle {\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)}}}$

${\displaystyle {\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)}}}$

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

${\displaystyle {\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)}}}$

${\displaystyle {\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

Примечания

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

Рекомендации

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

дальнейшее чтение

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

внешняя ссылка

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