Теорія типів

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

Інколи визначення елементу запозичують з теорії множин та використовують його для позначення всіх закритих термів, які редукуються до однієї нормальної форми. Закритим термом називається терм, який не має параметрів. Терм виду ${\displaystyle x+1}$ має параметр ${\displaystyle x}$ та називається відкритим термом. Таким чином, ${\displaystyle 2+1}$ та ${\displaystyle 3+0}$ є різними термами, але вони обидва редукуються до елементу ${\displaystyle 3}$.

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

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

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

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

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

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

На практиці можна побудувати тип ${\displaystyle I\ \mathrm {nat} \ 3\ 4}$, але такий тип не буде мати термів. У теорії типів Мартіна-Льофа нові терми рівності мають властивість рефлексивності. Якщо ${\displaystyle 3}$ є термом типу ${\displaystyle \mathrm {nat} }$, то існує терм типу ${\displaystyle I\ \mathrm {nat} \ 3\ 3}$. Більш складні рівності можуть бути створені шляхом створення рефлексивного терму та його подальшої редукції. Тобто якщо ${\displaystyle 2+1}$ є термом типу ${\displaystyle \mathrm {nat} }$, то існує терм типу ${\displaystyle I\ \mathrm {nat} \ (2+1)\ (2+1)}$, який редукується до терму типу ${\displaystyle I\ \mathrm {nat} \ (2+1)\ 3}$. Таким чином, у цій системі рівність типів означає те, що два значення одного типу конвертуються за допомогою редукції.

Наявність типу рівності є важливим, оскільки їм можна маніпулювати всередині системи. Ми можемо також визначити нерівність типів: як у інтерпретації Брауера — Гейтінга — Колмогорова, відображаємо ${\displaystyle \neg (a=b)}$ до ${\displaystyle (a=b)\to \bot }$. Тобто існує терм типу ${\displaystyle (I\ \mathrm {nat} \ 3\ 4)\to \bot }$, але не існує терму типу ${\displaystyle (I\ \mathrm {nat} \ 3\ 3)\to \bot }$.

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

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

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

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

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

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

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

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

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

• Просто типізоване лямбда-числення (яке є логікою вищого порядку);
• теорія типів Мартіна-Льофа;
• система F;
• обчислення конструкцій.

• Automath;
• деякі форми комбінаторної логіки;
• теорія типів ST;
• теорії типів, які визначені для лямбда-куба;
• типізоване лямбда-числення;
• чисті системи типів.

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

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

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

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

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

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

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

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

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

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

• якщо ${\displaystyle a}$ та ${\displaystyle b}$ є типами, то також типом є і ${\displaystyle \langle a,b\rangle }$;
• типами є тільки базові типи та ті типи, які були побудовані способом, описаним у попередньому пункті.

Комплексний тип ${\displaystyle \langle a,b\rangle }$ — це тип функцій від об'єктів типу ${\displaystyle a}$ до об'єктів типу ${\displaystyle b}$. Таким чином, існують типи виду ${\displaystyle \langle e,t\rangle }$, які інтерпретуються як елементи множини функцій від об'єктів до значень істинності, тобто характеристичних функцій множин об'єктів. Вираз типу ${\displaystyle \langle \langle e,t\rangle ,t\rangle }$ є функцією від множини об'єктів до значень істинності. Цей тип є стандартним типом кванторів природної мови, таких як всі або ніхто.

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

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