Систе́ма F (полімо́рфне ля́мбда-чи́слення, систе́ма
, типізо́ване ля́мбда-чи́слення дру́гого поря́дку) — система типізованого лямбда-числення, що відрізняється від просто типізованої системи наявністю механізму універсальної квантифікації над типами. Цю систему розробив 1972 року Жан-Ів Жирар[en][1] у контексті теорії доведень у логіці. Незалежно від нього подібну систему запропонував 1974 року Джон Рейнольдс[en][2]. Система F дозволяє формалізувати концепцію параметричного поліморфізму в мовах програмування та слугує теоретичною основою для таких мов програмування як Haskell та ML.
Система F допускає конструювання термів, залежних від типів. Технічно це досягається через механізм абстрагування терму за типом, що в результаті дає новий терм. Традиційно для такої абстракції використовують символ великої лямбди
. Наприклад, взявши терм
типу
та абстрагуючись за змінною типу
, отримуємо терм
. Цей терм є функцією з типів у терми. Застосовуючи цю функцію до різних типів, ми отримуватимемо терми з ідентичною структурою, але різними типами:
— терм типу
;
— терм типу
.
Видно, що терм
має поліморфну поведінку, тобто задає спільний інтерфейс для різних типів даних. У системі F цьому терму приписується тип
. Квантор загальності в типі підкреслює можливість підстановки замість змінної типу
будь-якого допустимого типу.
Формальний опис
Синтаксис типів
Типи Системи F конструюються із набору змінних типу за допомогою операторів
і
. За традицією для змінних типу використовують грецькі літери. Правила формування типів такі:
- (Змінна типу) Якщо
— змінна типу, то
— це тип; - (Стрілковий тип) Якщо
і
є типами, то
— це тип; - (Універсальний тип) Якщо
є змінною типу, а
— типом, то
— це тип.
Зовнішні дужки часто опускають, оператор
вважають правоасоціативним, а дію оператора
такою, що продовжується праворуч наскільки це можливо. Наприклад,
— стандартне скорочення для
.
Синтаксис термів
Терми системи F конструюються з набору термових змінних (
,
,
і т. д.) за такими правилами
- (Змінна) Якщо
— змінна, то
— це терм; - (Абстракція) Якщо
є змінною,
— типом, а
— термом, то
— це терм; - (Застосування) Якщо
і
є термами, то
— це терм; - (Універсальна абстракція) Якщо
є змінною типу, а
— термом, то
— це терм; - (Універсальне застосування) Якщо
є термом, а
— типом, то
— це терм.
Зовнішні дужки часто опускають, обидва сорти застосування вважають лівоасоціативними, а дію абстракцій — такою, що продовжується вправо наскільки це можливо.
Розрізняють дві версії просто типізованої системи. Якщо, як у наведених вище правилах, термові змінні в лямбда-абстракції анотуються типами, то систему називають типізованою за Чорчем. Якщо ж правило абстракції замінити на
- (Абстракція за Каррі) Якщо
є змінною, а
— термом, то
— це терм, і відкинути два останні правила, то систему називають типізованою за Каррі. Фактично, терми системи, типізованої за Каррі, ті самі, що й у безтиповому лямбда-численні.
Правила редукції
Крім стандартного для лямбда-обчислення правила
-редукції
![{\displaystyle (\lambda a^{A}.~M)~N\ \to _{\beta }\ M[a:=N]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/154fd8e28a0e3e57e44b5387bfa351fbacf59a3a)
у системі F у стилі Чорча вводиться додаткове правило,
,
що дозволяє обчислювати застосування терму до типу через механізм підстановки типу замість змінної типу.
Контексти типізації та затвердження типізації
Контекстом, як і в просто типізованому лямбда-обчисленні, називають множину тверджень про приписування типів різним змінним, розділених комою
![{\displaystyle \Gamma =x_{1}\!:\!A_{1},x_{2}\!:\!A_{1},\ldots ,x_{n}\!:\!A_{n}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4c67fce4d78b6369dfff7f669fad5d8267b6f71)
У контекст можна додати «свіжу» для цього контексту змінну: якщо
— допустимий контекст, який не містить змінної
, а
— тип, то
— теж допустимий контекст.
Загальний вигляд твердження про типізацію такий:
![{\displaystyle \Gamma \vdash M\!:\!A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f2600857f6a91c56805cb4592cda1515f079d7c)
Це читається так: у контексті
терм
має тип
.
Правила типізації за Чорчем
У системі F, типізованій за Чорчем, типи термам приписують за такими правилами: (Початкове правило) Якщо змінна
пирсутня в контексті
з типом
, то в цьому контексті
має тип
. У вигляді правила виведення
|
(Правило введення
) Якщо в деякому контексті, розширеному твердженням, що
має тип
, терм
має тип
, то в згаданому контексті (без
), лямбда-абстракція
має тип
. У вигляді правила виведення
|
(Правило видалення
) Якщо в деякому контексті терм
має тип
, а терм
має тип
, то застосування
має тип
. У вигляді правила виведення
|
(Правило введення
) Якщо в деякому контексті терм
має тип
, то в цьому контексті терм
має тип
. У вигляді правила виведення
|
Це правило вимагає застереження: змінна типу
не повинна зустрічатися у твердженнях типізації контексту
.
(Правило видалення
) Якщо в деякому контексті терм
має тип
, і
— це тип, то в цьому контексті терм
має тип
. У вигляді правила виведення
|
Правила типізації за Каррі
У системі F, типізованій за Каррі, приписування типів терм здійснюється відповідно до таких правил: (Початкове правило) Якщо змінна
в контексті
присутня з типом
, то в цьому контексті
має тип
. У вигляді правила виведення
|
(Правило введення
) Якщо в деякому контексті, розширеному твердженням, що
має тип
, терм
має тип
, то в згаданому контексті (без
), лямбда-абстракція
має тип
. У вигляді правила виведення
|
(Правило видалення
) Якщо в деякому контексті терм
має тип
, а терм
має тип
, то застосування
має тип
. У вигляді правила виведення
|
(Правило введення
) Якщо в деякому контексті терм
має тип
, то в цьому контексті цьому терму
можна приписати і тип
. У вигляді правила виведення
|
Це правило вимагає застереження: змінна типу
не повинна зустрічатися у твердженнях типізації контексту
.
(Правило видалення
) Якщо в деякому контексті терм
має тип
, і
— це тип, то в цьому контексті цьому терму
можна приписати й тип
. У вигляді правила виведення
|
- Приклад
За початковим правилом:
![{\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d5540e1bfac30468b60220503b43497fe44192b8)
Застосуємо правило видалення
, взявши як
тип
![{\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ed5b9c06decf0122ebce032557dd236779158453)
Тепер за правилом видалення
маємо можливість застосувати терм
сам до себе
![{\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash (x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc89f1b5d079643f7b22d47d4b300ecea4527d32)
і, нарешті, за правилом введення
![{\displaystyle \vdash (\lambda x.~x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/359032ff85ae77efd3d5e207f29ba131c5a7ddc9)
Це приклад терму, що типізується в системі F, але не в просто типізованій системі .
Подання типів даних
Система F має достатні виражальні засоби, для того щоб безпосередньо реалізувати багато типів даних, що використовуються в мовах програмування. Працюватимемо у версії Чорча системи F.
Порожній тип. Тип
![{\displaystyle \bot \ \equiv \ \forall \alpha .~\alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/befee1ce5e552b2623db8df7c76edb04b7b2beed)
ненаселений у системі F, тобто у ній відсутні терми з таким типом.
Одиничний тип. У типу
![{\displaystyle \top \ \equiv \ \forall \alpha .~\alpha \to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/63f83b054b31001dee0f207869616ceeb762e662)
в системі F є єдиний мешканець, що перебуває в нормальній формі, — терм.
.
Булів тип. У системі F задається так:
.
У цього типу рівно два мешканці, ототожнювані з двома булевими константами.
![{\displaystyle {\mathtt {true}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~x}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c89424be7e51ad294ee7c742288e042c5f806a2b)
![{\displaystyle {\mathtt {false}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~y}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b5a46012956ef0092a1381d9f25d210ba5e6ab8f)
Конструкція умовного оператора
![{\displaystyle {\mathtt {ifThenElse}}\ \equiv \ \Lambda \alpha .~\lambda b^{\mathtt {Bool}}.~\lambda x^{\alpha }.~\lambda y^{\alpha }.~b\,\alpha \,x\,y}](https://wikimedia.org/api/rest_v1/media/math/render/svg/69765b80478131814adbe47469301555a507db08)
Ця функція відповідає природним вимогам
![{\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {true}}\,M\,N=M}](https://wikimedia.org/api/rest_v1/media/math/render/svg/458a3828350ac775676d29b47892e62b0c6fb02f)
і
![{\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {false}}\,M\,N=N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ac13617774503a288a99044f60dbbf804eaac9cf)
для довільного типу
та довільних
і
. У цьому легко переконатися, розкривши визначення та виконавши
-редукції.
Тип добутку. Для довільних типів
і
тип їх декартового твору
![{\displaystyle A\times B~\equiv ~\forall \alpha .~(A\to B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/58abe456f94c28adabe0ccc855c15336cde4eacc)
населений парою
![{\displaystyle \langle M;N\rangle ~\equiv ~\Lambda \alpha .~\lambda f^{(A\to B\to \alpha )}.~f~M~N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/35502f72922c81d9ac3410a65f62070b1b797b3a)
для кожних
і
. Проєкції пари задаються функціями
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/1866f1804caa00825282fb229236fded8e36d231)
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/c099795a0ebcb20e873179d4bd6ceecbffd00373)
Ці функції відповідають природним вимогам
і
.
Тип суми. Для довільних типів
і
тип їх суми
![{\displaystyle A+B~\equiv ~\forall \alpha .~(A\to \alpha )\to (B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/6de7cb764b841c6a957d8d3b758e774bfec606c7)
населений або термом типу
, або термом типу
, залежно від застосованого конструктора
![{\displaystyle {\mathtt {injL}}\,M~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,f\,M}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3567d6a2119a4f0ad188fa90c163be8f24e5def9)
![{\displaystyle {\mathtt {injR}}\,N~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,g\,N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aa9957c8d8754ae33e2cde3d69c99df70e101d85)
Тут
,
. Функція, що здійснює розбір випадків (порівняння зі взірцем), має вигляд
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/f8311c58e757435dce68e677ad28ef7e9ea1ca43)
Ця функція відповідає таким природним вимогам
![{\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injL}}\,M)\,F\,G=F\,M}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bbe3b1b9dd4aac3089b13b1dbaa5f5c060c0ee3f)
і
![{\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injR}}\,N)\,F\,G=G\,N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/947e1b55549469d3576c753ec642fd1c6859fbb0)
для довільних типів
,
і
та довільних термів
і
.
Числа Чорча. Тип натуральних чисел у системі F
![{\displaystyle {\mathtt {Nat}}\ \equiv \ \forall \alpha .~\alpha \to (\alpha \to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/cdb2bb94d49604a2b6f0f4815407ba2e1219f052)
населений нескінченною кількістю різних елементів, одержуваних за допомогою двох конструкторів
і
:
![{\displaystyle {\mathtt {zero}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,z}](https://wikimedia.org/api/rest_v1/media/math/render/svg/335b340f8437669a209cd9c5567c1b5e664c8931)
![{\displaystyle {\mathtt {succ}}\ \equiv \ \lambda n^{\mathtt {Nat}}.\,\Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,s\,(n\,\alpha \,z\,s)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ccaff29aff61287ad3507f67cf9cfa6259e83bd)
Натуральне число
можна отримати застосувавши
разів другий конструктор до першого або, еквівалентно, подати термом
![{\displaystyle {\overline {n}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \rightarrow \alpha }.\,\underbrace {s(s(s\ldots (s} _{n}\,z)\ldots ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d742f3b5197cc598efb69d91ebe7d9805cd22fb3)
Властивості
- Просто типізована система має властивість ти́пової безпеки: при
-редукціях тип лямбда-терму залишається незмінним, а сама типізація не заважає перебігу обчислень.
- У своїй дисертації Жан-Ів Жирар[en] показав[1], що система F має властивість сильної нормалізації: будь-який допустимий терм за скінченне число
-редукцій зводиться до єдиної нормальної форми.
- Система F є імпредикативною системою, оскільки змінна типу, що зв'язується квантором загальності при визначенні універсального типу, може заміщатися самим об'єктом, що визначається. Наприклад, терм
одиничного типу
можна застосувати до власного типу, породжуючи терм типу
. Як показав Джо Веллз (Joe Wells) 1994 року[3], задача виведення типів для версії Каррі системи F нерозв'язна. Тому при практичній реалізації мов програмування зазвичай використовують обмежені, предикативні версії поліморфізму: пренекс-поліморфізм (поліморфізм у стилі ML), поліморфізм рангу 2 тощо. У разі пренекс-поліморфізму областю визначення змінних типу є лише типи без кванторів. У цих системах задачу виведення типів можна розв'язати, такий висновок базується на алгоритмі Гіндлі — Мілнера.
- Відповідність Каррі — Говарда пов'язує систему F із мінімальною інтуїціоністською логікою висловлювань другого порядку[en], формули якої побудовано з пропозиційних змінних за допомогою імплікації та універсальної квантифікації за висловлюваннями. При цьому значення
(істина),
(брехня), зв'язки
(заперечення),
(кон'юнкція) та
(диз'юнкція), а також
(квантор існування) можна визначити так
![{\displaystyle \top ~\equiv ~\forall \alpha .\,\alpha \to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/8eef891729e0c009a80334f213ac111660a8c6e8)
![{\displaystyle \bot ~\equiv ~\forall \alpha .\,\alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc9c68ba07b1b3fbcb36fa6e1929e0f599d85fe8)
![{\displaystyle \lnot A~\equiv ~A\to \bot }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ae988a96ea0b8c359706cd0ac1bc0ed098e63fbb)
![{\displaystyle A\land B~\equiv ~\forall \alpha .\,(A\to B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ed9333f4930ecc2ffb620d993b4fb1b58a4eadc)
![{\displaystyle A\lor B~\equiv ~\forall \alpha .\,(A\to \alpha )\to (B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/a1347ecd1951bf3208fc954b68e3b81e0d1447ea)
![{\displaystyle \exists \alpha .\,M[\alpha ]~\equiv ~\forall \gamma .\,(\forall \alpha .\,M[\alpha ]\to \gamma )\to \gamma }](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1a7cd018093ccc25534e9938eb1a9d4bf039ba1)
Зазначимо, що відповідність Каррі — Говарда ставить у відповідність до істини — одиничний тип, брехні — порожній тип, кон'юнкції — добуток типів, а диз'юнкції — їх суму.
Примітки
- ↑ а б Girard, Jean-Yves. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. — Université Paris 7, 1972.
- ↑ John C. Reynolds. Towards a Theory of Type Structure : [арх. 31 жовтня 2014]. — 1974.
- ↑ Wells J. B. Typability and type checking in the second-order lambda-calculus are equivalent and undecidable : [арх. 22 лютого 2007] // Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). — 1994. — С. 176–185.
Література
- 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 (28 липня). — С. 117-309.
- Jean-Yves Girard, Paul Taylor, Yves Lafont. Proofs and Types. — Cambridge University Press, 1989. — ISBN 0 521 37181 3.