Система F - System F

Для исполнителей электронной транс-музыки см. Ферри Корстен.

Система F, также известный как (Жирар – Рейнольдс) полиморфное лямбда-исчисление или лямбда-исчисление второго порядка, это типизированное лямбда-исчисление это отличается от просто типизированное лямбда-исчисление за счет внедрения механизма универсальная количественная оценка над типами. Таким образом, система F формализует понятие параметрический полиморфизм в языки программирования, и формирует теоретическую основу для таких языков, как Haskell и ML. Система F была открыта независимо логик Жан-Ив Жирар (1972) и специалист в области информатики Джон С. Рейнольдс (1974).

В то время как просто типизированное лямбда-исчисление имеет переменные в диапазоне терминов и связующие для них, Система F дополнительно имеет переменные в диапазоне типы, и связующие к ним. Например, тот факт, что функция идентичности может иметь любой тип формы A → A, будет формализован в Системе F как суждение

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

куда ${\displaystyle \alpha }$ это переменная типа. Верхний регистр ${\displaystyle \Lambda }$ традиционно используется для обозначения функций уровня типа, в отличие от строчных букв ${\displaystyle \lambda }$ который используется для функций уровня значений. (Надстрочный ${\displaystyle \alpha }$ означает, что граница Икс относится к типу ${\displaystyle \alpha }$; выражение после двоеточия является типом предшествующего лямбда-выражения.)

Как система переписывания терминов, Система F сильно нормализующий. Однако вывод типа в Системе F (без явных аннотаций типов) неразрешим. Под Изоморфизм Карри – Ховарда, Система F соответствует фрагменту второго порядка интуиционистская логика который использует только универсальную количественную оценку. Систему F можно рассматривать как часть лямбда-куб, вместе с еще более выразительными типизированными лямбда-исчислениями, в том числе с зависимые типы.

По словам Жирара, буква «F» в Система F был выбран случайно.^[1]

Правила набора

Правила типизации Системы F - это правила просто типизированного лямбда-исчисления с добавлением следующего:

${\displaystyle {\frac {\Gamma \vdash M{\mathbin {:}}\forall \alpha .\sigma }{\Gamma \vdash M\tau {\mathbin {:}}\sigma [\tau /\alpha ]}}}$ (1)

${\displaystyle {\frac {\Gamma ,\alpha ~{\text{type}}\vdash M{\mathbin {:}}\sigma }{\Gamma \vdash \Lambda \alpha .M{\mathbin {:}}\forall \alpha .\sigma }}}$ (2)

куда ${\displaystyle \sigma ,\tau }$ типы, ${\displaystyle \alpha }$ это переменная типа, а ${\displaystyle \alpha ~{\text{type}}}$ в контексте указывает, что ${\displaystyle \alpha }$ связан. Первое правило - это правило приложения, а второе - правило абстракции.^[2][3]

Логика и предикаты

В ${\displaystyle {\mathsf {Boolean}}}$ тип определяется как:${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$, куда ${\displaystyle \alpha }$ это переменная типа. Это означает: ${\displaystyle {\mathsf {Boolean}}}$ - это тип всех функций, которые принимают на входе тип α и два выражения типа α и производят на выходе выражение типа α (обратите внимание, что мы рассматриваем ${\displaystyle \to }$ быть правоассоциативный.)

Следующие два определения логических значений ${\displaystyle \mathbf {T} }$ и ${\displaystyle \mathbf {F} }$ используются, расширяя определение Церковные логические значения:

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

(Обратите внимание, что для указанных выше двух функций требуется три - не два - аргумента. Последние два должны быть лямбда-выражениями, но первое должно быть типом. Этот факт отражается в том, что тип этих выражений ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$; универсальный квантор, связывающий α, соответствует Λ, связывающему альфа в самом лямбда-выражении. Также обратите внимание, что ${\displaystyle {\mathsf {Boolean}}}$ удобное сокращение для ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$, но это не символ самой Системы F, а скорее «метасимвол». Так же, ${\displaystyle \mathbf {T} }$ и ${\displaystyle \mathbf {F} }$ также являются «метасимволами», удобными сокращениями «сборок» Системы F (в Чувство Бурбаки ); в противном случае, если бы такие функции могли быть названы (в Системе F), тогда не было бы необходимости в лямбда-выражающем аппарате, способном определять функции анонимно и для комбинатор с фиксированной точкой, что позволяет обойти это ограничение.)

Затем с этими двумя ${\displaystyle \lambda }$-термы, мы можем определить некоторые логические операторы (которые имеют тип ${\displaystyle {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}}$):

${\displaystyle {\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {F} \,\mathbf {T} \end{aligned}}}$

Обратите внимание, что в определениях выше, ${\displaystyle {\mathsf {Boolean}}}$ аргумент типа для ${\displaystyle x}$, указывая, что два других параметра, которые передаются ${\displaystyle x}$ относятся к типу ${\displaystyle {\mathsf {Boolean}}}$. Как и в церковных кодировках, нет необходимости в IFTHENELSE работать так, как можно просто использовать сырые ${\displaystyle {\mathsf {Boolean}}}$-типированные термины как функции принятия решений. Однако, если об этом попросят:

${\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

сделаю. предикат это функция, которая возвращает ${\displaystyle {\mathsf {Boolean}}}$-типированное значение. Самый фундаментальный предикат - это ISZERO который возвращается ${\displaystyle \mathbf {T} }$ тогда и только тогда, когда его аргументом является Церковная цифра 0:

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

Структуры системы F

Система F позволяет встраивать рекурсивные конструкции естественным образом, как и в Теория типов Мартина-Лёфа. Абстрактные структуры (S) создаются с использованием конструкторы. Это функции, набранные как:

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$.

Рекурсивность проявляется при ${\displaystyle S}$ сам появляется в одном из типов ${\displaystyle K_{i}}$. Если у вас есть ${\displaystyle m}$ из этих конструкторов вы можете определить тип ${\displaystyle S}$ в качестве:

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

Например, натуральные числа можно определить как индуктивный тип данных. ${\displaystyle N}$ с конструкторами

${\displaystyle {\mathit {zero}}:\mathrm {N} }$

${\displaystyle {\mathit {succ}}:\mathrm {N} \rightarrow \mathrm {N} }$

Тип системы F, соответствующий этой структуре:${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$. Термины этого типа представляют собой типизированную версию Церковные цифры, первые из которых:

0 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x}$

1 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx}$

2 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)}$

3 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))}$

Если мы изменим порядок каррированных аргументов (т.е. ${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$), то цифра Чёрча для ${\displaystyle n}$ это функция, которая принимает функцию ж в качестве аргумента и возвращает ${\displaystyle n}$^th сила ж. То есть цифра Чёрча - это функция высшего порядка - принимает функцию с одним аргументом ж, и возвращает другую функцию с одним аргументом.

Использование в языках программирования

Версия Системы F, используемая в этой статье, представляет собой явно типизированное исчисление в стиле Чёрча. Информация о типе, содержащаяся в λ-термах, делает проверка типов простой. Джо Уэллс (1994) разрешил «неприятную открытую проблему», доказав, что проверка типов неразрешимый для варианта системы F в стиле Карри, то есть такой, в которой отсутствуют явные аннотации ввода.^[4][5]

Результат Уэллса означает, что вывод типа для Системы F невозможно. Ограничение Системы F, известное как "Хиндли-Милнер "или просто" HM "имеет простой алгоритм вывода типов и используется во многих статически типизированный функциональные языки программирования Такие как Haskell 98 и ML семья. Со временем, когда ограничения систем типов в стиле HM стали очевидными, языки неуклонно переходили к более выразительной логике для своих систем типов. GHC компилятор Haskell, выходит за рамки HM (по состоянию на 2008 г.) и использует System F, расширенную несинтаксическим равенством типов;^[6] не-HM особенности в OCaml система типов включает GADT.^[7][8]

Изоморфизм Жирара-Рейнольдса

Во втором порядке интуиционистская логика полиморфное лямбда-исчисление второго порядка (F2) было открыто Жираром (1972) и независимо Рейнольдсом (1974).^[9] Жирар доказал Теорема представления: что в интуиционистской логике предикатов второго порядка (P2) функции от натуральных чисел до натуральных чисел, которые могут быть доказаны как полные, образуют проекцию из P2 в F2.^[9] Рейнольдс доказал Теорема об абстракции: что каждый член в F2 удовлетворяет логическому отношению, которое может быть вложено в логические отношения P2.^[9] Рейнольдс доказал, что проекция Жирара с последующим вложением Рейнольдса образуют тождество, т. Е. Изоморфизм Жирара-Рейнольдса.^[9]

Система F_ω

Система F соответствует первой оси Барендрегта лямбда-куб, Система F_ω или полиморфное лямбда-исчисление высшего порядка совмещает первую ось (полиморфизм) со второй осью (операторы типа ); это другая, более сложная система.

Система F_ω можно определить индуктивно на семействе систем, где индукция основана на виды разрешено в каждой системе:

• ${\displaystyle F_{n}}$ виды разрешений:
  • ${\displaystyle \star }$ (вид типов) и
  • ${\displaystyle J\Rightarrow K}$ куда ${\displaystyle J\in F_{n-1}}$ и ${\displaystyle K\in F_{n}}$ (вид функций от типов к типам, где тип аргумента имеет более низкий порядок)

В пределе можно определить систему ${\displaystyle F_{\omega }}$ быть

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

То есть F_ω - это система, которая позволяет выполнять функции от типов к типам, где аргумент (и результат) может иметь любой порядок.

Обратите внимание, что хотя F_ω не накладывает ограничений на порядок аргументов в этих отображениях, это ограничивает вселенная аргументов для этих отображений: они должны быть типами, а не значениями. Система F_ω не позволяет отображать значения в типы (Зависимые типы ), хотя он позволяет отображать значения в значения (${\displaystyle \lambda }$ абстракция), отображения типов в значения (${\displaystyle \Lambda }$ абстракция, иногда пишется ${\displaystyle \forall }$) и отображения типов в типы (${\displaystyle \lambda }$ абстракция на уровне типов)

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

• Экзистенциальные типы - экзистенциально определенные аналоги универсальных типов
• Система F_<: - расширяет систему F подтипами
• Система U

Примечания

1. Жирар, Жан-Ив (1986). «Система F переменных типов, пятнадцать лет спустя». Теоретическая информатика. 45: 160. Дои:10.1016/0304-3975(86)90044-7. Однако в [3] было показано, что очевидные правила преобразования для этой системы, случайно названной F, сходятся.
2. Харпер Р. "Практические основы языков программирования, второе издание" (PDF). С. 142–3.
3. Геверс Х., Нордстрём Б., Довек Г. «Доказательства программ и формализация математики» (PDF). п. 51.
4. Уэллс, Дж. Б. (20 января 2005 г.). «Исследовательские интересы Джо Уэллса». Университет Хериот-Ватт.
5. Уэллс, Дж. Б. (1999). «Типизация и проверка типов в Системе F эквивалентны и неразрешимы». Анна. Pure Appl. Логика. 98 (1–3): 111–156. Дои:10.1016 / S0168-0072 (98) 00047-5.«Проект Чёрча: типизация и проверка типов в {S} ystem {F} эквивалентны и неразрешимы». 29 сентября 2007 г. Архивировано с оригинал 29 сентября 2007 г.
6. «Система FC: ограничения и принуждения равенства». gitlab.haskell.org. Получено 2019-07-08.
7. «Примечания к выпуску OCaml 4.00.1». ocaml.org. 2012-10-05. Получено 2019-09-23.
8. "Справочное руководство по OCaml 4.09". 2012-09-11. Получено 2019-09-23.
9. Филип Вадлер (2005) Изоморфизм Жирара-Рейнольдса (второе издание) Эдинбургский университет, Языки программирования и основы в Эдинбурге

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

• Жирар, Жан-Ив (1971). "Une Extension de l'Interpretation de l'Interpretation of Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Материалы Второго симпозиума по скандинавской логике. Амстердам. С. 63–92. Дои:10.1016 / S0049-237X (08) 70843-7.
• Жирар, Жан-Ив (1972), Функция интерпретации и выявление купюр в искусстве арифметики высшего качества (Докторская диссертация) (на французском языке), Université Paris 7.
• Рейнольдс, Джон (1974). К теории структуры типов.
• Жирар, Жан-Ив; Лафон, Ив; Тейлор, Пол (1989). Доказательства и типы. Издательство Кембриджского университета. ISBN  978-0-521-37181-0.
• Уэллс, Дж. Б. (1994). «Типизация и проверка типов в лямбда-исчислении второго порядка эквивалентны и неразрешимы». Материалы 9-го ежегодного IEEE Симпозиум по логике в компьютерных науках (LICS). С. 176–185. Дои:10.1109 / LICS.1994.316068. ISBN  0-8186-6310-3. Версия PostScript

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

• Пирс, Бенджамин (2002). "V Полиморфизм, глава 23. Универсальные типы, глава 25. Реализация системы F на ML". Типы и языки программирования. MIT Press. С. 339–362, 381–388. ISBN  0-262-16209-1.

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

• Резюме системы F Франка Бинара.
• Система F_ω: рабочая лошадка современных компиляторов к Грег Моррисетт