WikiDer > Система F

System F

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

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

куда это переменная типа. Верхний регистр традиционно используется для обозначения функций уровня типа, в отличие от строчных букв который используется для функций уровня значений. (Надстрочный означает, что граница Икс относится к типу ; выражение после двоеточия является типом предшествующего лямбда-выражения.)

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

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

Правила набора

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

(1) (2)

куда типы, это переменная типа, а в контексте указывает, что связан. Первое правило - это правило приложения, а второе - правило абстракции.[2][3]

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

В тип определяется как:, куда это переменная типа. Это означает: - это тип всех функций, которые принимают на входе тип α и два выражения типа α и производят на выходе выражение типа α (обратите внимание, что мы рассматриваем быть правоассоциативный.)

Следующие два определения логических значений и используются, расширяя определение Церковные логические значения:

(Обратите внимание, что для указанных выше двух функций требуется три - не два - аргумента. Последние два должны быть лямбда-выражениями, но первое должно быть типом. Этот факт отражается в том, что тип этих выражений ; универсальный квантор, связывающий α, соответствует Λ, связывающему альфа в самом лямбда-выражении. Также обратите внимание, что удобное сокращение для , но это не символ самой Системы F, а скорее «метасимвол». Так же, и также являются «метасимволами», удобными сокращениями «сборок» Системы F (в Чувство Бурбаки); в противном случае, если бы такие функции могли быть названы (в Системе F), тогда не было бы необходимости в лямбда-выражающем аппарате, способном определять функции анонимно и для комбинатор с фиксированной точкой, что позволяет обойти это ограничение.)

Затем с этими двумя -термы, мы можем определить некоторые логические операторы (которые имеют тип ):

Обратите внимание, что в определениях выше, аргумент типа для , указывая, что два других параметра, которые передаются относятся к типу . Как и в церковных кодировках, нет необходимости в IFTHENELSE работать так, как можно просто использовать сырые -типированные термины как функции принятия решений. Однако, если об этом попросят:

сделаю. предикат это функция, которая возвращает -типированное значение. Самый фундаментальный предикат - это ISZERO который возвращается тогда и только тогда, когда его аргументом является Церковная цифра 0:

Структуры системы F

Система F позволяет встраивать рекурсивные конструкции естественным образом, как и в Теория типов Мартина-Лёфа. Абстрактные структуры (S) создаются с использованием конструкторы. Это функции, набранные как:

.

Рекурсивность проявляется при сам появляется в одном из типов . Если у вас есть из этих конструкторов вы можете определить тип в качестве:

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

Тип системы F, соответствующий этой структуре:. Термины этого типа представляют собой типизированную версию Церковные цифры, первые из которых:

0 :=
1 :=
2 :=
3 :=

Если мы изменим порядок каррированных аргументов (т.е. ), то цифра Чёрча для это функция, которая принимает функцию ж в качестве аргумента и возвращает th сила ж. То есть цифра Чёрча - это функция высшего порядка - принимает функцию с одним аргументом ж, и возвращает другую функцию с одним аргументом.

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

Версия Системы 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ω - это система, которая позволяет выполнять функции от типов к типам, где аргумент (и результат) может иметь любой порядок.

Обратите внимание, что хотя 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 эквивалентны и неразрешимы». Анна. Pure Appl. Логика. 98 (1–3): 111–156. Дои: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. ^ а б c d Филип Вадлер (2005) Изоморфизм Жирара-Рейнольдса (второе издание) Эдинбургский университет, Языки программирования и основы в Эдинбурге

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

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

внешняя ссылка