Теорія типів

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

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

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

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

Історія

[ред. | ред. код]

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

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

Базові поняття

[ред. | ред. код]

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

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

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

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

Відмінності від теорії множин

[ред. | ред. код]

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

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

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

[ред. | ред. код]

Нормалізація

[ред. | ред. код]

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

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

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

Залежні типи

[ред. | ред. код]
Докладніше: Залежний тип

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

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

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

Типи рівності

[ред. | ред. код]

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

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

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

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

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

Індуктивні типи

[ред. | ред. код]

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

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

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

Універсальний тип

[ред. | ред. код]

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

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

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

Обчислювальна складова

[ред. | ред. код]

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

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

Теорії типів

[ред. | ред. код]

Значні

[ред. | ред. код]

Другорядні

[ред. | ред. код]

Активні

[ред. | ред. код]

Практичне використання

[ред. | ред. код]

Мови програмування

[ред. | ред. код]
Докладніше: Система типізації

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

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

Математичні основи

[ред. | ред. код]

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

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

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

[ред. | ред. код]

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

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

Лінгвістика

[ред. | ред. код]

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

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

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

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

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

Соціальні науки

[ред. | ред. код]

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

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

[ред. | ред. код]

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

  • декартово замкнені категорії відповідають типізованому лямбда-численню (Ламбек, 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. ETCS in nLab. ncatlab.org. Архів оригіналу за 23 лютого 2019. Процитовано 22 лютого 2019.
  3. John L. Bell (2012). Types, Sets and Categories. У Akihiro Kanamory (ред.). Handbook of the History of Logic. Volume 6. Sets and Extensions in the Twentieth Century (PDF). Elsevier. ISBN 978-0-08-093066-4. Архів оригіналу (PDF) за 17 квітня 2018. Процитовано 21 лютого 2019.

Література

[ред. | ред. код]