Русская Википедия:Система F

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

Система F допускает конструирование термов, зависящих от типов. Технически это достигается через механизм абстрагирования терма по типу, что в результате даёт новый терм. Традиционно для такой абстракции используют символ большой лямбды <math>\Lambda</math>. Например, взяв терм <math>\lambda x^\alpha.~x</math> типа <math>\alpha\to\alpha</math> и абстрагируясь по переменной типа <math>\alpha</math>, получаем терм <math>\Lambda\alpha.~\lambda x^\alpha.~x</math>. Этот терм представляет собой функцию из типов в термы. Применяя эту функцию к различным типам, мы будем получать термы с идентичной структурой, но разными типами:

<math>(\Lambda\alpha.~\lambda x^\alpha.~x)~\texttt{Bool}\ \to_{\beta}\ \lambda x^\texttt{Bool}.~x</math> — терм типа <math>\texttt{Bool}\to\texttt{Bool}</math>;

<math>(\Lambda\alpha.~\lambda x^\alpha.~x)~\texttt{Nat}\ \to_{\beta}\ \lambda x^\texttt{Nat}.~x</math> — терм типа <math>\texttt{Nat}\to\texttt{Nat}</math>.

Видно, что терм <math>\Lambda\alpha.~\lambda x^\alpha.~x</math> обладает полиморфным поведением, то есть задаёт общий интерфейс для различных типов данных. В Системе F этому терму приписывается тип <math>\forall\alpha.~\alpha\to\alpha</math>. Квантор всеобщности в типе подчёркивает возможность подстановки вместо переменной типа <math>\alpha</math> любого допустимого типа.

Формальное описание

Синтаксис типов

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

(Переменная типа) Если <math>\alpha</math> — переменная типа, то <math>\alpha</math> — это тип;
(Стрелочный тип) Если <math>A</math> и <math>B</math> являются типами, то <math>(A\to B)</math> — это тип;
(Универсальный тип) Если <math>\alpha</math> является переменной типа, а <math>B</math> — типом, то <math>(\forall\alpha.~B)</math> — это тип.

Внешние скобки часто опускают, оператор <math>\rightarrow</math> считают правоассоциативным, а действие оператора <math>\forall</math> продолжающимся вправо насколько это возможно. Например, <math>\forall\alpha.~\forall\beta.~\alpha\to\beta\to\alpha</math> — стандартное сокращение для <math>(\forall\alpha.~(\forall\beta.~(\alpha\to(\beta\to\alpha))))</math>.

Синтаксис термов

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

(Переменная) Если <math>x</math> — переменная, то <math>x</math> — это терм;
(Абстракция) Если <math>x</math> является переменной, <math>A</math> — типом, а <math>M</math> — термом, то <math>(\lambda x^A.~M)</math> — это терм;
(Применение) Если <math>M</math> и <math>N</math> являются термами, то <math>(M~N)</math> — это терм;
(Универсальная абстракция) Если <math>\alpha</math> является переменной типа, а <math>M</math> — термом, то <math>(\Lambda \alpha.~M)</math> — это терм;
(Универсальное применение) Если <math>M</math> является термом, а <math>A</math> — типом, то <math>(M~A)</math> — это терм.

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

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

(Абстракция по Карри) Если <math>x</math> является переменной, а <math>M</math> — термом, то <math>(\lambda x.~M)</math> — это терм,

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

Правила редукции

Помимо стандартного для лямбда-исчисления правила <math>\beta</math>-редукции

<math>(\lambda a^A.~M)~N\ \to_{\beta}\ M[a:=N]</math>

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

<math>(\Lambda \alpha.~M)~A\ \to_{\beta}\ M[\alpha:=A]</math>,

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

Контексты типизации и утверждение типизации

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

<math>\Gamma=x_1\!:\!A_1,x_2\!:\!A_1,\ldots,x_n\!:\!A_n</math>

В контекст можно добавить «свежую» для этого контекста переменную: если <math>\Gamma</math> — допустимый контекст, не содержащий переменной <math>x</math>, а <math>B</math> — тип, то <math>\Gamma,x\!:\!B</math> — тоже допустимый контекст.

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

<math>\Gamma\vdash M\!:\!A</math>

Это читается следующим образом: в контексте <math>\Gamma</math> терм <math>M</math> имеет тип <math>A</math>.

Правила типизации по Чёрчу

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

(Начальное правило) Если переменная <math>x</math> присутствует с типом <math>A</math> в контексте <math>\Gamma</math>, то в этом контексте <math>x</math> имеет тип <math>A</math>. В виде правила вывода

<math>{x\!:\!A \in \Gamma}\over{\Gamma \vdash x\!:\!A }</math>

(Правило введения <math>\rightarrow</math>) Если в некотором контексте, расширенном утверждением, что <math>a</math> имеет тип <math>A</math>, терм <math>M</math> имеет тип <math>B</math>, то в упомянутом контексте (без <math>a</math>), лямбда-абстракция <math>\lambda a^A.~M</math> имеет тип <math>A \to B</math>. В виде правила вывода

<math>{\Gamma,a\!:\!A\vdash M\!:\!B}\over{\Gamma\vdash (\lambda a^A.~M)\!:\!(A \to B)}</math>

(Правило удаления <math>\rightarrow</math>) Если в некотором контексте терм <math>M</math> имеет тип <math>A \to B</math>, а терм <math>N</math> имеет тип <math>A</math>, то применение <math>M~N</math> имеет тип <math>B</math>. В виде правила вывода

<math>{\Gamma\vdash M\!:\!(A \to B)\quad\Gamma\vdash N\!:\!A}\over{\Gamma\vdash (M~N)\!:\!B}</math>

(Правило введения <math>\forall</math>) Если в некотором контексте терм <math>M</math> имеет тип <math>A</math>, то в этом контексте терм <math>\Lambda \alpha.~M</math> имеет тип <math>\forall\alpha.~A</math>. В виде правила вывода

<math>{\Gamma\vdash M\!:\!A}\over{\Gamma\vdash (\Lambda \alpha.~M)\!:\!(\forall\alpha.~A)}</math>

Это правило требует оговорки: переменная типа <math>\alpha</math> не должна встречаться в утверждениях типизации контекста <math>\Gamma</math>.

(Правило удаления <math>\forall</math>) Если в некотором контексте терм <math>M</math> имеет тип <math>\forall\alpha.~A</math>, и <math>B</math> — это тип, то в этом контексте терм <math>M~B</math> имеет тип <math>A[\alpha:=B]</math>. В виде правила вывода

<math>{\Gamma\vdash M\!:\!(\forall\alpha.~A)}\over{\Gamma\vdash (M~B)\!:\!(A[\alpha:=B])}</math>

Правила типизации по Карри

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

(Начальное правило) Если переменная <math>x</math> присутствует с типом <math>A</math> в контексте <math>\Gamma</math>, то в этом контексте <math>x</math> имеет тип <math>A</math>. В виде правила вывода

<math>{x\!:\!A \in \Gamma}\over{\Gamma \vdash x\!:\!A }</math>

(Правило введения <math>\rightarrow</math>) Если в некотором контексте, расширенном утверждением, что <math>a</math> имеет тип <math>A</math>, терм <math>M</math> имеет тип <math>B</math>, то в упомянутом контексте (без <math>a</math>), лямбда-абстракция <math>\lambda a.~M</math> имеет тип <math>A \to B</math>. В виде правила вывода

<math>{\Gamma,a\!:\!A\vdash M\!:\!B}\over{\Gamma\vdash (\lambda a.~M)\!:\!(A \to B)}</math>

(Правило удаления <math>\rightarrow</math>) Если в некотором контексте терм <math>M</math> имеет тип <math>A \to B</math>, а терм <math>N</math> имеет тип <math>A</math>, то применение <math>M~N</math> имеет тип <math>B</math>. В виде правила вывода

<math>{\Gamma\vdash M\!:\!(A \to B)\quad\Gamma\vdash N\!:\!A}\over{\Gamma\vdash (M~N)\!:\!B}</math>

(Правило введения <math>\forall</math>) Если в некотором контексте терм <math>M</math> имеет тип <math>A</math>, то в этом контексте этому терму <math>M</math> может быть приписан и тип <math>\forall\alpha.~A</math>. В виде правила вывода

<math>{\Gamma\vdash M\!:\!A}\over{\Gamma\vdash M\!:\!(\forall\alpha.~A)}</math>

Это правило требует оговорки: переменная типа <math>\alpha</math> не должна встречаться в утверждениях типизации контекста <math>\Gamma</math>.

(Правило удаления <math>\forall</math>) Если в некотором контексте терм <math>M</math> имеет тип <math>\forall\alpha.~A</math>, и <math>B</math> — это тип, то в этом контексте этому терму <math>M</math> может быть приписан и тип <math>A[\alpha:=B]</math>. В виде правила вывода

<math>{\Gamma\vdash M\!:\!(\forall\alpha.~A)}\over{\Gamma\vdash M\!:\!(A[\alpha:=B])}</math>

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

<math>x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash x\!:\!(\forall\alpha.~\alpha\to\alpha)</math>

Применим правило удаления <math>\forall</math>, взяв в качестве <math>B</math> тип <math>\forall\alpha.~\alpha\to\alpha</math>

<math>x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash x\!:\!(\forall\alpha.~\alpha\to\alpha)\to(\forall\alpha.~\alpha\to\alpha)</math>

Теперь по правилу удаления <math>\rightarrow</math> имеем возможность применить терм <math>x</math> сам к себе

<math>x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash (x~x)\!:\!(\forall\alpha.~\alpha\to\alpha)</math>

и, наконец, по правилу введения <math>\rightarrow</math>

<math>\vdash (\lambda x.~x~x)\!:\!(\forall\alpha.~\alpha\to\alpha)\to(\forall\alpha.~\alpha\to\alpha)</math>

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

Представление типов данных

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

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

<math>\bot\ \equiv\ \forall\alpha.~\alpha</math>

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

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

<math>\top\ \equiv\ \forall\alpha.~\alpha\to\alpha</math>

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

<math>\mathtt{id}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~x</math>.

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

<math>\mathtt{Bool}\ \equiv\ \forall\alpha.~\alpha\to\alpha\to\alpha</math>.

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

<math>\mathtt{true}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~\lambda y^\alpha.~x</math>

<math>\mathtt{false}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~\lambda y^\alpha.~y</math>

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

<math>\mathtt{ifThenElse} \ \equiv\ \Lambda\alpha.~\lambda b^{\mathtt{Bool}}.~\lambda x^\alpha.~\lambda y^\alpha.~b\,\alpha\,x\,y </math>

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

<math>\mathtt{ifThenElse}\,A\,\mathtt{true}\,M\,N=M</math>

и

<math>\mathtt{ifThenElse}\,A\,\mathtt{false}\,M\,N=N</math>

для произвольного типа <math>A</math> и произвольных <math>M\!:\!A</math> и <math>N\!:\!A</math>. В этом легко убедиться, раскрыв определения и выполнив <math>\beta</math>-редукции.

Тип произведения. Для произвольных типов <math>A</math> и <math>B</math> тип их декартова произведения

<math>A\times B~\equiv~\forall\alpha.~(A\to B\to\alpha)\to\alpha</math>

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

<math>\langle M;N\rangle~\equiv~\Lambda\alpha.~\lambda f^{(A\to B\to\alpha)}.~f~M~N</math>

для каждых <math>M\!:\!A</math> и <math>N\!:\!B</math>. Проекции пары задаются функциями

<math>\mathtt{fst}\ \equiv\ \Lambda\alpha.~\Lambda\beta.~\lambda p^{\alpha\times\beta}.~p\,\alpha\,(\lambda x^\alpha.\,\lambda y^\beta.\,x)~:~\forall\alpha.~\forall\beta.\,\alpha\times\beta\to\alpha</math>

<math>\mathtt{snd}\ \equiv\ \Lambda\alpha.~\Lambda\beta.~\lambda p^{\alpha\times\beta}.~p\,\beta\,(\lambda x^\alpha.\,\lambda y^\beta.\,y)~:~\forall\alpha.~\forall\beta.\,\alpha\times\beta\to\beta</math>

Эти функции удовлетворяют естественным требованиям <math>\mathtt{fst}\,A\,B\,\langle M;N\rangle=M</math> и <math>\mathtt{snd}\,A\,B\,\langle M;N\rangle=N</math>.

Тип суммы. Для произвольных типов <math>A</math> и <math>B</math> тип их суммы

<math>A+B~\equiv~\forall\alpha.~(A\to\alpha)\to(B\to\alpha)\to\alpha</math>

населён либо термом типа <math>A</math>, либо термом типа <math>B</math>, в зависимости от применённого конструктора

<math>\mathtt{injL}\,M~\equiv~\Lambda\alpha.\,\lambda f^{A\to\alpha}.\,\lambda g^{B\to\alpha}.\,f\,M</math>

<math>\mathtt{injR}\,N~\equiv~\Lambda\alpha.\,\lambda f^{A\to\alpha}.\,\lambda g^{B\to\alpha}.\,g\,N</math>

Здесь <math>M\!:\!A</math>, <math>N\!:\!B</math>. Функция, осуществляющая разбор случаев (сопоставление с образцом), имеет вид

<math>\mathtt{match}~\equiv~\Lambda\alpha.\,\Lambda\beta.\,\Lambda\gamma.\,\lambda s^{\alpha+\beta}.\,\lambda f^{\alpha\to\gamma}.\,\lambda g^{\beta\to\gamma}.\,s\, \gamma\,f\,g~:~\forall\alpha.~\forall\beta.~\forall\gamma.~\alpha+\beta\to(\alpha\to \gamma)\to(\beta\to \gamma)\to \gamma</math>

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

<math>\mathtt{match}\,A\,B\,C\,(\mathtt{injL}\,M)\,F\,G=F\,M</math>

и

<math>\mathtt{match}\,A\,B\,C\,(\mathtt{injR}\,N)\,F\,G=G\,N</math>

для произвольных типов <math>A</math>, <math>B</math> и <math>C</math> и произвольных термов <math>F\!:\!A\to C</math> и <math>G\!:\!B\to C</math>.

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

<math>\mathtt{Nat}\ \equiv\ \forall\alpha.~\alpha\to(\alpha\to\alpha)\to\alpha</math>

населён бесконечным количеством различных элементов, получаемых посредством двух конструкторов <math>\mathtt{zero}\!:\!\mathtt{Nat}</math> и <math>\mathtt{succ}\!:\!\mathtt{Nat}\to \mathtt{Nat}</math>:

<math>\mathtt{zero}\ \equiv\ \Lambda\alpha.\,\lambda z^{\alpha}.\,\lambda s^{\alpha\to\alpha}.\,z</math>

<math>\mathtt{succ}\ \equiv\ \lambda n^{\mathtt{Nat}} .\,\Lambda \alpha.\,\lambda z^{\alpha}.\,\lambda s^{\alpha\to\alpha} .\,s\,(n\,\alpha\,z\,s)</math>

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

<math>\overline{n}\ \equiv\ \Lambda\alpha.\,\lambda z^{\alpha}.\,\lambda s^{\alpha\rightarrow\alpha}.\,\underbrace{s(s(s \ldots (s}_{n} \,z) \ldots ))</math>

Свойства

Просто типизированная система обладает свойством типовой безопасности: при <math>\beta</math>-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.

В своей диссертации Жан-Ив Жирар показал^[1], что Система F обладает свойством сильной нормализации: любой допустимый терм за конечное число <math>\beta</math>-редукций приводится к единственной нормальной форме.

Система F является en (Impredicativity) системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм <math>\texttt{id}</math> единичного типа <math>\top\equiv\forall\alpha.~\alpha\to\alpha</math> может быть применён к собственному типу, порождая терм типа <math>\top\to\top</math>. Как показал Джо Уэллс в 1994 году^[3], задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.

Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской en (Second-order propositional logic), формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения <math>\top</math> (истина), <math>\bot</math> (ложь), связки <math>\lnot</math> (отрицание), <math>\land</math> (конъюнкция) и <math>\lor</math> (дизъюнкция), а также <math>\exists</math> (квантор существования) могут быть определены так

<math>\top~\equiv~\forall\alpha.\,\alpha\to\alpha</math>

<math>\bot~\equiv~\forall\alpha.\,\alpha</math>

<math>\lnot A~\equiv~A\to\bot</math>

<math>A\land B~\equiv~\forall\alpha.\,(A\to B\to\alpha)\to\alpha</math>

<math>A\lor B~\equiv~\forall\alpha.\,(A\to\alpha)\to(B\to\alpha)\to\alpha</math>

<math>\exists\alpha.\,M[\alpha]~\equiv~\forall\gamma.\,(\forall\alpha.\,M[\alpha]\to\gamma)\to\gamma</math>

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

Примечания

Шаблон:Примечания

Литература

Шаблон:Книга
- Перевод на русский язык: Шаблон:Книга
Шаблон:Статья
Шаблон:Книга

↑ ^1,0 ^1,1 Ошибка цитирования Неверный тег <ref>; для сносок Girard72 не указан текст
↑ Ошибка цитирования Неверный тег <ref>; для сносок Reynolds74 не указан текст
↑ Ошибка цитирования Неверный тег <ref>; для сносок Wells94 не указан текст

[Girard72-1] 1,0 ^1,1 Ошибка цитирования Неверный тег <ref>; для сносок Girard72 не указан текст

[Reynolds74-2] Ошибка цитирования Неверный тег <ref>; для сносок Reynolds74 не указан текст

[Wells94-3] Ошибка цитирования Неверный тег <ref>; для сносок Wells94 не указан текст

[1]

[2]

[3]

Партнерские ресурсы
Криптовалюты	Обмен криптовалют - www.bestchange.ru Криптовалютная биржа CoinEx Криптовалютная биржа Binance HIVE OS - операционная система для майнинга e4pool - Мультивалютный пул для майнинга.
Магазины	AliExpress — глобальная виртуальная (в Интернете) торговая площадка, предоставляющая возможность покупать товары производителей из КНР; computeruniverse.net - Интернет-магазин компьютеров(Промо код 5 Евро на первую покупку:FWWC3ZKQ);
Хостинг	DigitalOcean - американский провайдер облачных инфраструктур, с главным офисом в Нью-Йорке и с центрами обработки данных по всему миру;
Разное	Викиум - Онлайн-тренажер для мозга Like Центр - Центр поддержки и развития предпринимательства. Gamersbay - лучший магазин по бустингу для World of Warcraft. Ноотропы OmniMind N°1 - Усиливает мозговую активность. Повышает мотивацию. Улучшает память. Санкт-Петербургская школа телевидения - это федеральная сеть образовательных центров, которая имеет филиалы в 37 городах России. Lingualeo.com — интерактивный онлайн-сервис для изучения и практики английского языка в увлекательной игровой форме. Junyschool (Джунискул) – международная школа программирования и дизайна для детей и подростков от 5 до 17 лет, где ученики осваивают компьютерную грамотность, развивают алгоритмическое и креативное мышление, изучают основы программирования и компьютерной графики, создают собственные проекты: игры, сайты, программы, приложения, анимации, 3D-модели, монтируют видео. Умназия - Интерактивные онлайн-курсы и тренажеры для развития мышления детей 6-13 лет SkillBox - это один из лидеров российского рынка онлайн-образования. Среди партнеров Skillbox ведущий разработчик сервисного дизайна AIC, медиа-компания Yoola, первое и самое крупное русскоязычное аналитическое агентство Tagline, онлайн-школа дизайна и иллюстрации Bang! Bang! Education, оператор PR-рынка PACO, студия рисования Draw&Go, агентство performance-маркетинга Ingate, scrum-студия Sibirix, имидж-лаборатория Персона. «Нетология» — это университет по подготовке и дополнительному обучению специалистов в области интернет-маркетинга, управления проектами и продуктами, дизайна, Data Science и разработки. В рамках Нетологии студенты получают ценные теоретические знания от лучших экспертов Рунета, выполняют практические задания на отработку полученных навыков, общаются с экспертами и единомышленниками. Познакомиться со всеми продуктами подробнее можно на сайте https://netology.ru, линейка курсов и профессий постоянно обновляется. StudyBay Brazil – это онлайн биржа для португалоговорящих студентов и авторов! Студент получает уникальную работу любого уровня сложности и больше свободного времени, в то время как у автора появляется дополнительный заработок и бесценный опыт. Автор24 — самая большая в России площадка по написанию учебных работ: контрольные и курсовые работы, дипломы, рефераты, решение задач, отчеты по практике, а так же любой другой вид работы. Сервис сотрудничает с более 70 000 авторов. Более 1 000 000 работ уже выполнено. StudyBay – это онлайн биржа для англоязычных студентов и авторов! Студент получает уникальную работу любого уровня сложности и больше свободного времени, в то время как у автора появляется дополнительный заработок и бесценный опыт.