Система 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}$

где - переменная типа . Верхний регистр традиционно используется для обозначения функций уровня типа, в отличие от нижнего регистра, который используется для функций уровня значений. (Верхний индекс означает, что привязка x относится к типу ; выражение после двоеточия - это тип предшествующего ему лямбда-выражения.)${\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)

где являются типами, является переменной типа и в контексте указывает, что она связана. Первое правило - это правило приложения, а второе - правило абстракции.^{[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 (в смысле Бурбаки${\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} }$); в противном случае, если бы такие функции могли быть названы (в Системе 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}$

Сделаю. Предикат является функцией , которая возвращает -typed значения. Самый фундаментальный предикат - 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}$.

Рекурсивность проявляется, когда сама появляется внутри одного из типов . Если у вас есть из этих конструкторов, вы можете определить тип как:${\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} }$

Тип System 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))}$

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

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

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

Результат Уэллса означает, что вывод типа для Системы F невозможен. Ограничение Системы F, известное как « Hindley – Milner » или просто «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 \lambda }$

См. Также [ править ]

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

Примечания [ править ]

Ссылки [ править ]

Дальнейшее чтение [ править ]

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

Внешние ссылки [ править ]

В Викиучебнике есть книга по теме: Haskell

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