Система F

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\Gamma=x_1\!:\!A_1,x_2\!:\!A_1,\ldots,x_n\!:\!A_n

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

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

\Gamma\vdash M\!:\!A

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

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

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

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

{x\!:\!A \in \Gamma}\over{\Gamma \vdash x\!:\!A }

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

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

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

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

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

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

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

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

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

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

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

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

{x\!:\!A \in \Gamma}\over{\Gamma \vdash x\!:\!A }

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

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

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

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

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

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

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

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

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

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

x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash x\!:\!(\forall\alpha.~\alpha\to\alpha)

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

x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash x\!:\!(\forall\alpha.~\alpha\to\alpha)\to(\forall\alpha.~\alpha\to\alpha)

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

x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash (x~x)\!:\!(\forall\alpha.~\alpha\to\alpha)

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

\vdash (\lambda x.~x~x)\!:\!(\forall\alpha.~\alpha\to\alpha)\to(\forall\alpha.~\alpha\to\alpha)

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

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

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

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

\bot\ \equiv\ \forall\alpha.~\alpha

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

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

\top\ \equiv\ \forall\alpha.~\alpha\to\alpha

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

\mathtt{id}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~x.

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

\mathtt{Bool}\ \equiv\ \forall\alpha.~\alpha\to\alpha\to\alpha.

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

\mathtt{true}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~\lambda y^\alpha.~x
\mathtt{false}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~\lambda y^\alpha.~y

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

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

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

\mathtt{ifThenElse}\,A\,\mathtt{true}\,M\,N=M

и

\mathtt{ifThenElse}\,A\,\mathtt{false}\,M\,N=N

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

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

A\times B~\equiv~\forall\alpha.~(A\to B\to\alpha)\to\alpha

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

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

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

\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
\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

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

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

A+B~\equiv~\forall\alpha.~(A\to\alpha)\to(B\to\alpha)\to\alpha

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

\mathtt{injL}\,M~\equiv~\Lambda\alpha.\,\lambda f^{A\to\alpha}.\,\lambda g^{B\to\alpha}.\,f\,M
\mathtt{injR}\,N~\equiv~\Lambda\alpha.\,\lambda f^{A\to\alpha}.\,\lambda g^{B\to\alpha}.\,g\,N

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

\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

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

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

и

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

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

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

\mathtt{Nat}\ \equiv\ \forall\alpha.~\alpha\to(\alpha\to\alpha)\to\alpha

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

\mathtt{zero}\ \equiv\ \Lambda\alpha.\,\lambda z^{\alpha}.\,\lambda s^{\alpha\to\alpha}.\,z
\mathtt{succ}\ \equiv\ \lambda n^{\mathtt{Nat}} .\,\Lambda \alpha.\,\lambda z^{\alpha}.\,\lambda s^{\alpha\to\alpha} .\,s\,(n\,\alpha\,z\,s)

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

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

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

  • Просто типизированная система обладает свойством типовой безопасности: при \beta-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
  • В своей диссертации Жан-Ив Жирар показал[1], что Система F обладает свойством сильной нормализации: любой допустимый терм за конечное число \beta-редукций приводится к единственной нормальной форме.
  • Система F является импредикативной (англ.) системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм \texttt{id} единичного типа \top\equiv\forall\alpha.~\alpha\to\alpha может быть применён к собственному типу, порождая терм типа \top\to\top. Как показал Джо Уэллс в 1994 году[3], задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.
  • Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской логикой высказываний второго порядка (англ.), формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения \top (истина), \bot (ложь), связки \lnot (отрицание), \land (конъюнкция) и \lor (дизъюнкция), а также \exists (квантор существования) могут быть определены так
\top~\equiv~\forall\alpha.\,\alpha\to\alpha
\bot~\equiv~\forall\alpha.\,\alpha
\lnot A~\equiv~A\to\bot
A\land B~\equiv~\forall\alpha.\,(A\to B\to\alpha)\to\alpha
A\lor B~\equiv~\forall\alpha.\,(A\to\alpha)\to(B\to\alpha)\to\alpha
\exists\alpha.\,M[\alpha]~\equiv~\forall\gamma.\,(\forall\alpha.\,M[\alpha]\to\gamma)\to\gamma

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

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

  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.

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