Меню Главная Случайная статья Настройки Система F Материал из https://ru.wikipedia.org Система F (полиморфное лямбда-исчисление, система ${\displaystyle \lambda 2}$, типизированное лямбда-исчисление второго порядка) — система типизированного лямбда-исчисления, отличающаяся от просто типизированной системы наличием механизма универсальной квантификации над типами. Эту систему разработал в 1972 году Жан-Ив Жирар [1] в контексте теории доказательств в логике. Независимо от него подобную систему предложил в 1974 году Джон Рейнольдс[2]. Система F позволяет формализовать концепцию параметрического полиморфизма в языках программирования и служит теоретической основой для таких языков программирования как Haskell и ML. Система F допускает конструирование термов, зависящих от типов. Технически это достигается через механизм абстрагирования терма по типу, что в результате даёт новый терм. Традиционно для такой абстракции используют символ большой лямбды ${\displaystyle \Lambda }$. Например, взяв терм ${\displaystyle \lambda x^{\alpha }.~x}$ типа ${\displaystyle \alpha \to \alpha }$ и абстрагируясь по переменной типа ${\displaystyle \alpha }$, получаем терм ${\displaystyle \Lambda \alpha .~\lambda x^{\alpha }.~x}$. Этот терм представляет собой функцию из типов в термы. Применяя эту функцию к различным типам, мы будем получать термы с идентичной структурой, но разными типами: ${\displaystyle (\Lambda \alpha .~\lambda x^{\alpha }.~x)~{\texttt {Bool}}\ \to _{\beta }\ \lambda x^{\texttt {Bool}}.~x}$ — терм типа ${\displaystyle {\texttt {Bool}}\to {\texttt {Bool}}}$; ${\displaystyle (\Lambda \alpha .~\lambda x^{\alpha }.~x)~{\texttt {Nat}}\ \to _{\beta }\ \lambda x^{\texttt {Nat}}.~x}$ — терм типа ${\displaystyle {\texttt {Nat}}\to {\texttt {Nat}}}$. Видно, что терм ${\displaystyle \Lambda \alpha .~\lambda x^{\alpha }.~x}$ обладает полиморфным поведением, то есть задаёт общий интерфейс для различных типов данных. В Системе F этому терму приписывается тип ${\displaystyle \forall \alpha .~\alpha \to \alpha }$. Квантор всеобщности в типе подчёркивает возможность подстановки вместо переменной типа ${\displaystyle \alpha }$ любого допустимого типа. Содержание 1 Формальное описание 1.1 Синтаксис типов 1.2 Синтаксис термов 1.3 Правила редукции 1.4 Контексты типизации и утверждение типизации 1.5 Правила типизации по Чёрчу 1.6 Правила типизации по Карри 2 Представление типов данных 3 Свойства 4 Примечания 5 Литература Формальное описание Синтаксис типов Типы Системы F конструируются из набора переменных типа с помощью операторов ${\displaystyle \to }$ и ${\displaystyle \forall }$. По традиции для переменных типа используют греческие буквы. Правила формирования типов таковы: (Переменная типа) Если ${\displaystyle \alpha }$ — переменная типа, то ${\displaystyle \alpha }$ — это тип; (Стрелочный тип) Если ${\displaystyle A}$ и ${\displaystyle B}$ являются типами, то ${\displaystyle (A\to B)}$ — это тип; (Универсальный тип) Если ${\displaystyle \alpha }$ является переменной типа, а ${\displaystyle B}$ — типом, то ${\displaystyle (\forall \alpha .~B)}$ — это тип. Внешние скобки часто опускают, оператор ${\displaystyle \rightarrow }$ считают правоассоциативным, а действие оператора ${\displaystyle \forall }$ продолжающимся вправо насколько это возможно. Например, ${\displaystyle \forall \alpha .~\forall \beta .~\alpha \to \beta \to \alpha }$ — стандартное сокращение для ${\displaystyle (\forall \alpha .~(\forall \beta .~(\alpha \to (\beta \to \alpha ))))}$. Синтаксис термов Термы Системы F конструируются из набора термовых переменных (${\displaystyle x}$, ${\displaystyle y}$, ${\displaystyle z}$ и т.д.) по следующим правилам (Переменная) Если ${\displaystyle x}$ — переменная, то ${\displaystyle x}$ — это терм; (Абстракция) Если ${\displaystyle x}$ является переменной, ${\displaystyle A}$ — типом, а ${\displaystyle M}$ — термом, то ${\displaystyle (\lambda x^{A}.~M)}$ — это терм; (Применение) Если ${\displaystyle M}$ и ${\displaystyle N}$ являются термами, то ${\displaystyle (M~N)}$ — это терм; (Универсальная абстракция) Если ${\displaystyle \alpha }$ является переменной типа, а ${\displaystyle M}$ — термом, то ${\displaystyle (\Lambda \alpha .~M)}$ — это терм; (Универсальное применение) Если ${\displaystyle M}$ является термом, а ${\displaystyle A}$ — типом, то ${\displaystyle (M~A)}$ — это терм. Внешние скобки часто опускают, оба сорта применения считают левоассоциативными, а действие абстракций — продолжающимся вправо насколько это возможно. Различают две версии просто типизированной системы. Если, как в приведённых выше правилах, термовые переменные в лямбда-абстракции аннотируются типами, то систему называют типизированной по Чёрчу. Если же правило абстракции заменить на (Абстракция по Карри) Если ${\displaystyle x}$ является переменной, а ${\displaystyle M}$ — термом, то ${\displaystyle (\lambda x.~M)}$ — это терм, и отбросить два последних правила, то систему называют типизированной по Карри. Фактически, термы системы, типизированной по Карри, те же, что и в бестиповом лямбда-исчислении. Правила редукции Помимо стандартного для лямбда-исчисления правила ${\displaystyle \beta }$-редукции ${\displaystyle (\lambda a^{A}.~M)~N\ \to _{\beta }\ M[a:=N]}$ в системе F в стиле Чёрча вводится дополнительное правило, ${\displaystyle (\Lambda \alpha .~M)~A\ \to _{\beta }\ M[\alpha :=A]}$, позволяющее вычислять применение терма к типу через механизм подстановки типа вместо переменной типа. Контексты типизации и утверждение типизации Контекстом, как и в просто типизированном лямбда-исчислении, называется множество утверждений о приписывании типов различным переменным, разделённых запятой ${\displaystyle \Gamma =x_{1}\!:\!A_{1},x_{2}\!:\!A_{1},\ldots ,x_{n}\!:\!A_{n}}$ В контекст можно добавить «свежую» для этого контекста переменную: если ${\displaystyle \Gamma }$ — допустимый контекст, не содержащий переменной ${\displaystyle x}$, а ${\displaystyle B}$ — тип, то ${\displaystyle \Gamma ,x\!:\!B}$ — тоже допустимый контекст. Общий вид утверждения о типизации таков: ${\displaystyle \Gamma \vdash M\!:\!A}$ Это читается следующим образом: в контексте ${\displaystyle \Gamma }$ терм ${\displaystyle M}$ имеет тип ${\displaystyle A}$. Правила типизации по Чёрчу В Системе F, типизированной по Чёрчу, приписывание типов термам осуществляется в соответствии со следующими правилами: (Начальное правило) Если переменная ${\displaystyle x}$ присутствует с типом ${\displaystyle A}$ в контексте ${\displaystyle \Gamma }$, то в этом контексте ${\displaystyle x}$ имеет тип ${\displaystyle A}$. В виде правила вывода ${\displaystyle {x\!:\!A\in \Gamma } \over {\Gamma \vdash x\!:\!A}}$ (Правило введения ${\displaystyle \rightarrow }$) Если в некотором контексте, расширенном утверждением, что ${\displaystyle a}$ имеет тип ${\displaystyle A}$, терм ${\displaystyle M}$ имеет тип ${\displaystyle B}$, то в упомянутом контексте (без ${\displaystyle a}$), лямбда-абстракция ${\displaystyle \lambda a^{A}.~M}$ имеет тип ${\displaystyle A\to B}$. В виде правила вывода ${\displaystyle {\Gamma ,a\!:\!A\vdash M\!:\!B} \over {\Gamma \vdash (\lambda a^{A}.~M)\!:\!(A\to B)}}$ (Правило удаления ${\displaystyle \rightarrow }$) Если в некотором контексте терм ${\displaystyle M}$ имеет тип ${\displaystyle A\to B}$, а терм ${\displaystyle N}$ имеет тип ${\displaystyle A}$, то применение ${\displaystyle M~N}$ имеет тип ${\displaystyle B}$. В виде правила вывода ${\displaystyle {\Gamma \vdash M\!:\!(A\to B)\quad \Gamma \vdash N\!:\!A} \over {\Gamma \vdash (M~N)\!:\!B}}$ (Правило введения ${\displaystyle \forall }$) Если в некотором контексте терм ${\displaystyle M}$ имеет тип ${\displaystyle A}$, то в этом контексте терм ${\displaystyle \Lambda \alpha .~M}$ имеет тип ${\displaystyle \forall \alpha .~A}$. В виде правила вывода ${\displaystyle {\Gamma \vdash M\!:\!A} \over {\Gamma \vdash (\Lambda \alpha .~M)\!:\!(\forall \alpha .~A)}}$ Это правило требует оговорки: переменная типа ${\displaystyle \alpha }$ не должна встречаться в утверждениях типизации контекста ${\displaystyle \Gamma }$. (Правило удаления ${\displaystyle \forall }$) Если в некотором контексте терм ${\displaystyle M}$ имеет тип ${\displaystyle \forall \alpha .~A}$, и ${\displaystyle B}$ — это тип, то в этом контексте терм ${\displaystyle M~B}$ имеет тип ${\displaystyle A[\alpha :=B]}$. В виде правила вывода ${\displaystyle {\Gamma \vdash M\!:\!(\forall \alpha .~A)} \over {\Gamma \vdash (M~B)\!:\!(A[\alpha :=B])}}$ Правила типизации по Карри В Системе F, типизированной по Карри, приписывание типов термам осуществляется в соответствии со следующими правилами: (Начальное правило) Если переменная ${\displaystyle x}$ присутствует с типом ${\displaystyle A}$ в контексте ${\displaystyle \Gamma }$, то в этом контексте ${\displaystyle x}$ имеет тип ${\displaystyle A}$. В виде правила вывода ${\displaystyle {x\!:\!A\in \Gamma } \over {\Gamma \vdash x\!:\!A}}$ (Правило введения ${\displaystyle \rightarrow }$) Если в некотором контексте, расширенном утверждением, что ${\displaystyle a}$ имеет тип ${\displaystyle A}$, терм ${\displaystyle M}$ имеет тип ${\displaystyle B}$, то в упомянутом контексте (без ${\displaystyle a}$), лямбда-абстракция ${\displaystyle \lambda a.~M}$ имеет тип ${\displaystyle A\to B}$. В виде правила вывода ${\displaystyle {\Gamma ,a\!:\!A\vdash M\!:\!B} \over {\Gamma \vdash (\lambda a.~M)\!:\!(A\to B)}}$ (Правило удаления ${\displaystyle \rightarrow }$) Если в некотором контексте терм ${\displaystyle M}$ имеет тип ${\displaystyle A\to B}$, а терм ${\displaystyle N}$ имеет тип ${\displaystyle A}$, то применение ${\displaystyle M~N}$ имеет тип ${\displaystyle B}$. В виде правила вывода ${\displaystyle {\Gamma \vdash M\!:\!(A\to B)\quad \Gamma \vdash N\!:\!A} \over {\Gamma \vdash (M~N)\!:\!B}}$ (Правило введения ${\displaystyle \forall }$) Если в некотором контексте терм ${\displaystyle M}$ имеет тип ${\displaystyle A}$, то в этом контексте этому терму ${\displaystyle M}$ может быть приписан и тип ${\displaystyle \forall \alpha .~A}$. В виде правила вывода ${\displaystyle {\Gamma \vdash M\!:\!A} \over {\Gamma \vdash M\!:\!(\forall \alpha .~A)}}$ Это правило требует оговорки: переменная типа ${\displaystyle \alpha }$ не должна встречаться в утверждениях типизации контекста ${\displaystyle \Gamma }$. (Правило удаления ${\displaystyle \forall }$) Если в некотором контексте терм ${\displaystyle M}$ имеет тип ${\displaystyle \forall \alpha .~A}$, и ${\displaystyle B}$ — это тип, то в этом контексте этому терму ${\displaystyle M}$ может быть приписан и тип ${\displaystyle A[\alpha :=B]}$. В виде правила вывода ${\displaystyle {\Gamma \vdash M\!:\!(\forall \alpha .~A)} \over {\Gamma \vdash M\!:\!(A[\alpha :=B])}}$ Пример. По начальному правилу: ${\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )}$ Применим правило удаления ${\displaystyle \forall }$, взяв в качестве ${\displaystyle B}$ тип ${\displaystyle \forall \alpha .~\alpha \to \alpha }$ ${\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}$ Теперь по правилу удаления ${\displaystyle \rightarrow }$ имеем возможность применить терм ${\displaystyle x}$ сам к себе ${\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash (x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )}$ и, наконец, по правилу введения ${\displaystyle \rightarrow }$ ${\displaystyle \vdash (\lambda x.~x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}$ Это пример терма, типизируемого в Системе F, но не в просто типизированной системе. Представление типов данных Система F обладает достаточными выразительными средствами, для того чтобы напрямую реализовать многие типы данных, используемые в языках программирования. Будем работать в версии Чёрча системы F. Пустой тип. Тип ${\displaystyle \bot \ \equiv \ \forall \alpha .~\alpha }$ необитаем в системе F, то есть в ней отсутствуют термы с таким типом. Единичный тип. У типа ${\displaystyle \top \ \equiv \ \forall \alpha .~\alpha \to \alpha }$ в системе F имеется единственный находящийся в нормальной форме обитатель — терм ${\displaystyle {\mathtt {id}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~x}$. Булев тип. В системе F задается так: ${\displaystyle {\mathtt {Bool}}\ \equiv \ \forall \alpha .~\alpha \to \alpha \to \alpha }$. У этого типа ровно два обитателя, отождествляемых с двумя булевыми константами ${\displaystyle {\mathtt {true}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~x}$ ${\displaystyle {\mathtt {false}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~y}$ Конструкция условного оператора ${\displaystyle {\mathtt {ifThenElse}}\ \equiv \ \Lambda \alpha .~\lambda b^{\mathtt {Bool}}.~\lambda x^{\alpha }.~\lambda y^{\alpha }.~b\,\alpha \,x\,y}$ Эта функция удовлетворяет естественным требованиям ${\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {true}}\,M\,N=M}$ и ${\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {false}}\,M\,N=N}$ для произвольного типа ${\displaystyle A}$ и произвольных ${\displaystyle M\!:\!A}$ и ${\displaystyle N\!:\!A}$. В этом легко убедиться, раскрыв определения и выполнив ${\displaystyle \beta }$-редукции. Тип произведения. Для произвольных типов ${\displaystyle A}$ и ${\displaystyle B}$ тип их декартова произведения ${\displaystyle A\times B~\equiv ~\forall \alpha .~(A\to B\to \alpha )\to \alpha }$ населён парой ${\displaystyle \langle M;N\rangle ~\equiv ~\Lambda \alpha .~\lambda f^{(A\to B\to \alpha )}.~f~M~N}$ для каждых ${\displaystyle M\!:\!A}$ и ${\displaystyle N\!:\!B}$. Проекции пары задаются функциями ${\displaystyle {\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 }$ ${\displaystyle {\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 }$ Эти функции удовлетворяют естественным требованиям ${\displaystyle {\mathtt {fst}}\,A\,B\,\langle M;N\rangle =M}$ и ${\displaystyle {\mathtt {snd}}\,A\,B\,\langle M;N\rangle =N}$. Тип суммы. Для произвольных типов ${\displaystyle A}$ и ${\displaystyle B}$ тип их суммы ${\displaystyle A+B~\equiv ~\forall \alpha .~(A\to \alpha )\to (B\to \alpha )\to \alpha }$ населён либо термом типа ${\displaystyle A}$, либо термом типа ${\displaystyle B}$, в зависимости от применённого конструктора ${\displaystyle {\mathtt {injL}}\,M~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,f\,M}$ ${\displaystyle {\mathtt {injR}}\,N~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,g\,N}$ Здесь ${\displaystyle M\!:\!A}$, ${\displaystyle N\!:\!B}$. Функция, осуществляющая разбор случаев (сопоставление с образцом), имеет вид ${\displaystyle {\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 }$ Эта функция удовлетворяет следующим естественным требованиям ${\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injL}}\,M)\,F\,G=F\,M}$ и ${\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injR}}\,N)\,F\,G=G\,N}$ для произвольных типов ${\displaystyle A}$, ${\displaystyle B}$ и ${\displaystyle C}$ и произвольных термов ${\displaystyle F\!:\!A\to C}$ и ${\displaystyle G\!:\!B\to C}$. Числа Чёрча. Тип натуральных чисел в системе F ${\displaystyle {\mathtt {Nat}}\ \equiv \ \forall \alpha .~\alpha \to (\alpha \to \alpha )\to \alpha }$ населён бесконечным количеством различных элементов, получаемых посредством двух конструкторов ${\displaystyle {\mathtt {zero}}\!:\!{\mathtt {Nat}}}$ и ${\displaystyle {\mathtt {succ}}\!:\!{\mathtt {Nat}}\to {\mathtt {Nat}}}$: ${\displaystyle {\mathtt {zero}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,z}$ ${\displaystyle {\mathtt {succ}}\ \equiv \ \lambda n^{\mathtt {Nat}}.\,\Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,s\,(n\,\alpha \,z\,s)}$ Натуральное число ${\displaystyle n}$ может быть получено ${\displaystyle n}$-кратным применением второго конструктора к первому или, эквивалентно, представлено термом ${\displaystyle {\overline {n}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \rightarrow \alpha }.\,\underbrace {s(s(s\ldots (s} _{n}\,z)\ldots ))}$ Свойства Просто типизированная система обладает свойством типовой безопасности: при ${\displaystyle \beta }$-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений. В своей диссертации Жан-Ив Жирар показал[1], что Система F обладает свойством сильной нормализации: любой допустимый терм за конечное число ${\displaystyle \beta }$-редукций приводится к единственной нормальной форме. Система F является импредикативной системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм ${\displaystyle {\texttt {id}}}$ единичного типа ${\displaystyle \top \equiv \forall \alpha .~\alpha \to \alpha }$ может быть применён к собственному типу, порождая терм типа ${\displaystyle \top \to \top }$. Как показал Джо Уэллс в 1994 году[3], задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера. Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской логикой высказываний второго порядка[англ.], формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения ${\displaystyle \top }$ (истина), ${\displaystyle \bot }$ (ложь), связки ${\displaystyle \lnot }$ (отрицание), ${\displaystyle \land }$ (конъюнкция) и ${\displaystyle \lor }$ (дизъюнкция), а также ${\displaystyle \exists }$ (квантор существования) могут быть определены так ${\displaystyle \top ~\equiv ~\forall \alpha .\,\alpha \to \alpha }$ ${\displaystyle \bot ~\equiv ~\forall \alpha .\,\alpha }$ ${\displaystyle \lnot A~\equiv ~A\to \bot }$ ${\displaystyle A\land B~\equiv ~\forall \alpha .\,(A\to B\to \alpha )\to \alpha }$ ${\displaystyle A\lor B~\equiv ~\forall \alpha .\,(A\to \alpha )\to (B\to \alpha )\to \alpha }$ ${\displaystyle \exists \alpha .\,M[\alpha ]~\equiv ~\forall \gamma .\,(\forall \alpha .\,M[\alpha ]\to \gamma )\to \gamma }$ Отметим, что соответствие Карри — Ховарда ставит в соответствие истине — единичный тип, лжи — пустой тип, конъюнкции — произведение типов, а дизъюнкции — их сумму. Примечания 1 2 Girard, Jean-Yves. Interprtation fonctionnelle et limination des coupures de l’arithmtique d’ordre suprieur : Ph.D. thesis. — Universit Paris 7, 1972. John C. Reynolds. Towards a Theory of Type Structure. — 1974. Архивировано 31 октября 2014 года. 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. Архивировано 22 февраля 2007 года. Литература Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1. Перевод на русский язык: Barendregt, Henk. Lambda Calculi with Types // Handbook of Logic in Computer Science. — Oxford University Press, 1992. — Т. II. — С. 117-309.