Система Ф

Система 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 была выбрана случайно. ^[1]

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

Правила типизации Системы 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$ связан. Первое правило — это правило применения, а второе — правило абстракции. ^[2]^[3]

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

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

Система 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 в стиле Карри, то есть такого, в котором отсутствуют явные аннотации типизации. ^[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 _ω можно определить индуктивно на семействе систем, где индукция основана на видах, разрешенных в каждой системе:

$F_{n}$ $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 _<: . ^[10]^[11]

См. также

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

Примечания

^ Жирар, Жан-Ив (1986). «Система F типов переменных, пятнадцать лет спустя». Теоретическая информатика . 45 : 160. дои : 10.1016/0304-3975(86)90044-7 . Однако в [3] было показано, что очевидные правила преобразования для этой системы, названной случайно F, являются сходящимися.
^ Харпер Р. «Практические основы языков программирования, второе издание» (PDF) . стр. 142–3.
^ Геверс Х., Нордстрем Б., Довек Г. «Доказательства программ и формализация математики» (PDF) . п. 51.
^ Уэллс, Дж. Б. (20 января 2005 г.). «Исследовательские интересы Джо Уэллса» . Университет Хериот-Ватт.
^ Уэллс, Дж. Б. (1999). «Типизация и проверка типов в Системе F эквивалентны и неразрешимы» . Энн. Чистое приложение. Логика . 98 (1–3): 111–156. дои : 10.1016/S0168-0072(98)00047-5 . «Проект Черча: типизация и проверка типов в {системе {F} эквивалентны и неразрешимы» . 29 сентября 2007 г. Архивировано из оригинала 29 сентября 2007 г.
^ «Система FC: ограничения равенства и принуждения» . gitlab.haskell.org . Проверено 8 июля 2019 г.
^ «Примечания к выпуску OCaml 4.00.1» . ocaml.org . 05.10.2012 . Проверено 23 сентября 2019 г.
^ «Справочное руководство по OCaml 4.09» . 11 сентября 2012 г. Проверено 23 сентября 2019 г.
^ Jump up to: ^а ^б ^с ^д Филип Уодлер (2005) Изоморфизм Жирара-Рейнольдса (второе издание) Эдинбургский университет , Языки программирования и основы в Эдинбурге
^ Карделли, Лука; Мартини, Симона; Митчелл, Джон К.; Щедров, Андре (1994). «Расширение системы F с подтипированием». Информация и вычисления, том. 9 . Северная Голландия, Амстердам. стр. 4–56. дои : 10.1006/inco.1994.1013 .
^ Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. ISBN 978-0-262-16209-8 . , Глава 26: Ограниченная количественная оценка

Ссылки

Жирар, Жан-Ив (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 _ω : рабочая лошадка современных компиляторов Грега Моррисетта

[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 г.

[gr2-9] Jump up to: ^а ^б ^с ^д Филип Уодлер (2005) Изоморфизм Жирара-Рейнольдса (второе издание) Эдинбургский университет , Языки программирования и основы в Эдинбурге

[10] Карделли, Лука; Мартини, Симона; Митчелл, Джон К.; Щедров, Андре (1994). «Расширение системы F с подтипированием». Информация и вычисления, том. 9 . Северная Голландия, Амстердам. стр. 4–56. дои : 10.1006/inco.1994.1013 .

[11] Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. ISBN 978-0-262-16209-8 . , Глава 26: Ограниченная количественная оценка

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]