Система Ф

Чтобы узнать об исполнителе электронной транс-музыки, см. Ферри Корстен .

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

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

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

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

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

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

Правила набора текста

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

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

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

где $\sigma ,\tau$ являются типами, $\alpha$ является переменной типа, и $\alpha ~{\text{type}}$ в контексте указывает на то, что $\alpha$ связан. Первое правило — это правило применения, а второе — правило абстракции.

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

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

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

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

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

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

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

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

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

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

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

$\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 позволяет естественным образом встраивать рекурсивные конструкции, аналогично теории типов Мартина-Лёфа . Абстрактные структуры ( S ) создаются с помощью конструкторов . Это функции, типизированные как:

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

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

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

Например, натуральные числа можно определить как индуктивный тип данных N с помощью конструкторов.

${\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}$

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

${\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}$

Если мы изменим порядок каррированных аргументов ( т.е. $\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha$), то число Чёрча для n — это функция, которая принимает функцию f в качестве аргумента и возвращает n ^й мощность ф . Другими словами, число Чёрча является функцией более высокого порядка : оно принимает функцию с одним аргументом f и возвращает другую функцию с одним аргументом.

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

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

Результат Уэллса подразумевает, что вывод типа для системы F невозможен.Ограничение системы F, известное как « Хиндли-Милнер » или просто «HM», действительно имеет простой алгоритм вывода типа и используется для многих статически типизированных функциональных языков программирования, таких как Haskell 98 и семейство ML . Со временем, когда ограничения систем типов в стиле HM стали очевидными, языки постепенно перешли к более выразительной логике своих систем типов. GHC - компилятор Haskell, выходит за рамки HM (по состоянию на 2008 год) и использует расширенную систему F с несинтаксическим равенством типов; Функции, не относящиеся к HM, в OCaml системе типов включают GADT .

Жирара

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

Система F _ω

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

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

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

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

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

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

Обратите внимание, что хотя F _ω не накладывает никаких ограничений на порядок аргументов в этих отображениях, он ограничивает вселенную аргументов для этих отображений: они должны быть типами, а не значениями. Система F _ω не допускает отображения значений в типы ( зависимые типы ), хотя и допускает отображения значений в значения ( $\lambda$ абстракция), сопоставления типов со значениями ( $\Lambda$ абстракция) и сопоставления типов с типами ( $\lambda$ абстракция на уровне типов).

Система F _<:

Система F _<: , произносится как «F-sub», является расширением системы F с подтипом . Система F _<: имеет центральное значение для теории языков программирования с 1980-х годов. потому что ядро ​​функциональных языков программирования , как и языки семейства ML , поддерживают как параметрический полиморфизм , так и подтипирование записей , что можно выразить в System F _<: .

См. также

• Экзистенциальные типы — экзистенциально квантифицированные аналоги универсальных типов.
• Система У

Ссылки

• Жирар, Жан-Ив (1971). «Расширение интерпретации Гёделя на анализ и его применение для устранения сокращений в анализе и теории типов». Материалы Второго скандинавского логического симпозиума . Амстердам. стр. 63–92. дои : 10.1016/S0049-237X(08)70843-7 .
• Жирар, Жан-Ив (1972), Функциональная интерпретация и устранение сокращений в арифметике высшего порядка (докторская диссертация) (на французском языке), Парижский университет 7 .
• Рейнольдс, Джон (1974). К теории структуры типов (PDF) .
• Жирар, Жан-Ив; Лафон, Ив; Тейлор, Пол (1989). Доказательства и типы . Издательство Кембриджского университета. ISBN  978-0-521-37181-0 .
• Уэллс, Дж. Б. (1994). «Типизация и проверка типов в лямбда-исчислении второго порядка эквивалентны и неразрешимы». Материалы 9-го ежегодного симпозиума IEEE по логике в информатике (LICS) . стр. 176–185. дои : 10.1109/LICS.1994.316068 . ISBN  0-8186-6310-3 . Постскриптум версия

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

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

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

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