Система Ф

Типизированное лямбда-исчисление

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

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

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

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

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

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

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

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

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

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

Тип определяется как: , где — переменная типа . Это означает: является типом всех функций, которые принимают на входе тип α и два выражения типа α и производят на выходе выражение типа α (обратите внимание, что мы считаем его правоассоциативным ) . ${\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}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Результат Уэллса подразумевает, что вывод типа для системы F невозможен. Ограничение системы F, известное как « Хиндли-Милнер » или просто «HM», действительно имеет простой алгоритм вывода типа и используется для многих статически типизированных функциональных языков программирования , таких как Haskell 98 и семейство ML . Со временем, когда ограничения систем типов в стиле HM стали очевидны, языки постепенно перешли к более выразительной логике своих систем типов. GHC - компилятор Haskell, выходит за рамки HM (по состоянию на 2008 год) и использует расширенную систему 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 \lambda }$

Система F

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

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

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

Примечания

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 эквивалентны и неразрешимы». Анна. Чистое приложение. Логика . 98 (1–3): 111–156. дои : 10.1016/S0168-0072(98)00047-5 .«Проект Церкви: типизация и проверка типов в {системе {F} эквивалентны и неразрешимы». 29 сентября 2007 г. Архивировано из оригинала 29 сентября 2007 г.
6. «Система FC: ограничения и принуждения равенства». gitlab.haskell.org . Проверено 8 июля 2019 г.
7. «Примечания к выпуску OCaml 4.00.1» . ocaml.org . 05.10.2012 . Проверено 23 сентября 2019 г.
8. «Справочное руководство OCaml 4.09» . 11 сентября 2012 г. Проверено 23 сентября 2019 г.
9. Филип Уодлер (2005) Изоморфизм Жирара-Рейнольдса (второе издание) Эдинбургский университет , Языки программирования и основы в Эдинбурге
10. Карделли, Лука; Мартини, Симона; Митчелл, Джон К.; Щедров, Андре (1994). «Расширение системы F с подтипированием». Информация и вычисления, том. 9 . Северная Голландия, Амстердам. стр. 4–56. дои : 10.1006/inco.1994.1013 .
11. Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. ISBN 978-0-262-16209-8., Глава 26: Ограниченная количественная оценка

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

• Жирар, Жан-Ив (1971). «Расширение интерпретации Гёделя для анализа и его применение для устранения купюр в анализе и теории типов». Материалы Второго скандинавского логического симпозиума . Амстердам. стр. 63–92. дои : 10.1016/S0049-237X(08)70843-7.
• Жирар, Жан-Ив (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre superieur (докторская диссертация) (на французском языке), Парижский университет 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. Реализация системы F в машинном обучении». Типы и языки программирования . МТИ Пресс. стр. 339–362, 381–388. ISBN 0-262-16209-1.

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

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