Систе́ма F (полімо́рфне ля́мбда-чи́слення, систе́ма , типізо́ване ля́мбда-чи́слення дру́гого поря́дку) — система типізованого лямбда-числення, що відрізняється від наявністю механізму універсальної квантифікації над типами. Цю систему розробив 1972 року [en] у контексті теорії доведень у логіці. Незалежно від нього подібну систему запропонував 1974 року [en]. Система F дозволяє формалізувати концепцію в мовах програмування та слугує теоретичною основою для таких мов програмування як Haskell та ML.
Система F допускає конструювання термів, залежних від типів. Технічно це досягається через механізм абстрагування терму за типом, що в результаті дає новий терм. Традиційно для такої абстракції використовують символ великої лямбди . Наприклад, взявши терм типу та абстрагуючись за змінною типу , отримуємо терм . Цей терм є функцією з типів у терми. Застосовуючи цю функцію до різних типів, ми отримуватимемо терми з ідентичною структурою, але різними типами:
- — терм типу ;
- — терм типу .
Видно, що терм має поліморфну поведінку, тобто задає спільний інтерфейс для різних типів даних. У системі F цьому терму приписується тип . Квантор загальності в типі підкреслює можливість підстановки замість змінної типу будь-якого допустимого типу.
Формальний опис
Синтаксис типів
Типи Системи F конструюються із набору змінних типу за допомогою операторів і . За традицією для змінних типу використовують грецькі літери. Правила формування типів такі:
- (Змінна типу) Якщо — змінна типу, то — це тип;
- (Стрілковий тип) Якщо і є типами, то — це тип;
- (Універсальний тип) Якщо є змінною типу, а — типом, то — це тип.
Зовнішні дужки часто опускають, оператор вважають правоасоціативним, а дію оператора такою, що продовжується праворуч наскільки це можливо. Наприклад, — стандартне скорочення для .
Синтаксис термів
Терми системи F конструюються з набору термових змінних (, , і т. д.) за такими правилами
- (Змінна) Якщо — змінна, то — це терм;
- (Абстракція) Якщо є змінною, — типом, а — термом, то — це терм;
- (Застосування) Якщо і є термами, то — це терм;
- (Універсальна абстракція) Якщо є змінною типу, а — термом, то — це терм;
- (Універсальне застосування) Якщо є термом, а — типом, то — це терм.
Зовнішні дужки часто опускають, обидва сорти застосування вважають лівоасоціативними, а дію абстракцій — такою, що продовжується вправо наскільки це можливо.
Розрізняють дві версії просто типізованої системи. Якщо, як у наведених вище правилах, термові змінні в лямбда-абстракції анотуються типами, то систему називають типізованою за Чорчем. Якщо ж правило абстракції замінити на
- (Абстракція за Каррі) Якщо є змінною, а — термом, то — це терм, і відкинути два останні правила, то систему називають типізованою за Каррі. Фактично, терми системи, типізованої за Каррі, ті самі, що й у безтиповому лямбда-численні.
Правила редукції
Крім стандартного для лямбда-обчислення правила -редукції
у системі F у стилі Чорча вводиться додаткове правило,
- ,
що дозволяє обчислювати застосування терму до типу через механізм підстановки типу замість змінної типу.
Контексти типізації та затвердження типізації
Контекстом, як і в , називають множину тверджень про приписування типів різним змінним, розділених комою
У контекст можна додати «свіжу» для цього контексту змінну: якщо — допустимий контекст, який не містить змінної , а — тип, то — теж допустимий контекст.
Загальний вигляд твердження про типізацію такий:
Це читається так: у контексті терм має тип .
Правила типізації за Чорчем
У системі F, типізованій за Чорчем, типи термам приписують за такими правилами: (Початкове правило) Якщо змінна пирсутня в контексті з типом , то в цьому контексті має тип . У вигляді правила виведення
(Правило введення ) Якщо в деякому контексті, розширеному твердженням, що має тип , терм має тип , то в згаданому контексті (без ), лямбда-абстракція має тип . У вигляді правила виведення
(Правило видалення ) Якщо в деякому контексті терм має тип , а терм має тип , то застосування має тип . У вигляді правила виведення
(Правило введення ) Якщо в деякому контексті терм має тип , то в цьому контексті терм має тип . У вигляді правила виведення
Це правило вимагає застереження: змінна типу не повинна зустрічатися у твердженнях типізації контексту .
(Правило видалення ) Якщо в деякому контексті терм має тип , і — це тип, то в цьому контексті терм має тип . У вигляді правила виведення
Правила типізації за Каррі
У системі F, типізованій за Каррі, приписування типів терм здійснюється відповідно до таких правил: (Початкове правило) Якщо змінна в контексті присутня з типом , то в цьому контексті має тип . У вигляді правила виведення
(Правило введення ) Якщо в деякому контексті, розширеному твердженням, що має тип , терм має тип , то в згаданому контексті (без ), лямбда-абстракція має тип . У вигляді правила виведення
(Правило видалення ) Якщо в деякому контексті терм має тип , а терм має тип , то застосування має тип . У вигляді правила виведення
(Правило введення ) Якщо в деякому контексті терм має тип , то в цьому контексті цьому терму можна приписати і тип . У вигляді правила виведення
Це правило вимагає застереження: змінна типу не повинна зустрічатися у твердженнях типізації контексту .
(Правило видалення ) Якщо в деякому контексті терм має тип , і — це тип, то в цьому контексті цьому терму можна приписати й тип . У вигляді правила виведення
- Приклад
За початковим правилом:
Застосуємо правило видалення , взявши як тип
Тепер за правилом видалення маємо можливість застосувати терм сам до себе
і, нарешті, за правилом введення
Це приклад терму, що типізується в системі F, але не в .
Подання типів даних
Система F має достатні виражальні засоби, для того щоб безпосередньо реалізувати багато типів даних, що використовуються в мовах програмування. Працюватимемо у версії Чорча системи F.
Порожній тип. Тип
ненаселений у системі F, тобто у ній відсутні терми з таким типом.
Одиничний тип. У типу
в системі F є єдиний мешканець, що перебуває в нормальній формі, — терм.
- .
Булів тип. У системі F задається так:
- .
У цього типу рівно два мешканці, ототожнювані з двома булевими константами.
Конструкція умовного оператора
Ця функція відповідає природним вимогам
і
для довільного типу та довільних і . У цьому легко переконатися, розкривши визначення та виконавши -редукції.
Тип добутку. Для довільних типів і тип їх декартового твору
населений парою
для кожних і . Проєкції пари задаються функціями
Ці функції відповідають природним вимогам і .
Тип суми. Для довільних типів і тип їх суми
населений або термом типу , або термом типу , залежно від застосованого конструктора
Тут , . Функція, що здійснює розбір випадків (порівняння зі взірцем), має вигляд
Ця функція відповідає таким природним вимогам
і
для довільних типів , і та довільних термів і .
Числа Чорча. Тип натуральних чисел у системі F
населений нескінченною кількістю різних елементів, одержуваних за допомогою двох конструкторів і :
Натуральне число можна отримати застосувавши разів другий конструктор до першого або, еквівалентно, подати термом
Властивості
- Просто типізована система має властивість ти́пової безпеки: при -редукціях тип лямбда-терму залишається незмінним, а сама типізація не заважає перебігу обчислень.
- У своїй дисертації [en] показав, що система F має властивість сильної нормалізації: будь-який допустимий терм за скінченне число -редукцій зводиться до єдиної нормальної форми.
- Система F є імпредикативною системою, оскільки змінна типу, що зв'язується квантором загальності при визначенні універсального типу, може заміщатися самим об'єктом, що визначається. Наприклад, терм одиничного типу можна застосувати до власного типу, породжуючи терм типу . Як показав Джо Веллз (Joe Wells) 1994 року, задача виведення типів для версії Каррі системи F нерозв'язна. Тому при практичній реалізації мов програмування зазвичай використовують обмежені, предикативні версії поліморфізму: пренекс-поліморфізм (поліморфізм у стилі ML), поліморфізм рангу 2 тощо. У разі пренекс-поліморфізму областю визначення змінних типу є лише типи без кванторів. У цих системах задачу виведення типів можна розв'язати, такий висновок базується на алгоритмі Гіндлі — Мілнера.
- Відповідність Каррі — Говарда пов'язує систему F із мінімальною інтуїціоністською [en], формули якої побудовано з пропозиційних змінних за допомогою імплікації та універсальної квантифікації за висловлюваннями. При цьому значення (істина), (брехня), зв'язки (заперечення), (кон'юнкція) та (диз'юнкція), а також (квантор існування) можна визначити так
Зазначимо, що відповідність Каррі — Говарда ставить у відповідність до істини — одиничний тип, брехні — порожній тип, кон'юнкції — добуток типів, а диз'юнкції — їх суму.
Примітки
- 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. — .
- Barendregt, Henk. Lambda Calculi with Types // Handbook of Logic in Computer Science. — Oxford University Press, 1992. — Т. II (16 червня). — С. 117-309.
- Jean-Yves Girard, Paul Taylor, Yves Lafont. Proofs and Types. — Cambridge University Press, 1989. — .
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Siste ma F polimo rfne lya mbda chi slennya siste ma l 2 displaystyle lambda 2 tipizo vane lya mbda chi slennya dru gogo porya dku sistema tipizovanogo lyambda chislennya sho vidriznyayetsya vid nayavnistyu mehanizmu universalnoyi kvantifikaciyi nad tipami Cyu sistemu rozrobiv 1972 roku en u konteksti teoriyi doveden u logici Nezalezhno vid nogo podibnu sistemu zaproponuvav 1974 roku en Sistema F dozvolyaye formalizuvati koncepciyu v movah programuvannya ta sluguye teoretichnoyu osnovoyu dlya takih mov programuvannya yak Haskell ta ML Sistema F dopuskaye konstruyuvannya termiv zalezhnih vid tipiv Tehnichno ce dosyagayetsya cherez mehanizm abstraguvannya termu za tipom sho v rezultati daye novij term Tradicijno dlya takoyi abstrakciyi vikoristovuyut simvol velikoyi lyambdi L displaystyle Lambda Napriklad vzyavshi term l x a x displaystyle lambda x alpha x tipu a a displaystyle alpha to alpha ta abstraguyuchis za zminnoyu tipu a displaystyle alpha otrimuyemo term L a l x a x displaystyle Lambda alpha lambda x alpha x Cej term ye funkciyeyu z tipiv u termi Zastosovuyuchi cyu funkciyu do riznih tipiv mi otrimuvatimemo termi z identichnoyu strukturoyu ale riznimi tipami L a l x a x Bool b l x Bool x displaystyle Lambda alpha lambda x alpha x texttt Bool to beta lambda x texttt Bool x term tipu Bool Bool displaystyle texttt Bool to texttt Bool L a l x a x Nat b l x Nat x displaystyle Lambda alpha lambda x alpha x texttt Nat to beta lambda x texttt Nat x term tipu Nat Nat displaystyle texttt Nat to texttt Nat Vidno sho term L a l x a x displaystyle Lambda alpha lambda x alpha x maye polimorfnu povedinku tobto zadaye spilnij interfejs dlya riznih tipiv danih U sistemi F comu termu pripisuyetsya tip a a a displaystyle forall alpha alpha to alpha Kvantor zagalnosti v tipi pidkreslyuye mozhlivist pidstanovki zamist zminnoyi tipu a displaystyle alpha bud yakogo dopustimogo tipu Formalnij opisSintaksis tipiv Tipi Sistemi F konstruyuyutsya iz naboru zminnih tipu za dopomogoyu operatoriv displaystyle to i displaystyle forall Za tradiciyeyu dlya zminnih tipu vikoristovuyut grecki literi Pravila formuvannya tipiv taki Zminna tipu Yaksho a displaystyle alpha zminna tipu to a displaystyle alpha ce tip Strilkovij tip Yaksho A displaystyle A i B displaystyle B ye tipami to A B displaystyle A to B ce tip Universalnij tip Yaksho a displaystyle alpha ye zminnoyu tipu a B displaystyle B tipom to a B displaystyle forall alpha B ce tip Zovnishni duzhki chasto opuskayut operator displaystyle rightarrow vvazhayut pravoasociativnim a diyu operatora displaystyle forall takoyu sho prodovzhuyetsya pravoruch naskilki ce mozhlivo Napriklad a b a b a displaystyle forall alpha forall beta alpha to beta to alpha standartne skorochennya dlya a b a b a displaystyle forall alpha forall beta alpha to beta to alpha Sintaksis termiv Termi sistemi F konstruyuyutsya z naboru termovih zminnih x displaystyle x y displaystyle y z displaystyle z i t d za takimi pravilami Zminna Yaksho x displaystyle x zminna to x displaystyle x ce term Abstrakciya Yaksho x displaystyle x ye zminnoyu A displaystyle A tipom a M displaystyle M termom to l x A M displaystyle lambda x A M ce term Zastosuvannya Yaksho M displaystyle M i N displaystyle N ye termami to M N displaystyle M N ce term Universalna abstrakciya Yaksho a displaystyle alpha ye zminnoyu tipu a M displaystyle M termom to L a M displaystyle Lambda alpha M ce term Universalne zastosuvannya Yaksho M displaystyle M ye termom a A displaystyle A tipom to M A displaystyle M A ce term Zovnishni duzhki chasto opuskayut obidva sorti zastosuvannya vvazhayut livoasociativnimi a diyu abstrakcij takoyu sho prodovzhuyetsya vpravo naskilki ce mozhlivo Rozriznyayut dvi versiyi prosto tipizovanoyi sistemi Yaksho yak u navedenih vishe pravilah termovi zminni v lyambda abstrakciyi anotuyutsya tipami to sistemu nazivayut tipizovanoyu za Chorchem Yaksho zh pravilo abstrakciyi zaminiti na Abstrakciya za Karri Yaksho x displaystyle x ye zminnoyu a M displaystyle M termom to l x M displaystyle lambda x M ce term i vidkinuti dva ostanni pravila to sistemu nazivayut tipizovanoyu za Karri Faktichno termi sistemi tipizovanoyi za Karri ti sami sho j u beztipovomu lyambda chislenni Pravila redukciyi Krim standartnogo dlya lyambda obchislennya pravila b displaystyle beta redukciyi l a A M N b M a N displaystyle lambda a A M N to beta M a N u sistemi F u stili Chorcha vvoditsya dodatkove pravilo L a M A b M a A displaystyle Lambda alpha M A to beta M alpha A sho dozvolyaye obchislyuvati zastosuvannya termu do tipu cherez mehanizm pidstanovki tipu zamist zminnoyi tipu Konteksti tipizaciyi ta zatverdzhennya tipizaciyi Kontekstom yak i v nazivayut mnozhinu tverdzhen pro pripisuvannya tipiv riznim zminnim rozdilenih komoyu G x 1 A 1 x 2 A 1 x n A n displaystyle Gamma x 1 A 1 x 2 A 1 ldots x n A n U kontekst mozhna dodati svizhu dlya cogo kontekstu zminnu yaksho G displaystyle Gamma dopustimij kontekst yakij ne mistit zminnoyi x displaystyle x a B displaystyle B tip to G x B displaystyle Gamma x B tezh dopustimij kontekst Zagalnij viglyad tverdzhennya pro tipizaciyu takij G M A displaystyle Gamma vdash M A Ce chitayetsya tak u konteksti G displaystyle Gamma term M displaystyle M maye tip A displaystyle A Pravila tipizaciyi za Chorchem U sistemi F tipizovanij za Chorchem tipi termam pripisuyut za takimi pravilami Pochatkove pravilo Yaksho zminna x displaystyle x pirsutnya v konteksti G displaystyle Gamma z tipom A displaystyle A to v comu konteksti x displaystyle x maye tip A displaystyle A U viglyadi pravila vivedennya x A G G x A displaystyle x A in Gamma over Gamma vdash x A Pravilo vvedennya displaystyle rightarrow Yaksho v deyakomu konteksti rozshirenomu tverdzhennyam sho a displaystyle a maye tip A displaystyle A term M displaystyle M maye tip B displaystyle B to v zgadanomu konteksti bez a displaystyle a lyambda abstrakciya l a A M displaystyle lambda a A M maye tip A B displaystyle A to B U viglyadi pravila vivedennya G a A M B G l a A M A B displaystyle Gamma a A vdash M B over Gamma vdash lambda a A M A to B Pravilo vidalennya displaystyle rightarrow Yaksho v deyakomu konteksti term M displaystyle M maye tip A B displaystyle A to B a term N displaystyle N maye tip A displaystyle A to zastosuvannya M N displaystyle M N maye tip B displaystyle B U viglyadi pravila vivedennya G M A B G N A G M N B displaystyle Gamma vdash M A to B quad Gamma vdash N A over Gamma vdash M N B Pravilo vvedennya displaystyle forall Yaksho v deyakomu konteksti term M displaystyle M maye tip A displaystyle A to v comu konteksti term L a M displaystyle Lambda alpha M maye tip a A displaystyle forall alpha A U viglyadi pravila vivedennya G M A G L a M a A displaystyle Gamma vdash M A over Gamma vdash Lambda alpha M forall alpha A Ce pravilo vimagaye zasterezhennya zminna tipu a displaystyle alpha ne povinna zustrichatisya u tverdzhennyah tipizaciyi kontekstu G displaystyle Gamma Pravilo vidalennya displaystyle forall Yaksho v deyakomu konteksti term M displaystyle M maye tip a A displaystyle forall alpha A i B displaystyle B ce tip to v comu konteksti term M B displaystyle M B maye tip A a B displaystyle A alpha B U viglyadi pravila vivedennya G M a A G M B A a B displaystyle Gamma vdash M forall alpha A over Gamma vdash M B A alpha B Pravila tipizaciyi za Karri U sistemi F tipizovanij za Karri pripisuvannya tipiv term zdijsnyuyetsya vidpovidno do takih pravil Pochatkove pravilo Yaksho zminna x displaystyle x v konteksti G displaystyle Gamma prisutnya z tipom A displaystyle A to v comu konteksti x displaystyle x maye tip A displaystyle A U viglyadi pravila vivedennya x A G G x A displaystyle x A in Gamma over Gamma vdash x A Pravilo vvedennya displaystyle rightarrow Yaksho v deyakomu konteksti rozshirenomu tverdzhennyam sho a displaystyle a maye tip A displaystyle A term M displaystyle M maye tip B displaystyle B to v zgadanomu konteksti bez a displaystyle a lyambda abstrakciya l a M displaystyle lambda a M maye tip A B displaystyle A to B U viglyadi pravila vivedennya G a A M B G l a M A B displaystyle Gamma a A vdash M B over Gamma vdash lambda a M A to B Pravilo vidalennya displaystyle rightarrow Yaksho v deyakomu konteksti term M displaystyle M maye tip A B displaystyle A to B a term N displaystyle N maye tip A displaystyle A to zastosuvannya M N displaystyle M N maye tip B displaystyle B U viglyadi pravila vivedennya G M A B G N A G M N B displaystyle Gamma vdash M A to B quad Gamma vdash N A over Gamma vdash M N B Pravilo vvedennya displaystyle forall Yaksho v deyakomu konteksti term M displaystyle M maye tip A displaystyle A to v comu konteksti comu termu M displaystyle M mozhna pripisati i tip a A displaystyle forall alpha A U viglyadi pravila vivedennya G M A G M a A displaystyle Gamma vdash M A over Gamma vdash M forall alpha A Ce pravilo vimagaye zasterezhennya zminna tipu a displaystyle alpha ne povinna zustrichatisya u tverdzhennyah tipizaciyi kontekstu G displaystyle Gamma Pravilo vidalennya displaystyle forall Yaksho v deyakomu konteksti term M displaystyle M maye tip a A displaystyle forall alpha A i B displaystyle B ce tip to v comu konteksti comu termu M displaystyle M mozhna pripisati j tip A a B displaystyle A alpha B U viglyadi pravila vivedennya G M a A G M A a B displaystyle Gamma vdash M forall alpha A over Gamma vdash M A alpha B Priklad Za pochatkovim pravilom x a a a x a a a displaystyle x forall alpha alpha to alpha vdash x forall alpha alpha to alpha Zastosuyemo pravilo vidalennya displaystyle forall vzyavshi yak B displaystyle B tip a a a displaystyle forall alpha alpha to alpha x a a a x a a a a a a displaystyle x forall alpha alpha to alpha vdash x forall alpha alpha to alpha to forall alpha alpha to alpha Teper za pravilom vidalennya displaystyle rightarrow mayemo mozhlivist zastosuvati term x displaystyle x sam do sebe x a a a x x a a a displaystyle x forall alpha alpha to alpha vdash x x forall alpha alpha to alpha i nareshti za pravilom vvedennya displaystyle rightarrow l x x x a a a a a a displaystyle vdash lambda x x x forall alpha alpha to alpha to forall alpha alpha to alpha Ce priklad termu sho tipizuyetsya v sistemi F ale ne v Podannya tipiv danihSistema F maye dostatni virazhalni zasobi dlya togo shob bezposeredno realizuvati bagato tipiv danih sho vikoristovuyutsya v movah programuvannya Pracyuvatimemo u versiyi Chorcha sistemi F Porozhnij tip Tip a a displaystyle bot equiv forall alpha alpha nenaselenij u sistemi F tobto u nij vidsutni termi z takim tipom Odinichnij tip U tipu a a a displaystyle top equiv forall alpha alpha to alpha v sistemi F ye yedinij meshkanec sho perebuvaye v normalnij formi term i d L a l x a x displaystyle mathtt id equiv Lambda alpha lambda x alpha x Buliv tip U sistemi F zadayetsya tak B o o l a a a a displaystyle mathtt Bool equiv forall alpha alpha to alpha to alpha U cogo tipu rivno dva meshkanci ototozhnyuvani z dvoma bulevimi konstantami t r u e L a l x a l y a x displaystyle mathtt true equiv Lambda alpha lambda x alpha lambda y alpha x f a l s e L a l x a l y a y displaystyle mathtt false equiv Lambda alpha lambda x alpha lambda y alpha y Konstrukciya umovnogo operatora i f T h e n E l s e L a l b B o o l l x a l y a b a x y displaystyle mathtt ifThenElse equiv Lambda alpha lambda b mathtt Bool lambda x alpha lambda y alpha b alpha x y Cya funkciya vidpovidaye prirodnim vimogam i f T h e n E l s e A t r u e M N M displaystyle mathtt ifThenElse A mathtt true M N M i i f T h e n E l s e A f a l s e M N N displaystyle mathtt ifThenElse A mathtt false M N N dlya dovilnogo tipu A displaystyle A ta dovilnih M A displaystyle M A i N A displaystyle N A U comu legko perekonatisya rozkrivshi viznachennya ta vikonavshi b displaystyle beta redukciyi Tip dobutku Dlya dovilnih tipiv A displaystyle A i B displaystyle B tip yih dekartovogo tvoru A B a A B a a displaystyle A times B equiv forall alpha A to B to alpha to alpha naselenij paroyu M N L a l f A B a f M N displaystyle langle M N rangle equiv Lambda alpha lambda f A to B to alpha f M N dlya kozhnih M A displaystyle M A i N B displaystyle N B Proyekciyi pari zadayutsya funkciyami f s t L a L b l p a b p a l x a l y b x a b a b a 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 s n d L a L b l p a b p b l x a l y b y a b a b b 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 Ci funkciyi vidpovidayut prirodnim vimogam f s t A B M N M displaystyle mathtt fst A B langle M N rangle M i s n d A B M N N displaystyle mathtt snd A B langle M N rangle N Tip sumi Dlya dovilnih tipiv A displaystyle A i B displaystyle B tip yih sumi A B a A a B a a displaystyle A B equiv forall alpha A to alpha to B to alpha to alpha naselenij abo termom tipu A displaystyle A abo termom tipu B displaystyle B zalezhno vid zastosovanogo konstruktora i n j L M L a l f A a l g B a f M displaystyle mathtt injL M equiv Lambda alpha lambda f A to alpha lambda g B to alpha f M i n j R N L a l f A a l g B a g N displaystyle mathtt injR N equiv Lambda alpha lambda f A to alpha lambda g B to alpha g N Tut M A displaystyle M A N B displaystyle N B Funkciya sho zdijsnyuye rozbir vipadkiv porivnyannya zi vzircem maye viglyad m a t c h L a L b L g l s a b l f a g l g b g s g f g a b g a b a g b g g 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 Cya funkciya vidpovidaye takim prirodnim vimogam m a t c h A B C i n j L M F G F M displaystyle mathtt match A B C mathtt injL M F G F M i m a t c h A B C i n j R N F G G N displaystyle mathtt match A B C mathtt injR N F G G N dlya dovilnih tipiv A displaystyle A B displaystyle B i C displaystyle C ta dovilnih termiv F A C displaystyle F A to C i G B C displaystyle G B to C Chisla Chorcha Tip naturalnih chisel u sistemi F N a t a a a a a displaystyle mathtt Nat equiv forall alpha alpha to alpha to alpha to alpha naselenij neskinchennoyu kilkistyu riznih elementiv oderzhuvanih za dopomogoyu dvoh konstruktoriv z e r o N a t displaystyle mathtt zero mathtt Nat i s u c c N a t N a t displaystyle mathtt succ mathtt Nat to mathtt Nat z e r o L a l z a l s a a z displaystyle mathtt zero equiv Lambda alpha lambda z alpha lambda s alpha to alpha z s u c c l n N a t L a l z a l s a a s n a z s displaystyle mathtt succ equiv lambda n mathtt Nat Lambda alpha lambda z alpha lambda s alpha to alpha s n alpha z s Naturalne chislo n displaystyle n mozhna otrimati zastosuvavshi n displaystyle n raziv drugij konstruktor do pershogo abo ekvivalentno podati termom n L a l z a l s a a s s s s n z displaystyle overline n equiv Lambda alpha lambda z alpha lambda s alpha rightarrow alpha underbrace s s s ldots s n z ldots VlastivostiProsto tipizovana sistema maye vlastivist ti povoyi bezpeki pri b displaystyle beta redukciyah tip lyambda termu zalishayetsya nezminnim a sama tipizaciya ne zavazhaye perebigu obchislen U svoyij disertaciyi en pokazav sho sistema F maye vlastivist silnoyi normalizaciyi bud yakij dopustimij term za skinchenne chislo b displaystyle beta redukcij zvoditsya do yedinoyi normalnoyi formi Sistema F ye impredikativnoyu sistemoyu oskilki zminna tipu sho zv yazuyetsya kvantorom zagalnosti pri viznachenni universalnogo tipu mozhe zamishatisya samim ob yektom sho viznachayetsya Napriklad term id displaystyle texttt id odinichnogo tipu a a a displaystyle top equiv forall alpha alpha to alpha mozhna zastosuvati do vlasnogo tipu porodzhuyuchi term tipu displaystyle top to top Yak pokazav Dzho Vellz Joe Wells 1994 roku zadacha vivedennya tipiv dlya versiyi Karri sistemi F nerozv yazna Tomu pri praktichnij realizaciyi mov programuvannya zazvichaj vikoristovuyut obmezheni predikativni versiyi polimorfizmu preneks polimorfizm polimorfizm u stili ML polimorfizm rangu 2 tosho U razi preneks polimorfizmu oblastyu viznachennya zminnih tipu ye lishe tipi bez kvantoriv U cih sistemah zadachu vivedennya tipiv mozhna rozv yazati takij visnovok bazuyetsya na algoritmi Gindli Milnera Vidpovidnist Karri Govarda pov yazuye sistemu F iz minimalnoyu intuyicionistskoyu en formuli yakoyi pobudovano z propozicijnih zminnih za dopomogoyu implikaciyi ta universalnoyi kvantifikaciyi za vislovlyuvannyami Pri comu znachennya displaystyle top istina displaystyle bot brehnya zv yazki displaystyle lnot zaperechennya displaystyle land kon yunkciya ta displaystyle lor diz yunkciya a takozh displaystyle exists kvantor isnuvannya mozhna viznachiti tak a a a displaystyle top equiv forall alpha alpha to alpha a a displaystyle bot equiv forall alpha alpha A A displaystyle lnot A equiv A to bot A B a A B a a displaystyle A land B equiv forall alpha A to B to alpha to alpha A B a A a B a a displaystyle A lor B equiv forall alpha A to alpha to B to alpha to alpha a M a g a M a g g displaystyle exists alpha M alpha equiv forall gamma forall alpha M alpha to gamma to gamma Zaznachimo sho vidpovidnist Karri Govarda stavit u vidpovidnist do istini odinichnij tip brehni porozhnij tip kon yunkciyi dobutok tipiv a diz yunkciyi yih sumu PrimitkiGirard Jean Yves Interpretation fonctionnelle et elimination des coupures de l arithmetique d ordre superieur Universite Paris 7 1972 John C Reynolds Towards a Theory of Type Structure 31 zhovtnya 2014 1974 Wells J B Typability and type checking in the second order lambda calculus are equivalent and undecidable 22 lyutogo 2007 Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science LICS 1994 S 176 185 LiteraturaPierce 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 T II 16 chervnya S 117 309 Jean Yves Girard Paul Taylor Yves Lafont Proofs and Types Cambridge University Press 1989 ISBN 0 521 37181 3