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

Нерешенная задача в информатике :

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

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

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

Системы чистых типов были независимо представлены Стефано Берарди (1988) и Яном Терлоу (1989). ^[1]^[2] Барендрегт подробно обсуждал их в своих последующих статьях. ^[4] В своей кандидатской диссертации ^[5] Берарди определил куб конструктивной логики, аналогичный лямбда-кубу (эти спецификации независимы). Модификацию этого куба позже назвал L-куб Герман Геверс, который в своей докторской диссертации распространил соответствие Карри-Ховарда на этот параметр. ^[6] Основываясь на этих идеях, Г. Барт и другие определили классические системы чистого типа ( CPTS ), добавив оператор двойного отрицания . ^[7] Аналогичным образом, в 1998 году Тейн Боргуис представил модальные системы чистого типа ( 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]

${\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 – пример противоречивого ВТС
λμ-исчисление использует другой подход к управлению, чем CPTS.

Примечания

^ Jump up to: ^а ^б Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. п. 466 . ISBN 0-262-16209-1 .
^ Jump up to: ^а ^б Камареддин, Файруз Д.; Лаан, Тван; Недерпельт, Роб П. (2004). «Раздел 4c: Системы чистого типа». Современный взгляд на теорию типов: от ее истоков до сегодняшнего дня . Спрингер. п. 116. ИСБН 1-4020-2334-0 .
^ Барендрегт, HP (1991). «Введение в системы обобщенных типов» . Журнал функционального программирования . 1 (2): 125–154. дои : 10.1017/s0956796800020025 . hdl : 2066/17240 . S2CID 44757552 .
^ Jump up to: ^а ^б Барендрегт, Х. (1992). «Лямбда-исчисления с типами» . В Абрамский С.; Габбай, Д.; Майбаум, Т. (ред.). Справочник по логике в информатике . Оксфордские научные публикации .
^ Берарди, С. (1990). Типовая зависимость и конструктивная математика (кандидатская диссертация). Туринский университет .
^ Геверс, Х. (1993). Логика и системы типов (кандидатская диссертация). Университет Неймегена . CiteSeerX 10.1.1.56.7045 .
^ Барт, Г.; Хэтклифф, Дж.; Соренсен, МЗ (1997). «Понятие классической системы чистых типов». Электронные заметки по теоретической информатике . 6 :4–59. CiteSeerX 10.1.1.32.1371 . дои : 10.1016/S1571-0661(05)80170-7 .
^ Боргуис, Тейн (1998). «Модальные системы чистого типа». Журнал логики, языка и информации . 7 (3): 265–296. дои : 10.1023/А:1008254612284 . S2CID 5067584 .
^ Ян-Виллем Рурда; Йохан Йеуринг. «Системы чистых типов для функционального программирования» . Архивировано из оригинала 2 октября 2011 г. Проверено 29 августа 2010 г. Магистерская диссертация Рурды (ссылка на цитируемой странице) также содержит общее введение в системы чистых типов.
^ Соренсен, Мортен Хейне; Уржичин, Павел (2006). «Системы чистых типов и лямбда-куб § 14.7» . Лекции по изоморфизму Карри–Говарда . Эльзевир. п. 358. ИСБН 0-444-52077-5 .
^ МУДРЕЦ
^ Тысячелистник
^ Хенк 2000

Ссылки

Берарди, Стефано (1988). К математическому анализу конструктивного исчисления Кокана – Юэ и других систем в кубе Барендрегта (Технический отчет). Департамент компьютерных наук CMU и Dipartimento Matematica Туринского университета. КМУ-КС-88-131.
Терлоу, Дж. (1989). «Дальнейший теоретико-доказательный анализ GSTT» (Документ) (на голландском языке). Нидерланды: Университет Неймегена.

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

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

Внешние ссылки

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

[pierce2002-1] Jump up to: ^а ^б Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. п. 466 . ISBN 0-262-16209-1 .

[k116-2] Jump up to: ^а ^б Камареддин, Файруз Д.; Лаан, Тван; Недерпельт, Роб П. (2004). «Раздел 4c: Системы чистого типа». Современный взгляд на теорию типов: от ее истоков до сегодняшнего дня . Спрингер. п. 116. ИСБН 1-4020-2334-0 .

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

[Barendregt92-4] Jump up to: ^а ^б Барендрегт, Х. (1992). «Лямбда-исчисления с типами» . В Абрамский С.; Габбай, Д.; Майбаум, Т. (ред.). Справочник по логике в информатике . Оксфордские научные публикации .

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

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

[7] Барт, Г.; Хэтклифф, Дж.; Соренсен, МЗ (1997). «Понятие классической системы чистых типов». Электронные заметки по теоретической информатике . 6 :4–59. CiteSeerX 10.1.1.32.1371 . дои : 10.1016/S1571-0661(05)80170-7 .

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

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

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

[sage-11] МУДРЕЦ

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

[henk2000-13] Хенк 2000

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]