Теорія типів — це будь-яка формальна система, що може слугувати альтернативою наївній теорії множин. У теорії типів кожен «терм» має «тип», а операції виконуються в узгодженості з цими типами.
Теорія типів тісно пов'язана з системами типів — особливістю мов програмування, яка призначена для зменшення кількості помилок. Теорія типів була розроблена для обходження парадоксів формальної логіки.
Однією з найвідоміших теорій типів є типізоване лямбда-числення Алонзо Черча та інтуїціоністська теорія типів [en].
Історія
В проміжок між 1902 та 1908 роками Бертран Расселл запропонував різні теорії типів у відповідь до його відкриття, яке встановлювало присутність парадоксу Расселла у наївній теорії множин Готлоба Фреге. У 1908 році Расселл винайшов «розгалужену» теорію типів та «аксіому редукції», які були опубліковані у праці Вайтгеда та Расселла «Principia Mathematica». Вони намагалися вирішити парадокс Расселла за допомогою розробки ієрархії типів та призначенні кожної математичної сутності до типу. Сутності кожного типу будувалися сутностями типів, які розташовані нижче за ієрархією, що запобігало призначенню сутності до самої себе. У 1920-х роках Леон Хвістек та Френк Пламптон Ремзі запропонували нерозгалужену теорію типів, яка зараз відома як «теорія простих типів» або «проста теорія типів». Ця теорія не використовувала ієрархії типів та, як наслідок, не вимагала аксіоми редукції.
Найвідомішим прикладом використання типів є [en]Алонзо Черча. Теорія типів Черча допомогла формальним системам уникнути [en], присутнього у оригінальному безтиповому лямбда-численні. Черч продемонстрував, що ця теорія може служити основою для математики.
Базові поняття
У системі теорії типів кожен терм має тип. Наприклад, , та є окремими термами типу , тобто натуральними числами. Традиційно терм супроводжується двокрапкою і його типом, наприклад, .
Теорії типів мають явне обчислення, яке кодується правилами рерайтингу термів. Вони називаються правилами перетворення або, якщо правило працює лише в одному напрямку, правилом редукції. Наприклад, та є синтаксично різними термами, але перший терм редукується до другого. На запису ця редукція має вигляд .
Функції в теорії типів мають спеціальне правило редукції: аргумент виклику функції замінюється на кожне входження параметра у визначенні функції. Нехай функція визначена як (використовуючи лямбда нотацію Черча) або (використовуючи більш сучасну нотацію). Тоді виклик функції редукується шляхом заміни кожної копії термом в тілі визначення функції. Таким чином, .
Тип функції позначається стрілкою від типу параметра до результуючого типу функції. Таким чином, . Виклик функції з деяким аргументом може бути написаний з дужками або без них, наприклад, або . Зазвичай дужки не використовуються, тому що функції багатьох аргументів можуть бути визначеними за допомогою каррінгу.
Відмінності від теорії множин
Існує безліч різних теорій множин та різних систем теорії типів.
- Теорія множин побудована поверх логіки. Вона вимагає окремої системи, подібної логіці першого порядку. У теорії типів поняття типу «і» та «або» можуть бути закодовані як типи самої теорії типів.
- У теорії множин елемент може належати до безлічі різних множин, до підмножини, або до множини множин. У теорії типів терми, як правило, належать тільки до одного типу. (Там, де використовуються підмножини, теорія типів прагне використовувати функцію предикатів, яка повертає , якщо терм знаходиться в підмножині, та повертає в іншому випадку. Об'єднання двох типів можна зробити, створивши новий тип, який називається типом-сумою та містить нові терми.)
- Теорія множин зазвичай кодує числа як множини. ( — порожня множина, — множина, що містить порожню множину, і т. д.) Теорія типів може кодувати числа як функції, використовуючи [en], або як [en]. Індуктивні типи створюють нові константи для [en] і нуль, що дуже нагадує аксіоми Пеано.
- Теорія множин використовує нотацію побудови множини.
- Теорія типів має просте з'єднання з конструктивною математикою через [en] та може бути пов'язана з логікою ізоморфізмів Каррі — Говарда. Деякі теорії типів тісно пов'язані з теорією категорій.
Додаткові визначення
Нормалізація
Терм редукується до . Так як надалі не редукується, кажуть, що цей терм знаходиться у нормальній формі. Кажуть, що система теорії типів сильно нормалізується, якщо всі терми мають нормальну форму та будь-який порядок редукції досягає її. Слабо нормалізуючи системи мають нормальну форму, але деякі порядки редукції можуть назавжди зациклитися та ніколи її не досягнути.
Інколи визначення елементу запозичують з теорії множин та використовують його для позначення всіх закритих термів, які редукуються до однієї нормальної форми. Закритим термом називається терм, який не має параметрів. Терм виду має параметр та називається відкритим термом. Таким чином, та є різними термами, але вони обидва редукуються до елементу .
Схожим поняттям, яке визначається для закритих та відкритих термів, є поняття конвертованості. Два терми називаються конвертованими, якщо існує терм, до якого ці два терми редукуються. Наприклад, та є конвертованими. Терми та також є конвертованими. Однак терми та (де є вільною змінною) не є конвертованими, так як вони знаходяться у нормальній формі та не є однаковими. Слабо нормалізуючі системи можуть перевірити, чи є два терми конвертованими, шляхом редукції цих термів до однієї нормальної форми.
Залежні типи
Залежним типом називається тип, який залежить від термів та інших типів. Таким чином, тип, повернутий функцією, може залежати від аргументу функції.
Наприклад, список термів типу із 4 елементів може відрізнятися від списку термів типу із 5 елементів. У теорії типів з залежними типами можна визначити функцію, яка приймає параметр і повертає список, що містить нулів. Тип терму, породженого викликом функції з , відрізнявся би від типу терму, породженого викликом функції з .
Залежні типи відіграють центральну роль в теорії типів Мартіна-Льофа та в розробці функційних мов програмування, таких як [en], [en], Agda та [en].
Типи рівності
Багато систем теорії типів мають тип, який представляє рівність типів та термів. Цей тип відрізняється від конвертованості та часто визначається як пропозиційна рівність.
У теорії типів Мартіна-Льофа тип рівності (який також називається типом ідентичності) позначається як (від англ. Identity). Кажуть, що існує тип , коли є типом, а і — це терми типу . Терм типу інтерпретується як визначення рівності та .
На практиці можна побудувати тип , але такий тип не буде мати термів. У теорії типів Мартіна-Льофа нові терми рівності мають властивість рефлексивності. Якщо є термом типу , то існує терм типу . Більш складні рівності можуть бути створені шляхом створення рефлексивного терму та його подальшої редукції. Тобто якщо є термом типу , то існує терм типу , який редукується до терму типу . Таким чином, у цій системі рівність типів означає те, що два значення одного типу конвертуються за допомогою редукції.
Наявність типу рівності є важливим, оскільки їм можна маніпулювати всередині системи. Ми можемо також визначити нерівність типів: як у [en], відображаємо до . Тобто існує терм типу , але не існує терму типу .
[en] відрізняється від теорії типів Мартіна-Льофа в основному тим, як в них визначаються типи рівності.
Індуктивні типи
Система теорії типів вимагає деяких базових термів і типів для роботи. Деякі системи будують їх з функцій за допомогою [en]. Інші системи мають [en]: множину базових типів та множину конструкторів типів, які генерують типи з правильними властивостями. Наприклад, певні рекурсивні функції, побудовані на індуктивних типах, гарантовано припиняють свою роботу.
Коіндуктивний тип — це нескінченний тип даних, створений шляхом задання функції, яка генерує наступний елемент.
[en] будує більш широкий діапазон типів, дозволяючи одночасно визначати тип і рекурсивні функції, що працюють на ньому.
Універсальний тип
Типи були створені для запобігання парадоксів, таких як парадокс Расселла. Проте мотиви, які призводять до таких парадоксів (здатність формулювати твердження про всі типи) все ще існують. Саме тому багато теорій типів мають «універсальний» тип, який містить всі інші типи (але не самого себе).
У системах, де ви можете стверджувати щось відносно універсальних типів, існує ієрархія універсальних типів, кожний з яких містить нижчий за ієрархією тип. Ця ієрархія визначається нескінченною, але ствердженя повинні стосуватися лише кінцевого числа універсальних рівнів.
Універсальні типи особливо складні в теорії типів. Первісна пропозиція теорії типів Мартіна-Льофа страждала від [en].
Обчислювальна складова
Багато систем теорії типів, таких як [en], теорія типів Мартіна-Льофа, обчислення конструкцій, також є мовами програмування. Таким чином, кажуть, що вони мають «обчислювальну складову». Обчислення — це редукція термів мови за допомогою правил рерайтингу.
Система теорії типів, яка має якісну обчислювальну складову, також має просте з'єднання з конструктивною математикою через [en].
Теорії типів
Значні
- [en] (яке є [en]);
- теорія типів Мартіна-Льофа;
- система F;
- обчислення конструкцій.
Другорядні
- [en];
- деякі форми комбінаторної логіки;
- [en];
- теорії типів, які визначені для лямбда-куба;
- типізоване лямбда-числення;
- чисті системи типів.
Активні
- [en] зараз досліджується.
Практичне використання
Мови програмування
Існує тісний зв'язок між теорією типів та системами типізації. Системи типів є особливістю мов програмування, призначеної для виявлення помилок. Будь-який статичний аналіз програми, такий як алгоритми перевірки типу в фазі семантичного аналізу компілятором, має зв'язок з теорією типів.
Яскравим прикладом є Agda — мова програмування, що використовує теорію типів Мартіна-Льофа у якості своєї системи типів. Мова програмування ML була розроблена для маніпулювання теоріями типів та її власна система типів була під сильним впливом теорії типів.
Математичні основи
Перший комп'ютерний асистент, називався [en], використовував теорію типів для кодування математики на комп'ютері. [en] спеціально розробив теорію типів, щоб кодувати всю математику для розробки нових математичних основ. Існує дослідження математичних основ з використанням [en].
Математики, що працюють з теорією категорій, вже мали труднощі при роботі з широко поширеною теорією множин Цермело — Френкеля. Це призвело до таких пропозицій, як елементарна теорія категорій множин (ETCS) Уільяма Ловера. Дослідники вивчають зв'язки між залежними типами (особливо типом ідентичності) та алгебричною топологією (зокрема гомотопією).
Асистенти для доказів
Значна частина сучасних досліджень теорії типів проводиться для розвитку автоматизованої перевірки доказів, інтерактивних асистентів для доказів та автоматизованих доказів теорем. Більшість цих систем використовують теорію типів як математичну основу для кодування доказів, що не дивно, враховуючи тісний зв'язок між теорією типів і мовами програмування:
- Багато теорій типів, побудованих на [en], використовуються для систем [en] and [en];
- теорія типів Мартіна-Льофа використовується Agda — мовою програмування та асистентом для доказів;
- обчислювальна теорія типів використовується [en];
- обчислення конструкцій використовується Coq та [en].
Багато теорій типів використовуються асистентами для доказів [en] та [en]. Isabelle, окрім теорій типів, також використовує теорію множин Цермело — Френкеля. [en] є прикладом системи для доказів, яка використовує тільки теорію множин.
Лінгвістика
Теорія типів також широко використовується у формальних теоріях семантики природних мов, особливо у граматиці Монтегю та її нащадків. Зокрема, категориальні граматики та граматики прегруп широко використовують конструктори типів для визначення типів слів (іменник, дієслово, тощо).
Найбільш поширена конструкція приймає базові типи та відповідно у якості індивіда та значення істинності, а потім рекурсивно визначає множину типів таким чином:
- якщо та є типами, то також типом є і ;
- типами є тільки базові типи та ті типи, які були побудовані способом, описаним у попередньому пункті.
Комплексний тип — це тип функцій від об'єктів типу до об'єктів типу . Таким чином, існують типи виду , які інтерпретуються як елементи множини функцій від об'єктів до значень істинності, тобто характеристичних функцій множин об'єктів. Вираз типу є функцією від множини об'єктів до значень істинності. Цей тип є стандартним типом кванторів природної мови, таких як всі або ніхто.
З прикладних лінгвістичних систем можна відзначити Grammatical Framework, що збудований на основі теорії типів Мартіна-Льофа.
Соціальні науки
Грегорі Бейтсон вніс теорію логічних типів до соціальних наук; його визначення подвійного послання та ґрунтуються на теорії типів Расселла.
Зв'язок з теорією категорій
Хоча початкова мотивація теорії категорій була далекою від фундаменталізму, вона мала глибокі зв'язки з теорією типів. Як писав Джон Белл: «Насправді, категорії можуть самі себе розглядати як теорії типів певного роду; цей факт сам по собі свідчить про те, що теорія типів більш тісно пов'язана з теорією категорій, ніж теорією множин.» Коротко кажучи, категорію можна розглядати як теорію типів, вважаючи її об'єкти типами. Нижче наведено ряд важливих результатів:
- декартово замкнені категорії відповідають типізованому лямбда-численню (Ламбек, 1970);
- C-моноїди (категорії з множенням, зведенням в ступінь та єдиним нетермінальним об'єктом) відповідають нетипізованому лямбда-численню (було самостійно спостережено Ламбеком та Скоттом, 1980);
- локально декартово замкнені категорії відповідають теорії типів Мартіна-Льофа (1984).
Див. також
- Тип даних — конкретні типи даних у програмуванні
- Система типізації — більш практичне обговорення систем типів для мов програмування
Примітки
- Alonzo Church, A formulation of the simple theory of types [ 15 листопада 2018 у Wayback Machine.], The Journal of Symbolic Logic 5(2):56–68 (1940)
- . ncatlab.org. Архів оригіналу за 23 лютого 2019. Процитовано 22 лютого 2019.
- John L. Bell (2012). Types, Sets and Categories. У Akihiro Kanamory (ред.). (PDF). Elsevier. ISBN . Архів оригіналу (PDF) за 17 квітня 2018. Процитовано 21 лютого 2019.
Література
- C. Aarts, R. Backhouse, P. Hoogendijk, E. Voermans & J. van der Woude (December 1992) A Relational Theory of Datatypes [ 14 вересня 2018 у Wayback Machine.] via ResearchGate
- Andrews B., Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed. Kluwer Academic Publishers. ISBN .
- Jacobs, Bart (1999). . Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN . Архів оригіналу за 26 квітня 2019. Процитовано 21 лютого 2019. Covers type theory in depth, including polymorphic and dependent type extensions. Gives .
- Cardelli, Luca, 1997, «Type Systems, [ 10 квітня 2008 у Wayback Machine.]» in Allen B. Tucker, ed., The Computer Science and Engineering Handbook. CRC Press: 2208–2236.
- Collins, Jordan E. (2012). A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'. LAP Lambert Academic Publishing. ISBN . Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'.
- , 2002, «» in H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213–259. Intended as a type theory counterpart of Paul Halmos's (1960)
- — Type Theory [Архівовано 16 липня 2013 у WebCite], Stanford Encyclopedia of Philosophy.
- Thompson, Simon, 1991. Type Theory and Functional Programming [ 23 березня 2021 у Wayback Machine.]. Addison–Wesley. .
- , Basic Simple Type Theory, Cambridge University Press, 2008, (also 1995, 1997). A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though.
- Fairouz D. Kamareddine, Twan Laan, Rob P. Nederpelt, A modern perspective on type theory: from its origins until today, Springer, 2004,
- José Ferreirós, José Ferreirós Domínguez, Labyrinth of thought: a history of set theory and its role in modern mathematics, Edition 2, Springer, 2007, , chapter X «Logic and Type Theory in the Interwar Period».
- T. D. L. Laan, The evolution of type theory in logic and mathematics [ 22 лютого 2019 у Wayback Machine.], PhD thesis, Eindhoven University of Technology, 1997.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Teoriya tipiv ce bud yaka formalna sistema sho mozhe sluguvati alternativoyu nayivnij teoriyi mnozhin U teoriyi tipiv kozhen term maye tip a operaciyi vikonuyutsya v uzgodzhenosti z cimi tipami Teoriya tipiv tisno pov yazana z sistemami tipiv osoblivistyu mov programuvannya yaka priznachena dlya zmenshennya kilkosti pomilok Teoriya tipiv bula rozroblena dlya obhodzhennya paradoksiv formalnoyi logiki Odniyeyu z najvidomishih teorij tipiv ye tipizovane lyambda chislennya Alonzo Chercha ta intuyicionistska teoriya tipiv en IstoriyaV promizhok mizh 1902 ta 1908 rokami Bertran Rassell zaproponuvav rizni teoriyi tipiv u vidpovid do jogo vidkrittya yake vstanovlyuvalo prisutnist paradoksu Rassella u nayivnij teoriyi mnozhin Gotloba Frege U 1908 roci Rassell vinajshov rozgaluzhenu teoriyu tipiv ta aksiomu redukciyi yaki buli opublikovani u praci Vajtgeda ta Rassella Principia Mathematica Voni namagalisya virishiti paradoks Rassella za dopomogoyu rozrobki iyerarhiyi tipiv ta priznachenni kozhnoyi matematichnoyi sutnosti do tipu Sutnosti kozhnogo tipu buduvalisya sutnostyami tipiv yaki roztashovani nizhche za iyerarhiyeyu sho zapobigalo priznachennyu sutnosti do samoyi sebe U 1920 h rokah Leon Hvistek ta Frenk Plampton Remzi zaproponuvali nerozgaluzhenu teoriyu tipiv yaka zaraz vidoma yak teoriya prostih tipiv abo prosta teoriya tipiv Cya teoriya ne vikoristovuvala iyerarhiyi tipiv ta yak naslidok ne vimagala aksiomi redukciyi Najvidomishim prikladom vikoristannya tipiv ye en Alonzo Chercha Teoriya tipiv Chercha dopomogla formalnim sistemam uniknuti en prisutnogo u originalnomu beztipovomu lyambda chislenni Cherch prodemonstruvav sho cya teoriya mozhe sluzhiti osnovoyu dlya matematiki Bazovi ponyattyaU sistemi teoriyi tipiv kozhen term maye tip Napriklad 4 displaystyle 4 2 2 displaystyle 2 2 ta 2 2 displaystyle 2 cdot 2 ye okremimi termami tipu nat displaystyle mathrm nat tobto naturalnimi chislami Tradicijno term suprovodzhuyetsya dvokrapkoyu i jogo tipom napriklad 2 nat displaystyle 2 mathrm nat Teoriyi tipiv mayut yavne obchislennya yake koduyetsya pravilami rerajtingu termiv Voni nazivayutsya pravilami peretvorennya abo yaksho pravilo pracyuye lishe v odnomu napryamku pravilom redukciyi Napriklad 2 2 displaystyle 2 2 ta 4 displaystyle 4 ye sintaksichno riznimi termami ale pershij term redukuyetsya do drugogo Na zapisu cya redukciya maye viglyad 2 2 4 displaystyle 2 2 twoheadrightarrow 4 Funkciyi v teoriyi tipiv mayut specialne pravilo redukciyi argument vikliku funkciyi zaminyuyetsya na kozhne vhodzhennya parametra u viznachenni funkciyi Nehaj funkciya double displaystyle mathrm double viznachena yak lx x x displaystyle lambda x x x vikoristovuyuchi lyambda notaciyu Chercha abo x x x displaystyle x mapsto x x vikoristovuyuchi bilsh suchasnu notaciyu Todi viklik funkciyi double 2 displaystyle mathrm double 2 redukuyetsya shlyahom zamini kozhnoyi kopiyi x displaystyle x termom 2 displaystyle 2 v tili viznachennya funkciyi Takim chinom double 2 2 2 displaystyle mathrm double 2 twoheadrightarrow 2 2 Tip funkciyi poznachayetsya strilkoyu displaystyle to vid tipu parametra do rezultuyuchogo tipu funkciyi Takim chinom double nat nat displaystyle mathrm double mathrm nat to mathrm nat Viklik funkciyi z deyakim argumentom mozhe buti napisanij z duzhkami abo bez nih napriklad double 2 displaystyle mathrm double 2 abo double 2 displaystyle mathrm double 2 Zazvichaj duzhki ne vikoristovuyutsya tomu sho funkciyi bagatoh argumentiv mozhut buti viznachenimi za dopomogoyu karringu Vidminnosti vid teoriyi mnozhinIsnuye bezlich riznih teorij mnozhin ta riznih sistem teoriyi tipiv Teoriya mnozhin pobudovana poverh logiki Vona vimagaye okremoyi sistemi podibnoyi logici pershogo poryadku U teoriyi tipiv ponyattya tipu i ta abo mozhut buti zakodovani yak tipi samoyi teoriyi tipiv U teoriyi mnozhin element mozhe nalezhati do bezlichi riznih mnozhin do pidmnozhini abo do mnozhini mnozhin U teoriyi tipiv termi yak pravilo nalezhat tilki do odnogo tipu Tam de vikoristovuyutsya pidmnozhini teoriya tipiv pragne vikoristovuvati funkciyu predikativ yaka povertaye true displaystyle true yaksho term znahoditsya v pidmnozhini ta povertaye false displaystyle false v inshomu vipadku Ob yednannya dvoh tipiv mozhna zrobiti stvorivshi novij tip yakij nazivayetsya tipom sumoyu ta mistit novi termi Teoriya mnozhin zazvichaj koduye chisla yak mnozhini 0 displaystyle 0 porozhnya mnozhina 1 displaystyle 1 mnozhina sho mistit porozhnyu mnozhinu i t d Teoriya tipiv mozhe koduvati chisla yak funkciyi vikoristovuyuchi en abo yak en Induktivni tipi stvoryuyut novi konstanti dlya en i nul sho duzhe nagaduye aksiomi Peano Teoriya mnozhin vikoristovuye notaciyu pobudovi mnozhini Teoriya tipiv maye proste z yednannya z konstruktivnoyu matematikoyu cherez en ta mozhe buti pov yazana z logikoyu izomorfizmiv Karri Govarda Deyaki teoriyi tipiv tisno pov yazani z teoriyeyu kategorij Dodatkovi viznachennyaNormalizaciya Term 2 1 displaystyle 2 1 redukuyetsya do 3 displaystyle 3 Tak yak 3 displaystyle 3 nadali ne redukuyetsya kazhut sho cej term znahoditsya u normalnij formi Kazhut sho sistema teoriyi tipiv silno normalizuyetsya yaksho vsi termi mayut normalnu formu ta bud yakij poryadok redukciyi dosyagaye yiyi Slabo normalizuyuchi sistemi mayut normalnu formu ale deyaki poryadki redukciyi mozhut nazavzhdi zaciklitisya ta nikoli yiyi ne dosyagnuti Inkoli viznachennya elementu zapozichuyut z teoriyi mnozhin ta vikoristovuyut jogo dlya poznachennya vsih zakritih termiv yaki redukuyutsya do odniyeyi normalnoyi formi Zakritim termom nazivayetsya term yakij ne maye parametriv Term vidu x 1 displaystyle x 1 maye parametr x displaystyle x ta nazivayetsya vidkritim termom Takim chinom 2 1 displaystyle 2 1 ta 3 0 displaystyle 3 0 ye riznimi termami ale voni obidva redukuyutsya do elementu 3 displaystyle 3 Shozhim ponyattyam yake viznachayetsya dlya zakritih ta vidkritih termiv ye ponyattya konvertovanosti Dva termi nazivayutsya konvertovanimi yaksho isnuye term do yakogo ci dva termi redukuyutsya Napriklad 2 1 displaystyle 2 1 ta 1 2 displaystyle 1 2 ye konvertovanimi Termi x 1 1 displaystyle x 1 1 ta x 2 displaystyle x 2 takozh ye konvertovanimi Odnak termi x 1 displaystyle x 1 ta 1 x displaystyle 1 x de x displaystyle x ye vilnoyu zminnoyu ne ye konvertovanimi tak yak voni znahodyatsya u normalnij formi ta ne ye odnakovimi Slabo normalizuyuchi sistemi mozhut pereviriti chi ye dva termi konvertovanimi shlyahom redukciyi cih termiv do odniyeyi normalnoyi formi Zalezhni tipi Dokladnishe Zalezhnij tip Zalezhnim tipom nazivayetsya tip yakij zalezhit vid termiv ta inshih tipiv Takim chinom tip povernutij funkciyeyu mozhe zalezhati vid argumentu funkciyi Napriklad spisok termiv tipu nat displaystyle mathrm nat iz 4 elementiv mozhe vidriznyatisya vid spisku termiv tipu nat displaystyle mathrm nat iz 5 elementiv U teoriyi tipiv z zalezhnimi tipami mozhna viznachiti funkciyu yaka prijmaye parametr n displaystyle n i povertaye spisok sho mistit n displaystyle n nuliv Tip termu porodzhenogo viklikom funkciyi z 4 displaystyle 4 vidriznyavsya bi vid tipu termu porodzhenogo viklikom funkciyi z 5 displaystyle 5 Zalezhni tipi vidigrayut centralnu rol v teoriyi tipiv Martina Lofa ta v rozrobci funkcijnih mov programuvannya takih yak en en Agda ta en Tipi rivnosti Bagato sistem teoriyi tipiv mayut tip yakij predstavlyaye rivnist tipiv ta termiv Cej tip vidriznyayetsya vid konvertovanosti ta chasto viznachayetsya yak propozicijna rivnist U teoriyi tipiv Martina Lofa tip rivnosti yakij takozh nazivayetsya tipom identichnosti poznachayetsya yak I displaystyle I vid angl Identity Kazhut sho isnuye tip I A a b displaystyle I A a b koli A displaystyle A ye tipom a a displaystyle a i b displaystyle b ce termi tipu A displaystyle A Term tipu I A a b displaystyle I A a b interpretuyetsya yak viznachennya rivnosti a displaystyle a ta b displaystyle b Na praktici mozhna pobuduvati tip I nat 3 4 displaystyle I mathrm nat 3 4 ale takij tip ne bude mati termiv U teoriyi tipiv Martina Lofa novi termi rivnosti mayut vlastivist refleksivnosti Yaksho 3 displaystyle 3 ye termom tipu nat displaystyle mathrm nat to isnuye term tipu I nat 3 3 displaystyle I mathrm nat 3 3 Bilsh skladni rivnosti mozhut buti stvoreni shlyahom stvorennya refleksivnogo termu ta jogo podalshoyi redukciyi Tobto yaksho 2 1 displaystyle 2 1 ye termom tipu nat displaystyle mathrm nat to isnuye term tipu I nat 2 1 2 1 displaystyle I mathrm nat 2 1 2 1 yakij redukuyetsya do termu tipu I nat 2 1 3 displaystyle I mathrm nat 2 1 3 Takim chinom u cij sistemi rivnist tipiv oznachaye te sho dva znachennya odnogo tipu konvertuyutsya za dopomogoyu redukciyi Nayavnist tipu rivnosti ye vazhlivim oskilki yim mozhna manipulyuvati vseredini sistemi Mi mozhemo takozh viznachiti nerivnist tipiv yak u en vidobrazhayemo a b displaystyle neg a b do a b displaystyle a b to bot Tobto isnuye term tipu I nat 3 4 displaystyle I mathrm nat 3 4 to bot ale ne isnuye termu tipu I nat 3 3 displaystyle I mathrm nat 3 3 to bot en vidriznyayetsya vid teoriyi tipiv Martina Lofa v osnovnomu tim yak v nih viznachayutsya tipi rivnosti Induktivni tipi Sistema teoriyi tipiv vimagaye deyakih bazovih termiv i tipiv dlya roboti Deyaki sistemi buduyut yih z funkcij za dopomogoyu en Inshi sistemi mayut en mnozhinu bazovih tipiv ta mnozhinu konstruktoriv tipiv yaki generuyut tipi z pravilnimi vlastivostyami Napriklad pevni rekursivni funkciyi pobudovani na induktivnih tipah garantovano pripinyayut svoyu robotu Koinduktivnij tip ce neskinchennij tip danih stvorenij shlyahom zadannya funkciyi yaka generuye nastupnij element en buduye bilsh shirokij diapazon tipiv dozvolyayuchi odnochasno viznachati tip i rekursivni funkciyi sho pracyuyut na nomu Universalnij tip Tipi buli stvoreni dlya zapobigannya paradoksiv takih yak paradoks Rassella Prote motivi yaki prizvodyat do takih paradoksiv zdatnist formulyuvati tverdzhennya pro vsi tipi vse she isnuyut Same tomu bagato teorij tipiv mayut universalnij tip yakij mistit vsi inshi tipi ale ne samogo sebe U sistemah de vi mozhete stverdzhuvati shos vidnosno universalnih tipiv isnuye iyerarhiya universalnih tipiv kozhnij z yakih mistit nizhchij za iyerarhiyeyu tip Cya iyerarhiya viznachayetsya neskinchennoyu ale stverdzhenya povinni stosuvatisya lishe kincevogo chisla universalnih rivniv Universalni tipi osoblivo skladni v teoriyi tipiv Pervisna propoziciya teoriyi tipiv Martina Lofa strazhdala vid en Obchislyuvalna skladova Bagato sistem teoriyi tipiv takih yak en teoriya tipiv Martina Lofa obchislennya konstrukcij takozh ye movami programuvannya Takim chinom kazhut sho voni mayut obchislyuvalnu skladovu Obchislennya ce redukciya termiv movi za dopomogoyu pravil rerajtingu Sistema teoriyi tipiv yaka maye yakisnu obchislyuvalnu skladovu takozh maye proste z yednannya z konstruktivnoyu matematikoyu cherez en Teoriyi tipivZnachni en yake ye en teoriya tipiv Martina Lofa sistema F obchislennya konstrukcij Drugoryadni en deyaki formi kombinatornoyi logiki en teoriyi tipiv yaki viznacheni dlya lyambda kuba tipizovane lyambda chislennya chisti sistemi tipiv Aktivni en zaraz doslidzhuyetsya Praktichne vikoristannyaMovi programuvannya Dokladnishe Sistema tipizaciyi Isnuye tisnij zv yazok mizh teoriyeyu tipiv ta sistemami tipizaciyi Sistemi tipiv ye osoblivistyu mov programuvannya priznachenoyi dlya viyavlennya pomilok Bud yakij statichnij analiz programi takij yak algoritmi perevirki tipu v fazi semantichnogo analizu kompilyatorom maye zv yazok z teoriyeyu tipiv Yaskravim prikladom ye Agda mova programuvannya sho vikoristovuye teoriyu tipiv Martina Lofa u yakosti svoyeyi sistemi tipiv Mova programuvannya ML bula rozroblena dlya manipulyuvannya teoriyami tipiv ta yiyi vlasna sistema tipiv bula pid silnim vplivom teoriyi tipiv Matematichni osnovi Pershij komp yuternij asistent nazivavsya en vikoristovuvav teoriyu tipiv dlya koduvannya matematiki na komp yuteri en specialno rozrobiv teoriyu tipiv shob koduvati vsyu matematiku dlya rozrobki novih matematichnih osnov Isnuye doslidzhennya matematichnih osnov z vikoristannyam en Matematiki sho pracyuyut z teoriyeyu kategorij vzhe mali trudnoshi pri roboti z shiroko poshirenoyu teoriyeyu mnozhin Cermelo Frenkelya Ce prizvelo do takih propozicij yak elementarna teoriya kategorij mnozhin ETCS Uilyama Lovera Doslidniki vivchayut zv yazki mizh zalezhnimi tipami osoblivo tipom identichnosti ta algebrichnoyu topologiyeyu zokrema gomotopiyeyu Asistenti dlya dokaziv Znachna chastina suchasnih doslidzhen teoriyi tipiv provoditsya dlya rozvitku avtomatizovanoyi perevirki dokaziv interaktivnih asistentiv dlya dokaziv ta avtomatizovanih dokaziv teorem Bilshist cih sistem vikoristovuyut teoriyu tipiv yak matematichnu osnovu dlya koduvannya dokaziv sho ne divno vrahovuyuchi tisnij zv yazok mizh teoriyeyu tipiv i movami programuvannya Bagato teorij tipiv pobudovanih na en vikoristovuyutsya dlya sistem en and en teoriya tipiv Martina Lofa vikoristovuyetsya Agda movoyu programuvannya ta asistentom dlya dokaziv obchislyuvalna teoriya tipiv vikoristovuyetsya en obchislennya konstrukcij vikoristovuyetsya Coq ta en Bagato teorij tipiv vikoristovuyutsya asistentami dlya dokaziv en ta en Isabelle okrim teorij tipiv takozh vikoristovuye teoriyu mnozhin Cermelo Frenkelya en ye prikladom sistemi dlya dokaziv yaka vikoristovuye tilki teoriyu mnozhin Lingvistika Teoriya tipiv takozh shiroko vikoristovuyetsya u formalnih teoriyah semantiki prirodnih mov osoblivo u gramatici Montegyu ta yiyi nashadkiv Zokrema kategorialni gramatiki ta gramatiki pregrup shiroko vikoristovuyut konstruktori tipiv dlya viznachennya tipiv sliv imennik diyeslovo tosho Najbilsh poshirena konstrukciya prijmaye bazovi tipi e displaystyle e ta t displaystyle t vidpovidno u yakosti individa ta znachennya istinnosti a potim rekursivno viznachaye mnozhinu tipiv takim chinom yaksho a displaystyle a ta b displaystyle b ye tipami to takozh tipom ye i a b displaystyle langle a b rangle tipami ye tilki bazovi tipi ta ti tipi yaki buli pobudovani sposobom opisanim u poperednomu punkti Kompleksnij tip a b displaystyle langle a b rangle ce tip funkcij vid ob yektiv tipu a displaystyle a do ob yektiv tipu b displaystyle b Takim chinom isnuyut tipi vidu e t displaystyle langle e t rangle yaki interpretuyutsya yak elementi mnozhini funkcij vid ob yektiv do znachen istinnosti tobto harakteristichnih funkcij mnozhin ob yektiv Viraz tipu e t t displaystyle langle langle e t rangle t rangle ye funkciyeyu vid mnozhini ob yektiv do znachen istinnosti Cej tip ye standartnim tipom kvantoriv prirodnoyi movi takih yak vsi abo nihto Z prikladnih lingvistichnih sistem mozhna vidznachiti Grammatical Framework sho zbudovanij na osnovi teoriyi tipiv Martina Lofa Socialni nauki Gregori Bejtson vnis teoriyu logichnih tipiv do socialnih nauk jogo viznachennya podvijnogo poslannya ta gruntuyutsya na teoriyi tipiv Rassella Zv yazok z teoriyeyu kategorijHocha pochatkova motivaciya teoriyi kategorij bula dalekoyu vid fundamentalizmu vona mala gliboki zv yazki z teoriyeyu tipiv Yak pisav Dzhon Bell Naspravdi kategoriyi mozhut sami sebe rozglyadati yak teoriyi tipiv pevnogo rodu cej fakt sam po sobi svidchit pro te sho teoriya tipiv bilsh tisno pov yazana z teoriyeyu kategorij nizh teoriyeyu mnozhin Korotko kazhuchi kategoriyu mozhna rozglyadati yak teoriyu tipiv vvazhayuchi yiyi ob yekti tipami Nizhche navedeno ryad vazhlivih rezultativ dekartovo zamkneni kategoriyi vidpovidayut tipizovanomu lyambda chislennyu Lambek 1970 C monoyidi kategoriyi z mnozhennyam zvedennyam v stupin ta yedinim neterminalnim ob yektom vidpovidayut netipizovanomu lyambda chislennyu bulo samostijno sposterezheno Lambekom ta Skottom 1980 lokalno dekartovo zamkneni kategoriyi vidpovidayut teoriyi tipiv Martina Lofa 1984 Div takozhTip danih konkretni tipi danih u programuvanni Sistema tipizaciyi bilsh praktichne obgovorennya sistem tipiv dlya mov programuvannyaPrimitkiAlonzo Church A formulation of the simple theory of types 15 listopada 2018 u Wayback Machine The Journal of Symbolic Logic 5 2 56 68 1940 ncatlab org Arhiv originalu za 23 lyutogo 2019 Procitovano 22 lyutogo 2019 John L Bell 2012 Types Sets and Categories U Akihiro Kanamory red PDF Elsevier ISBN 978 0 08 093066 4 Arhiv originalu PDF za 17 kvitnya 2018 Procitovano 21 lyutogo 2019 LiteraturaC Aarts R Backhouse P Hoogendijk E Voermans amp J van der Woude December 1992 A Relational Theory of Datatypes 14 veresnya 2018 u Wayback Machine via ResearchGate Andrews B Peter 2002 An Introduction to Mathematical Logic and Type Theory To Truth Through Proof 2nd ed Kluwer Academic Publishers ISBN 978 1 4020 0763 7 Jacobs Bart 1999 Studies in Logic and the Foundations of Mathematics 141 North Holland Elsevier ISBN 0 444 50170 3 Arhiv originalu za 26 kvitnya 2019 Procitovano 21 lyutogo 2019 Covers type theory in depth including polymorphic and dependent type extensions Gives Cardelli Luca 1997 Type Systems 10 kvitnya 2008 u Wayback Machine in Allen B Tucker ed The Computer Science and Engineering Handbook CRC Press 2208 2236 Collins Jordan E 2012 A History of the Theory of Types Developments After the Second Edition of Principia Mathematica LAP Lambert Academic Publishing ISBN 978 3 8473 2963 3 Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of Principia Mathematica 2002 in H Schwichtenberg and R Steinbruggen eds Proof and System Reliability 213 259 Intended as a type theory counterpart of Paul Halmos s 1960 Type Theory Arhivovano 16 lipnya 2013 u WebCite Stanford Encyclopedia of Philosophy Thompson Simon 1991 Type Theory and Functional Programming 23 bereznya 2021 u Wayback Machine Addison Wesley ISBN 0 201 41667 0 Basic Simple Type Theory Cambridge University Press 2008 ISBN 0 521 05422 2 also 1995 1997 A good introduction to simple type theory for computer scientists the system described is not exactly Church s STT though Fairouz D Kamareddine Twan Laan Rob P Nederpelt A modern perspective on type theory from its origins until today Springer 2004 ISBN 1 4020 2334 0 Jose Ferreiros Jose Ferreiros Dominguez Labyrinth of thought a history of set theory and its role in modern mathematics Edition 2 Springer 2007 ISBN 3 7643 8349 6 chapter X Logic and Type Theory in the Interwar Period T D L Laan The evolution of type theory in logic and mathematics 22 lyutogo 2019 u Wayback Machine PhD thesis Eindhoven University of Technology 1997