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

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

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

⊢ Λ α . λ х α . х : ∀ α . α → α {\displaystyle \vdash \Lambda \alpha.\lambda x^{\alpha}.x:\forall \alpha.\alpha \to \alpha }

где — переменная типа . Верхний регистр традиционно используется для обозначения функций уровня типа, в отличие от нижнего регистра , который используется для функций уровня значения. (Верхний индекс означает, что граница x имеет тип ; выражение после двоеточия — это тип лямбда-выражения, предшествующего ему.) α {\displaystyle \альфа} Λ {\displaystyle \Лямбда} λ {\displaystyle \лямбда} α {\displaystyle \альфа} α {\displaystyle \альфа}

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

По словам Жирара, буква «F» в аббревиатуре System 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 \сигма ,\тау } α {\displaystyle \альфа} α   тип {\displaystyle \альфа ~{\text{тип}}} α {\displaystyle \альфа}

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

Тип определяется как: , где — переменная типа . Это означает: — тип всех функций, которые принимают на входе тип α и два выражения типа α, и производят на выходе выражение типа α (обратите внимание, что мы считаем его правоассоциативным . ) Б о о л е а н {\displaystyle {\mathsf {Булево значение}}} ∀ α . α → α → α {\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha } α {\displaystyle \альфа} Б о о л е а н {\displaystyle {\mathsf {Булево значение}}} → {\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 {Булево значение}}} ∀ α . α → α → α {\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha } Т {\displaystyle \mathbf {T} } Ф {\displaystyle \mathbf {F} }

Затем с помощью этих двух -термов мы можем определить некоторые логические операторы (которые имеют тип ): λ {\displaystyle \лямбда} Б о о л е а н → Б о о л е а н → Б о о л е а н {\displaystyle {\mathsf {Булевое значение}}\rightarrow {\mathsf {Булевое значение}}\rightarrow {\mathsf {Булевое значение}}}

А Н Д = λ х Б о о л е а н λ у Б о о л е а н . х Б о о л е а н у Ф О Р = λ х Б о о л е а н λ у Б о о л е а н . х Б о о л е а н Т у Н О Т = λ х Б о о л е а н . х Б о о л е а н Ф Т {\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 {Булево значение}}} х {\displaystyle x} х {\displaystyle x} Б о о л е а н {\displaystyle {\mathsf {Булево значение}}} Б о о л е а н {\displaystyle {\mathsf {Булево значение}}}

я Ф Т ЧАС Э Н Э Л С Э = Λ α . λ х Б о о л е а н λ у α λ з α . х α у з {\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}

будет делать. Предикат — это функция, которая возвращает типизированное значение. Самый фундаментальный предикат — ISZERO , который возвращает значение только в том случае, если его аргумент — это число Чёрча 0 : Б о о л е а н {\displaystyle {\mathsf {Булево значение}}} Т {\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 ) создаются с помощью конструкторов . Это функции, типизированные как:

K 1 → K 2 → ⋯ → S {\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S} .

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

∀ α . ( K 1 1 [ α / S ] → ⋯ → α ) ⋯ → ( K 1 m [ α / 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 }

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

z e r o : N s u c c : N → 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 }

0 := Λ α . λ x α . λ f α → α . x 1 := Λ α . λ x α . λ f α → α . f x 2 := Λ α . λ x α . λ f α → α . f ( f x ) 3 := Λ α . λ x α . λ f α → α . f ( f ( f x ) ) {\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 }

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

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

Результат Уэллса подразумевает, что вывод типа для System F невозможен. Ограничение System 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 {\displaystyle F_{n}} Виды разрешений:
    • ⋆ {\displaystyle \star } (вид типов) и
    • J ⇒ K {\displaystyle J\Rightarrow K} где и (вид функций из типов в типы, где тип аргумента имеет низший порядок) J ∈ F n − 1 {\displaystyle J\in F_{n-1}} K ∈ F n {\displaystyle K\in F_{n}}

В пределе мы можем определить систему как F ω {\displaystyle F_{\omega }}

  • F ω = ⋃ 1 ≤ i F i {\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. doi :10.1016/0304-3975(86)90044-7. Однако в [3] было показано, что очевидные правила преобразования для этой системы, названной F случайно, сходятся.
  2. ^ Харпер Р. «Практические основы языков программирования, второе издание» (PDF) . стр.  142–3 .
  3. ^ Гейверс Х., Нордстрём Б., Довек Г. «Доказательства программ и формализация математики» (PDF) . стр. 51.
  4. ^ Уэллс, Дж. Б. (2005-01-20). «Исследовательские интересы Джо Уэллса». Университет Хериот-Уотт.
  5. ^ Уэллс, Дж. Б. (1999). «Типичность и проверка типов в системе F эквивалентны и неразрешимы». Ann. Pure Appl. Logic . 98 ( 1– 3): 111– 156. doi : 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. ^ abcd Филип Вадлер (2005) Изоморфизм Жирара-Рейнольдса (второе издание) Эдинбургский университет , Языки программирования и основы в Эдинбурге
  10. ^ Карделли, Лука; Мартини, Симоне; Митчелл, Джон К.; Скедров, Андре (1994). «Расширение системы F с подтипированием». Информация и вычисления, т. 9. Северная Голландия, Амстердам. стр.  4–56 . doi : 10.1006/inco.1994.1013 .
  11. ^ Пирс, Бенджамин (2002). Типы и языки программирования . MIT Press. ISBN 978-0-262-16209-8., Глава 26: Ограниченная квантификация

Ссылки

  • Жирар, Жан-Ив (1971). «Расширение интерпретации Гёделя для анализа и его применение для устранения купюр в анализе и теории типов». Материалы Второго скандинавского логического симпозиума . Амстердам. стр.  63–92 . doi :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). Доказательства и шрифты. Cambridge University Press. ISBN 978-0-521-37181-0.
  • Уэллс, Дж. Б. (1994). «Типичность и проверка типов в лямбда-исчислении второго порядка эквивалентны и неразрешимы». Труды 9-го ежегодного симпозиума IEEE по логике в компьютерных науках (LICS) . стр.  176–185 . doi :10.1109/LICS.1994.316068. ISBN 0-8186-6310-3.Постскриптум версия

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

  • Пирс, Бенджамин (2002). "V Полиморфизм Гл. 23. Универсальные типы, Гл. 25. Реализация системы F на языке ML". Типы и языки программирования . MIT Press. С.  339– 362, 381– 388. ISBN 0-262-16209-1.
В Wikibooks есть книга по теме: Haskell
  • Краткое изложение Системы F Франка Бинарда.
  • Система Fω: рабочая лошадка современных компиляторов Грега Моррисетта
Retrieved from "https://en.wikipedia.org/w/index.php?title=System_F&oldid=1258607987"