Система F

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Система F допускает конструирование термов, зависящих от типов. Технически это достигается через механизм абстрагирования терма по типу, что в результате даёт новый терм. Традиционно для такой абстракции используют символ большой лямбды . Например, взяв терм типа и абстрагируясь по переменной типа , получаем терм . Этот терм представляет собой функцию из типов в термы. Применяя эту функцию к различным типам, мы будем получать термы с идентичной структурой, но разными типами:

— терм типа ;
— терм типа .

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

Формальное описание[править | править вики-текст]

Синтаксис типов[править | править вики-текст]

Типы Системы F конструируются из набора переменных типа с помощью операторов и . По традиции для переменных типа используют греческие буквы. Правила формирования типов таковы:

  • (Переменная типа) Если — переменная типа, то — это тип;
  • (Стрелочный тип) Если и являются типами, то — это тип;
  • (Универсальный тип) Если является переменной типа, а — типом, то — это тип.

Внешние скобки часто опускают, оператор считают правоассоциативным, а действие оператора продолжающимся вправо насколько это возможно. Например, — стандартное сокращение для .

Синтаксис термов[править | править вики-текст]

Термы Системы F конструируются из набора термовых переменных (, , и т.д.) по следующим правилам

  • (Переменная) Если — переменная, то — это терм;
  • (Абстракция) Если является переменной, — типом, а — термом, то — это терм;
  • (Применение) Если и являются термами, то — это терм;
  • (Универсальная абстракция) Если является переменной типа, а — термом, то — это терм;
  • (Универсальное применение) Если является термом, а — типом, то — это терм.

Внешние скобки часто опускают, оба сорта применения считают левоассоциативными, а действие абстракций — продолжающимся вправо насколько это возможно.

Различают две версии просто типизированной системы. Если, как в приведённых выше правилах, термовые переменные в лямбда-абстракции аннотируются типами, то систему называют типизированной по Чёрчу. Если же правило абстракции заменить на

  • (Абстракция по Карри) Если является переменной, а — термом, то — это терм,

и отбросить два последних правила, то систему называют типизированной по Карри. Фактически, термы системы, типизированной по Карри, те же, что и в бестиповом лямбда-исчислении.

Правила редукции[править | править вики-текст]

Помимо стандартного для лямбда-исчисления правила -редукции

в системе F в стиле Чёрча вводится дополнительное правило,

,

позволяющее вычислять применение терма к типу через механизм подстановки типа вместо переменной типа.

Контексты типизации и утверждение типизации[править | править вики-текст]

Контекстом, как и в просто типизированном лямбда-исчислении, называется множество утверждений о приписывании типов различным переменным, разделённых запятой

В контекст можно добавить «свежую» для этого контекста переменную: если — допустимый контекст, не содержащий переменной , а — тип, то — тоже допустимый контекст.

Общий вид утверждения о типизации таков:

Это читается следующим образом: в контексте терм имеет тип .

Правила типизации по Чёрчу[править | править вики-текст]

В Системе F, типизированной по Чёрчу, приписывание типов термам осуществляется в соответствии со следующими правилами:

(Начальное правило) Если переменная присутствует с типом в контексте , то в этом контексте имеет тип . В виде правила вывода

(Правило введения ) Если в некотором контексте, расширенном утверждением, что имеет тип , терм имеет тип , то в упомянутом контексте (без ), лямбда-абстракция имеет тип . В виде правила вывода

(Правило удаления ) Если в некотором контексте терм имеет тип , а терм имеет тип , то применение имеет тип . В виде правила вывода

(Правило введения ) Если в некотором контексте терм имеет тип , то в этом контексте терм имеет тип . В виде правила вывода

Это правило требует оговорки: переменная типа не должна встречаться в утверждениях типизации контекста .

(Правило удаления ) Если в некотором контексте терм имеет тип , и — это тип, то в этом контексте терм имеет тип . В виде правила вывода

Правила типизации по Карри[править | править вики-текст]

В Системе F, типизированной по Карри, приписывание типов термам осуществляется в соответствии со следующими правилами:

(Начальное правило) Если переменная присутствует с типом в контексте , то в этом контексте имеет тип . В виде правила вывода

(Правило введения ) Если в некотором контексте, расширенном утверждением, что имеет тип , терм имеет тип , то в упомянутом контексте (без ), лямбда-абстракция имеет тип . В виде правила вывода

(Правило удаления ) Если в некотором контексте терм имеет тип , а терм имеет тип , то применение имеет тип . В виде правила вывода

(Правило введения ) Если в некотором контексте терм имеет тип , то в этом контексте этому терму может быть приписан и тип . В виде правила вывода

Это правило требует оговорки: переменная типа не должна встречаться в утверждениях типизации контекста .

(Правило удаления ) Если в некотором контексте терм имеет тип , и — это тип, то в этом контексте этому терму может быть приписан и тип . В виде правила вывода

Пример. По начальному правилу:

Применим правило удаления , взяв в качестве тип

Теперь по правилу удаления имеем возможность применить терм сам к себе

и, наконец, по правилу введения

Это пример терма, типизируемого в Системе F, но не в просто типизированной системе.

Представление типов данных[править | править вики-текст]

Система F обладает достаточными выразительными средствами, для того чтобы напрямую реализовать многие типы данных, используемые в языках программирования. Будем работать в версии Чёрча системы F.

Пустой тип. Тип

необитаем в системе F, то есть в ней отсутствуют термы с таким типом.

Единичный тип. У типа

в системе F имеется единственный находящийся в нормальной форме обитатель — терм

.

Булев тип. В системе F задается так:

.

У этого типа ровно два обитателя, отождествляемых с двумя булевыми константами

Конструкция условного оператора

Эта функция удовлетворяет естественным требованиям

и

для произвольного типа и произвольных и . В этом легко убедиться, раскрыв определения и выполнив -редукции.

Тип произведения. Для произвольных типов и тип их декартова произведения

населён парой

для каждых и . Проекции пары задаются функциями

Эти функции удовлетворяют естественным требованиям и .

Тип суммы. Для произвольных типов и тип их суммы

населён либо термом типа , либо термом типа , в зависимости от применённого конструктора

Здесь , . Функция, осуществляющая разбор случаев (сопоставление с образцом), имеет вид

Эта функция удовлетворяет следующим естественным требованиям

и

для произвольных типов , и и произвольных термов и .

Числа Чёрча. Тип натуральных чисел в системе F

населён бесконечным количеством различных элементов, получаемых посредством двух конструкторов и :

Натуральное число может быть получено -кратным применением второго конструктора к первому или, эквивалентно, представлено термом

Свойства[править | править вики-текст]

  • Просто типизированная система обладает свойством типовой безопасности: при -редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
  • В своей диссертации Жан-Ив Жирар показал[1], что Система F обладает свойством сильной нормализации: любой допустимый терм за конечное число -редукций приводится к единственной нормальной форме.
  • Система F является импредикативной (англ.) системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм единичного типа может быть применён к собственному типу, порождая терм типа . Как показал Джо Уэллс в 1994 году[3], задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.
  • Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской логикой высказываний второго порядка (англ.), формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения (истина), (ложь), связки (отрицание), (конъюнкция) и (дизъюнкция), а также (квантор существования) могут быть определены так

Отметим, что соответствие Карри — Ховарда ставит в соответствие истине — единичный тип, лжи — пустой тип, конъюнкции — произведение типов, а дизъюнкции — их сумму.

Примечания[править | править вики-текст]

  1. 1 2 Girard, Jean-Yves Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur : Ph.D. thesis. — Université Paris 7, 1972.
  2. John C. Reynolds Towards a Theory of Type Structure. — 1974.
  3. Wells J. B. Typability and type checking in the second-order lambda-calculus are equivalent and undecidable // Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). — 1994. — С. 176–185.

Литература[править | править вики-текст]