www.wikidata.uk-ua.nina.az

Теорія типів це будь яка формальна система що може слугувати альтернативою наївній теорії множин У теорії типів кожен те

Теорія типів

Теорія типів — це будь-яка формальна система, що може слугувати альтернативою наївній теорії множин. У теорії типів кожен «терм» має «тип», а операції виконуються в узгодженості з цими типами.

Теорія типів тісно пов'язана з системами типів — особливістю мов програмування, яка призначена для зменшення кількості помилок. Теорія типів була розроблена для обходження парадоксів формальної логіки.

Однією з найвідоміших теорій типів є типізоване лямбда-числення Алонзо Черча та інтуїціоністська теорія типів Пера Мартіна-Льофа[en].

Історія Редагувати

В проміжок між 1902 та 1908 роками Бертран Расселл запропонував різні теорії типів у відповідь до його відкриття, яке встановлювало присутність парадоксу Расселла у наївній теорії множин Готлоба Фреге. У 1908 році Расселл винайшов «розгалужену» теорію типів та «аксіому редукції», які були опубліковані у праці Вайтгеда та Расселла «Principia Mathematica». Вони намагалися вирішити парадокс Расселла за допомогою розробки ієрархії типів та призначенні кожної математичної сутності до типу. Сутності кожного типу будувалися сутностями типів, які розташовані нижче за ієрархією, що запобігало призначенню сутності до самої себе. У 1920-х роках Леон Хвістек та Френк Пламптон Ремзі запропонували нерозгалужену теорію типів, яка зараз відома як «теорія простих типів» або «проста теорія типів». Ця теорія не використовувала ієрархії типів та, як наслідок, не вимагала аксіоми редукції.

Найвідомішим прикладом використання типів є просто типізоване лямбда-числення[en] Алонзо Черча. Теорія типів Черча допомогла формальним системам уникнути парадоксу Кліні — Россера[en], присутнього у оригінальному безтиповому лямбда-численню. Черч продемонстрував, що ця теорія може служити основою для математики.

Базові поняття Редагувати

У системі теорії типів кожен терм має тип. Наприклад, , та є окремими термами типу , тобто натуральними числами. Традиційно терм супроводжується двокрапкою і його типом, наприклад, .

Теорії типів мають явне обчислення, яке кодується правилами рерайтингу термів. Вони називаються правилами перетворення або, якщо правило працює лише в одному напрямку, правилом редукції. Наприклад, та є синтаксично різними термами, але перший терм редукується до другого. На запису ця редукція має вигляд .

Функції в теорії типів мають спеціальне правило редукції: аргумент виклику функції замінюється на кожне входження параметра у визначенні функції. Нехай функція визначена як (використовуючи лямбда нотацію Черча) або (використовуючи більш сучасну нотацію). Тоді виклик функції редукується шляхом заміни кожної копії термом в тілі визначення функції. Таким чином, .

Тип функції позначається стрілкою від типу параметра до результуючого типу функції. Таким чином, . Виклик функції з деяким аргументом може бути написаний з дужками або без них, наприклад, або . Зазвичай дужки не використовуються, тому що функції багатьох аргументів можуть бути визначеними за допомогою каррінгу.

Відмінності від теорії множин Редагувати

Існує безліч різних теорій множин та різних систем теорії типів.

  • Теорія множин побудована поверх логіки. Вона вимагає окремої системи, подібної логіці першого порядку. У теорії типів поняття типу «і» та «або» можуть бути закодовані як типи самої теорії типів.
  • У теорії множин елемент може належати до безлічі різних множин, до підмножини, або до множини множин. У теорії типів терми, як правило, належать тільки до одного типу. (Там, де використовуються підмножини, теорія типів прагне використовувати функцію предикатів, яка повертає , якщо терм знаходиться в підмножині, та повертає в іншому випадку. Об'єднання двох типів можна зробити, створивши новий тип, який називається типом-сумою та містить нові терми.)
  • Теорія множин зазвичай кодує числа як множини. ( — порожня множина,  — множина, що містить порожню множину, і т. д.) Теорія типів може кодувати числа як функції, використовуючи кодування Черча[en], або як індуктивні типи[en]. Індуктивні типи створюють нові константи для функції наступника[en] і нуль, що дуже нагадує аксіоми Пеано.
  • Теорія множин використовує нотацію побудови множини.
  • Теорія типів має просте з'єднання з конструктивною математикою через інтерпретацію Брауера — Гейтінга — Колмогорова[en] та може бути пов'язана з логікою ізоморфізмів Каррі — Говарда. Деякі теорії типів тісно пов'язані з теорією категорій.

Додаткові визначення Редагувати

Нормалізація Редагувати

Терм редукується до . Так як надалі не редукується, кажуть, що цей терм знаходиться у нормальній формі. Кажуть, що система теорії типів сильно нормалізується, якщо всі терми мають нормальну форму та будь-який порядок редукції досягає її. Слабо нормалізуючи системи мають нормальну форму, але деякі порядки редукції можуть назавжди зациклитися та ніколи її не досягнути.

Інколи визначення елементу запозичують з теорії множин та використовують його для позначення всіх закритих термів, які редукуються до однієї нормальної форми. Закритим термом називається терм, який не має параметрів. Терм виду має параметр та називається відкритим термом. Таким чином, та є різними термами, але вони обидва редукуються до елементу .

Схожим поняттям, яке визначається для закритих та відкритих термів, є поняття конвертованості. Два терми називаються конвертованими, якщо існує терм, до якого ці два терми редукуються. Наприклад, та є конвертованими. Терми та також є конвертованими. Однак терми та (де є вільною змінною) не є конвертованими, так як вони знаходяться у нормальній формі та не є однаковими. Слабо нормалізуючі системи можуть перевірити, чи є два терми конвертованими, шляхом редукції цих термів до однієї нормальної форми.

Залежні типи Редагувати

Залежним типом називається тип, який залежить від термів та інших типів. Таким чином, тип, повернутий функцією, може залежати від аргументу функції.

Наприклад, список термів типу із 4 елементів може відрізнятися від списку термів типу із 5 елементів. У теорії типів з залежними типами можна визначити функцію, яка приймає параметр і повертає список, що містить нулів. Тип терму, породженого викликом функції з , відрізнявся би від типу терму, породженого викликом функції з .

Залежні типи відіграють центральну роль в теорії типів Мартіна-Льофа та в розробці функційних мов програмування, таких як Idris[en], ATS[en], Agda та Epigram [en].

Типи рівності Редагувати

Багато систем теорії типів мають тип, який представляє рівність типів та термів. Цей тип відрізняється від конвертованості та часто визначається як пропозиційна рівність.

У теорії типів Мартіна-Льофа тип рівності (який також називається типом ідентичності) позначається як (від англ. Identity). Кажуть, що існує тип , коли є типом, а і  — це терми типу . Терм типу інтерпретується як визначення рівності та .

На практиці можна побудувати тип , але такий тип не буде мати термів. У теорії типів Мартіна-Льофа нові терми рівності мають властивість рефлексивності. Якщо є термом типу , то існує терм типу . Більш складні рівності можуть бути створені шляхом створення рефлексивного терму та його подальшої редукції. Тобто якщо є термом типу , то існує терм типу , який редукується до терму типу . Таким чином, у цій системі рівність типів означає те, що два значення одного типу конвертуються за допомогою редукції.

Наявність типу рівності є важливим, оскільки їм можна маніпулювати всередині системи. Ми можемо також визначити нерівність типів: як у інтерпретації Брауера — Гейтінга — Колмогорова[en], відображаємо до . Тобто існує терм типу , але не існує терму типу .

Гомотопічна теорія типів[en] відрізняється від теорії типів Мартіна-Льофа в основному тим, як в них визначаються типи рівності.

Індуктивні типи Редагувати

Система теорії типів вимагає деяких базових термів і типів для роботи. Деякі системи будують їх з функцій за допомогою кодування Черча[en]. Інші системи мають індуктивні типи[en]: множину базових типів та множину конструкторів типів, які генерують типи з правильними властивостями. Наприклад, певні рекурсивні функції, побудовані на індуктивних типах, гарантовано припиняють свою роботу.

Коіндуктивний тип — це нескінченний тип даних, створений шляхом задання функції, яка генерує наступний елемент.

Індукційна рекурсія[en] будує більш широкий діапазон типів, дозволяючи одночасно визначати тип і рекурсивні функції, що працюють на ньому.

Універсальний тип Редагувати

Типи були створені для запобігання парадоксів, таких як парадокс Расселла. Проте мотиви, які призводять до таких парадоксів (здатність формулювати твердження про всі типи) все ще існують. Саме тому багато теорій типів мають «універсальний» тип, який містить всі інші типи (але не самого себе).

У системах, де ви можете стверджувати щось відносно універсальних типів, існує ієрархія універсальних типів, кожний з яких містить нижчий за ієрархією тип. Ця ієрархія визначається нескінченною, але ствердженя повинні стосуватися лише кінцевого числа універсальних рівнів.

Універсальні типи особливо складні в теорії типів. Первісна пропозиція теорії типів Мартіна-Льофа страждала від парадоксу Жирара[en].

Обчислювальна складова Редагувати

Багато систем теорії типів, таких як просто типізоване лямбда-обчислення[en], теорія типів Мартіна-Льофа, обчислення конструкцій, також є мовами програмування. Таким чином, кажуть, що вони мають «обчислювальну складову». Обчислення — це редукція термів мови за допомогою правил рерайтингу.

Система теорії типів, яка має якісну обчислювальну складову, також має просте з'єднання з конструктивною математикою через інтерпретацію Брауера — Гейтінга — Колмогорова[en].

Теорії типів Редагувати

Значні Редагувати

Другорядні Редагувати

Активні Редагувати

  • Гомотопічна теорія типів[en] зараз досліджується.

Практичне використання Редагувати

Мови програмування Редагувати

Існує тісний зв'язок між теорією типів та системами типізації. Системи типів є особливістю мов програмування, призначеної для виявлення помилок. Будь-який статичний аналіз програми, такий як алгоритми перевірки типу в фазі семантичного аналізу компілятором, має зв'язок з теорією типів.

Яскравим прикладом є Agda — мова програмування, що використовує теорію типів Мартіна-Льофа у якості своєї системи типів. Мова програмування ML була розроблена для маніпулювання теоріями типів та її власна система типів була під сильним впливом теорії типів.

Математичні основи Редагувати

Перший комп'ютерний асистент, називався Automath[en], використовував теорію типів для кодування математики на комп'ютері. Мартін-Льоф[en] спеціально розробив теорію типів, щоб кодувати всю математику для розробки нових математичних основ. Існує дослідження математичних основ з використанням гомотопічної теорії типів[en].

Математики, що працюють з теорією категорій, вже мали труднощі при роботі з широко поширеною теорією множин Цермело — Френкеля. Це призвело до таких пропозицій, як елементарна теорія категорій множин (ETCS) Уільяма Ловера. Дослідники вивчають зв'язки між залежними типами (особливо типом ідентичності) та алгебричною топологією (зокрема гомотопією).

Асистенти для доказів Редагувати

Значна частина сучасних досліджень теорії типів проводиться для розвитку автоматизованої перевірки доказів, інтерактивних асистентів для доказів та автоматизованих доказів теорем. Більшість цих систем використовують теорію типів як математичну основу для кодування доказів, що не дивно, враховуючи тісний зв'язок між теорією типів і мовами програмування:

  • Багато теорій типів, побудованих на логіці вищого порядку[en], використовуються для систем HOL[en] and Prototype Verification System[en];
  • теорія типів Мартіна-Льофа використовується Agda — мовою програмування та асистентом для доказів;
  • обчислювальна теорія типів використовується NuPRL[en];
  • обчислення конструкцій використовується Coq та Matita[en].

Багато теорій типів використовуються асистентами для доказів LEGO[en] та Isabelle[en]. Isabelle, окрім теорій типів, також використовує теорію множин Цермело — Френкеля. Mizar[en] є прикладом системи для доказів, яка використовує тільки теорію множин.

Лінгвістика Редагувати

Теорія типів також широко використовується у формальних теоріях семантики природних мов, особливо у граматиці Монтегю та її нащадків. Зокрема, категориальні граматики та граматики прегруп широко використовують конструктори типів для визначення типів слів (іменник, дієслово, тощо).

Найбільш поширена конструкція приймає базові типи та відповідно у якості індивіда та значення істинності, а потім рекурсивно визначає множину типів таким чином:

  • якщо та є типами, то також типом є і ;
  • типами є тільки базові типи та ті типи, які були побудовані способом, описаним у попередньому пункті.

Комплексний тип  — це тип функцій від об'єктів типу до об'єктів типу . Таким чином, існують типи виду , які інтерпретуються як елементи множини функцій від об'єктів до значень істинності, тобто характеристичних функцій множин об'єктів. Вираз типу є функцією від множини об'єктів до значень істинності. Цей тип є стандартним типом кванторів природної мови, таких як всі або ніхто.

З прикладних лінгвістичних систем можна відзначити логічний фреймворк Grammatical Framework, що збудований на основі теорії типів Мартіна-Льофа.

Соціальні науки Редагувати

Грегорі Бейтсон вніс теорію логічних типів до соціальних наук; його визначення подвійного послання та логічних рівнів ґрунтуються на теорії типів Расселла.

Зв'язок з теорією категорій Редагувати

Хоча початкова мотивація теорії категорій була далекою від фундаменталізму, вона мала глибокі зв'язки з теорією типів. Як писав Джон Белл: «Насправді, категорії можуть самі себе розглядати як теорії типів певного роду; цей факт сам по собі свідчить про те, що теорія типів більш тісно пов'язана з теорією категорій, ніж теорією множин.» Коротко кажучи, категорію можна розглядати як теорію типів, вважаючи її об'єкти типами. Нижче наведено ряд важливих результатів:

  • декартово замкнені категорії відповідають типізованому лямбда-численню (Ламбек, 1970);
  • C-моноїди (категорії з множенням, зведенням в ступінь та єдиним нетермінальним об'єктом) відповідають нетипізованому лямбда-численню (було самостійно спостережено Ламбеком та Скоттом, 1980);
  • локально декартово замкнені категорії відповідають теорії типів Мартіна-Льофа (1984).

Див. також Редагувати

Примітки Редагувати

  1. Alonzo Church, A formulation of the simple theory of types [ 15 листопада 2018 у Wayback Machine.], The Journal of Symbolic Logic 5(2):56–68 (1940)
  2. . ncatlab.org. Архів оригіналу за 23 лютого 2019. Процитовано 22 лютого 2019. 
  3. John L. Bell (2012). . У Akihiro Kanamory. Handbook of the History of Logic. Volume 6. Sets and Extensions in the Twentieth Century. Elsevier. ISBN 978-0-08-093066-4. Архів оригіналу за 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 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. Архів оригіналу за 26 квітня 2019. Процитовано 21 лютого 2019.  Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
  • 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 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'.
  • Constable, Robert L., 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) Naïve Set Theory
  • Thierry Coquand — Type Theory [Архівовано 16 липня 2013 у WebCite], Stanford Encyclopedia of Philosophy.
  • Thompson, Simon, 1991. Type Theory and Functional Programming [ 23 березня 2021 у Wayback Machine.]. Addison–Wesley. ISBN 0-201-41667-0.
  • J. Roger Hindley, 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
  • 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, 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 лютого 2019 у Wayback Machine.], PhD thesis, Eindhoven University of Technology, 1997.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри
Дата публікації:
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 Pera Martina Lofa en Zmist 1 Istoriya 2 Bazovi ponyattya 3 Vidminnosti vid teoriyi mnozhin 4 Dodatkovi viznachennya 4 1 Normalizaciya 4 2 Zalezhni tipi 4 3 Tipi rivnosti 4 4 Induktivni tipi 4 5 Universalnij tip 4 6 Obchislyuvalna skladova 5 Teoriyi tipiv 5 1 Znachni 5 2 Drugoryadni 5 3 Aktivni 6 Praktichne vikoristannya 6 1 Movi programuvannya 6 2 Matematichni osnovi 6 3 Asistenti dlya dokaziv 6 4 Lingvistika 6 5 Socialni nauki 7 Zv yazok z teoriyeyu kategorij 8 Div takozh 9 Primitki 10 LiteraturaIstoriya RedaguvatiV 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 prosto tipizovane lyambda chislennya en Alonzo Chercha Teoriya tipiv Chercha 1 dopomogla formalnim sistemam uniknuti paradoksu Klini Rossera en prisutnogo u originalnomu beztipovomu lyambda chislennyu Cherch prodemonstruvav sho cya teoriya mozhe sluzhiti osnovoyu dlya matematiki Bazovi ponyattya RedaguvatiU sistemi teoriyi tipiv kozhen term maye tip Napriklad 4 displaystyle 4 nbsp 2 2 displaystyle 2 2 nbsp ta 2 2 displaystyle 2 cdot 2 nbsp ye okremimi termami tipu n a t displaystyle mathrm nat nbsp tobto naturalnimi chislami Tradicijno term suprovodzhuyetsya dvokrapkoyu i jogo tipom napriklad 2 n a t displaystyle 2 mathrm nat nbsp 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 nbsp ta 4 displaystyle 4 nbsp ye sintaksichno riznimi termami ale pershij term redukuyetsya do drugogo Na zapisu cya redukciya maye viglyad 2 2 4 displaystyle 2 2 twoheadrightarrow 4 nbsp Funkciyi v teoriyi tipiv mayut specialne pravilo redukciyi argument vikliku funkciyi zaminyuyetsya na kozhne vhodzhennya parametra u viznachenni funkciyi Nehaj funkciya d o u b l e displaystyle mathrm double nbsp viznachena yak l x x x displaystyle lambda x x x nbsp vikoristovuyuchi lyambda notaciyu Chercha abo x x x displaystyle x mapsto x x nbsp vikoristovuyuchi bilsh suchasnu notaciyu Todi viklik funkciyi d o u b l e 2 displaystyle mathrm double 2 nbsp redukuyetsya shlyahom zamini kozhnoyi kopiyi x displaystyle x nbsp termom 2 displaystyle 2 nbsp v tili viznachennya funkciyi Takim chinom d o u b l e 2 2 2 displaystyle mathrm double 2 twoheadrightarrow 2 2 nbsp Tip funkciyi poznachayetsya strilkoyu displaystyle to nbsp vid tipu parametra do rezultuyuchogo tipu funkciyi Takim chinom d o u b l e n a t n a t displaystyle mathrm double mathrm nat to mathrm nat nbsp Viklik funkciyi z deyakim argumentom mozhe buti napisanij z duzhkami abo bez nih napriklad d o u b l e 2 displaystyle mathrm double 2 nbsp abo d o u b l e 2 displaystyle mathrm double 2 nbsp Zazvichaj duzhki ne vikoristovuyutsya tomu sho funkciyi bagatoh argumentiv mozhut buti viznachenimi za dopomogoyu karringu Vidminnosti vid teoriyi mnozhin RedaguvatiIsnuye 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 t r u e displaystyle true nbsp yaksho term znahoditsya v pidmnozhini ta povertaye f a l s e displaystyle false nbsp 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 nbsp porozhnya mnozhina 1 displaystyle 1 nbsp mnozhina sho mistit porozhnyu mnozhinu i t d Teoriya tipiv mozhe koduvati chisla yak funkciyi vikoristovuyuchi koduvannya Chercha en abo yak induktivni tipi en Induktivni tipi stvoryuyut novi konstanti dlya funkciyi nastupnika en i nul sho duzhe nagaduye aksiomi Peano Teoriya mnozhin vikoristovuye notaciyu pobudovi mnozhini Teoriya tipiv maye proste z yednannya z konstruktivnoyu matematikoyu cherez interpretaciyu Brauera Gejtinga Kolmogorova en ta mozhe buti pov yazana z logikoyu izomorfizmiv Karri Govarda Deyaki teoriyi tipiv tisno pov yazani z teoriyeyu kategorij Dodatkovi viznachennya RedaguvatiNormalizaciya Redaguvati Term 2 1 displaystyle 2 1 nbsp redukuyetsya do 3 displaystyle 3 nbsp Tak yak 3 displaystyle 3 nbsp 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 nbsp maye parametr x displaystyle x nbsp ta nazivayetsya vidkritim termom Takim chinom 2 1 displaystyle 2 1 nbsp ta 3 0 displaystyle 3 0 nbsp ye riznimi termami ale voni obidva redukuyutsya do elementu 3 displaystyle 3 nbsp 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 nbsp ta 1 2 displaystyle 1 2 nbsp ye konvertovanimi Termi x 1 1 displaystyle x 1 1 nbsp ta x 2 displaystyle x 2 nbsp takozh ye konvertovanimi Odnak termi x 1 displaystyle x 1 nbsp ta 1 x displaystyle 1 x nbsp de x displaystyle x nbsp 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 Redaguvati Dokladnishe Zalezhnij tipZalezhnim tipom nazivayetsya tip yakij zalezhit vid termiv ta inshih tipiv Takim chinom tip povernutij funkciyeyu mozhe zalezhati vid argumentu funkciyi Napriklad spisok termiv tipu n a t displaystyle mathrm nat nbsp iz 4 elementiv mozhe vidriznyatisya vid spisku termiv tipu n a t displaystyle mathrm nat nbsp iz 5 elementiv U teoriyi tipiv z zalezhnimi tipami mozhna viznachiti funkciyu yaka prijmaye parametr n displaystyle n nbsp i povertaye spisok sho mistit n displaystyle n nbsp nuliv Tip termu porodzhenogo viklikom funkciyi z 4 displaystyle 4 nbsp vidriznyavsya bi vid tipu termu porodzhenogo viklikom funkciyi z 5 displaystyle 5 nbsp Zalezhni tipi vidigrayut centralnu rol v teoriyi tipiv Martina Lofa ta v rozrobci funkcijnih mov programuvannya takih yak Idris en ATS en Agda ta Epigram en Tipi rivnosti Redaguvati 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 nbsp vid angl Identity Kazhut sho isnuye tip I A a b displaystyle I A a b nbsp koli A displaystyle A nbsp ye tipom a a displaystyle a nbsp i b displaystyle b nbsp ce termi tipu A displaystyle A nbsp Term tipu I A a b displaystyle I A a b nbsp interpretuyetsya yak viznachennya rivnosti a displaystyle a nbsp ta b displaystyle b nbsp Na praktici mozhna pobuduvati tip I n a t 3 4 displaystyle I mathrm nat 3 4 nbsp ale takij tip ne bude mati termiv U teoriyi tipiv Martina Lofa novi termi rivnosti mayut vlastivist refleksivnosti Yaksho 3 displaystyle 3 nbsp ye termom tipu n a t displaystyle mathrm nat nbsp to isnuye term tipu I n a t 3 3 displaystyle I mathrm nat 3 3 nbsp Bilsh skladni rivnosti mozhut buti stvoreni shlyahom stvorennya refleksivnogo termu ta jogo podalshoyi redukciyi Tobto yaksho 2 1 displaystyle 2 1 nbsp ye termom tipu n a t displaystyle mathrm nat nbsp to isnuye term tipu I n a t 2 1 2 1 displaystyle I mathrm nat 2 1 2 1 nbsp yakij redukuyetsya do termu tipu I n a t 2 1 3 displaystyle I mathrm nat 2 1 3 nbsp 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 interpretaciyi Brauera Gejtinga Kolmogorova en vidobrazhayemo a b displaystyle neg a b nbsp do a b displaystyle a b to bot nbsp Tobto isnuye term tipu I n a t 3 4 displaystyle I mathrm nat 3 4 to bot nbsp ale ne isnuye termu tipu I n a t 3 3 displaystyle I mathrm nat 3 3 to bot nbsp Gomotopichna teoriya tipiv en vidriznyayetsya vid teoriyi tipiv Martina Lofa v osnovnomu tim yak v nih viznachayutsya tipi rivnosti Induktivni tipi Redaguvati Sistema teoriyi tipiv vimagaye deyakih bazovih termiv i tipiv dlya roboti Deyaki sistemi buduyut yih z funkcij za dopomogoyu koduvannya Chercha en Inshi sistemi mayut induktivni tipi 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 Indukcijna rekursiya en buduye bilsh shirokij diapazon tipiv dozvolyayuchi odnochasno viznachati tip i rekursivni funkciyi sho pracyuyut na nomu Universalnij tip Redaguvati 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 paradoksu Zhirara en Obchislyuvalna skladova Redaguvati Bagato sistem teoriyi tipiv takih yak prosto tipizovane lyambda obchislennya 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 interpretaciyu Brauera Gejtinga Kolmogorova en Teoriyi tipiv RedaguvatiZnachni Redaguvati Prosto tipizovane lyambda chislennya en yake ye logikoyu vishogo poryadku en teoriya tipiv Martina Lofa sistema F obchislennya konstrukcij Drugoryadni Redaguvati Automath en deyaki formi kombinatornoyi logiki teoriya tipiv ST en teoriyi tipiv yaki viznacheni dlya lyambda kuba tipizovane lyambda chislennya chisti sistemi tipiv Aktivni Redaguvati Gomotopichna teoriya tipiv en zaraz doslidzhuyetsya Praktichne vikoristannya RedaguvatiMovi programuvannya Redaguvati Dokladnishe Sistema tipizaciyiIsnuye 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 Redaguvati Pershij komp yuternij asistent nazivavsya Automath en vikoristovuvav teoriyu tipiv dlya koduvannya matematiki na komp yuteri Martin Lof en specialno rozrobiv teoriyu tipiv shob koduvati vsyu matematiku dlya rozrobki novih matematichnih osnov Isnuye doslidzhennya matematichnih osnov z vikoristannyam gomotopichnoyi teoriyi tipiv 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 2 Uilyama Lovera Doslidniki vivchayut zv yazki mizh zalezhnimi tipami osoblivo tipom identichnosti ta algebrichnoyu topologiyeyu zokrema gomotopiyeyu Asistenti dlya dokaziv Redaguvati 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 logici vishogo poryadku en vikoristovuyutsya dlya sistem HOL en and Prototype Verification System en teoriya tipiv Martina Lofa vikoristovuyetsya Agda movoyu programuvannya ta asistentom dlya dokaziv obchislyuvalna teoriya tipiv vikoristovuyetsya NuPRL en obchislennya konstrukcij vikoristovuyetsya Coq ta Matita en Bagato teorij tipiv vikoristovuyutsya asistentami dlya dokaziv LEGO en ta Isabelle en Isabelle okrim teorij tipiv takozh vikoristovuye teoriyu mnozhin Cermelo Frenkelya Mizar en ye prikladom sistemi dlya dokaziv yaka vikoristovuye tilki teoriyu mnozhin Lingvistika Redaguvati 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 nbsp ta t displaystyle t nbsp vidpovidno u yakosti individa ta znachennya istinnosti a potim rekursivno viznachaye mnozhinu tipiv takim chinom yaksho a displaystyle a nbsp ta b displaystyle b nbsp ye tipami to takozh tipom ye i a b displaystyle langle a b rangle nbsp 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 nbsp ce tip funkcij vid ob yektiv tipu a displaystyle a nbsp do ob yektiv tipu b displaystyle b nbsp Takim chinom isnuyut tipi vidu e t displaystyle langle e t rangle nbsp 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 nbsp 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 logichnij frejmvork Grammatical Framework sho zbudovanij na osnovi teoriyi tipiv Martina Lofa Socialni nauki Redaguvati Gregori Bejtson vnis teoriyu logichnih tipiv do socialnih nauk jogo viznachennya podvijnogo poslannya ta logichnih rivniv gruntuyutsya na teoriyi tipiv Rassella Zv yazok z teoriyeyu kategorij RedaguvatiHocha 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 3 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 takozh RedaguvatiTip danih konkretni tipi danih u programuvanni Sistema tipizaciyi bilsh praktichne obgovorennya sistem tipiv dlya mov programuvannyaPrimitki Redaguvati Alonzo Church A formulation of the simple theory of types Arhivovano 15 listopada 2018 u Wayback Machine The Journal of Symbolic Logic 5 2 56 68 1940 ETCS in nLab ncatlab org Arhiv originalu za 23 lyutogo 2019 Procitovano 22 lyutogo 2019 John L Bell 2012 Types Sets and Categories U Akihiro Kanamory Handbook of the History of Logic Volume 6 Sets and Extensions in the Twentieth Century Elsevier ISBN 978 0 08 093066 4 Arhiv originalu za 17 kvitnya 2018 Procitovano 21 lyutogo 2019 Literatura RedaguvatiC Aarts R Backhouse P Hoogendijk E Voermans amp J van der Woude December 1992 A Relational Theory of Datatypes Arhivovano 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 Categorical Logic and Type Theory 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 categorical semantics Cardelli Luca 1997 Type Systems Arhivovano 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 Constable Robert L 2002 Naive Computational Type Theory in H Schwichtenberg and R Steinbruggen eds Proof and System Reliability 213 259 Intended as a type theory counterpart of Paul Halmos s 1960 Naive Set Theory Thierry Coquand Type Theory Arhivovano 16 lipnya 2013 u WebCite Stanford Encyclopedia of Philosophy Thompson Simon 1991 Type Theory and Functional Programming Arhivovano 23 bereznya 2021 u Wayback Machine Addison Wesley ISBN 0 201 41667 0 J Roger Hindley 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 Book review 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 Arhivovano 22 lyutogo 2019 u Wayback Machine PhD thesis Eindhoven University of Technology 1997 Otrimano z https uk wikipedia org w index php title Teoriya tipiv amp oldid 38149152