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

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

В филиалах математическая логика известный как теория доказательств и теория типов, а система чистых типов (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] (названный в честь Хенк Барендрегт, Герман Гёверс, и Ян Виллем Клоп ).

Определение

Система чистого типа определяется тройкой куда это своего рода набор, - это набор аксиом, а это свод правил. Набор текста в системах чистого типа определяется следующими правилами, где любой[4]:

Реализации

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

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

Смотрите также

Примечания

  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" (на голландском языке). Нидерланды: Университет Неймегена. Цитировать журнал требует | журнал = (помощь)

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

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