Открыть главное меню

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

ЛитератураПравить