Теорія типів

Вступ в предмет

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

Простори функцій ()
Простори пар ()
Ідентифікаційні простори ()
Поліноміальні функтори ()
Простори шляхів ()
Склейки ()
Інфінітезимальні околи ()
Фактор-простори Lean ()
CW-комплекси ()

Слухачам курсу (10) пропонується застосувати теорію типів для доведення початкового але нетривіального результу, який є відкритою проблемою в теорії типів для однєї із математик, що є курсами на кафедрі чистої математики (КМ-111):

Теорія гомотопій
Гомологічна алгебра
Теорія категорій
Функціональний аналіз
Диференціальна геометрія

Курс (10) умовно можна розділити на 4 частини, кожна з яких показує не тільки типи-аксіоми, але і мета-теоретичні спряження в яких вони приймають участь.

Мотивація

Головна мотивація гомотопічної теорії — надати обчислювальну семантику гомотопічним типам та CW-комплексам. Головна ідея гомотопічної теорії [1] полягає в поєднанні просторів функцій , просторів контекстів і просторів шляхів таким чином, що вони утворюють фібраційну рівність яка збігається (доводиться в самій теорії) з простором шляхів.

def isContr (A: U) : U
 := Σ (x: A), Π (y: A), Path A x y

def fiber (A B: U) (f: A → B) (y: B): U
 := Σ (x: A), Path B y (f x)

def isEquiv (A B: U) (f: A → B): U
 := Π (y: B), isContr (fiber A B f y)

def equiv(X Y: U): U
 := Σ (f: X → Y), isEqiv X Y f

def ua (A B : U) (p : Path U A B) : equiv A B
 := transp (<i> equiv A (p @ i)) 0 (idEquiv A)

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

def isProp (A : U) : U
 := Π (a b : A), Path A a b

def isSet (A : U) : U
 := Π (a b : A) (a0 b0 : Path A a b),
    Path (Path A a b) a0 b0

def isGroupoid (A : U) : U
 := Π (a b : A) (x y : Path A a b)
    (i j : Path (Path A a b) x y),
    Path (Path (Path A a b) x y) i j

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

def CatGroupoid (X : U) (G : isGroupoid X)
  : isCatGroupoid (PathCat X)
 := ( idp X,
      comp-Path X,
      G,
      sym X,
      comp-inv-Path⁻¹ X,
      comp-inv-Path X,
      comp-Path-left X,
      comp-Path-right X,
      comp-Path-assoc X,
      ★
    )

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

[1]. Pelayo, Warren. Homotopy type theory and Voevodsky's univalent foundations. 2012.

Фібраційні доведення

Фібраційні доведення моделюються примітивами-аксіомами які є теоретико-типовими відображеннями категорної мета-теоретичної моделі спряжень трьох функторів Кока-Райта, з яких народжуються простори функцій та простори контекстів: 1) Простір функцій (П); 2) Простір пар (Σ). Ці способи доведення дозволяють безпосреденьо аналізувати розшарування.

Доведення рівності

В інтенсіональній теорії типів тип рівності вбудований теж як теоретико-типові примітиви категорної мета-теоретичної моделі спряжень трьох функторів Якобса-Лавіра: 1) Фактор-простору (Q); 2) Ідентифікаційної системи (=); 3) Стягуваного простору (С). Ці способи доведення дозволяють безпосередньо працювати з ідентифікаційними системами: строгою для теорії множин і гомотопічною для теорії гомотопій.

Індуктивні доведення

В теорії типів індуктивні типи можуть бути вбудованими декількома способами: як поліноміальні функтори W і M або загальні схеми ідуктивних типів Полін-Морін (Calculus of Inductive Constructions) з такими властивостями 1) верифікація скінченності програм; 2) верифікація строгої позитивності параметрів; 3) верифікація взаємної рекурсії.

У цьому курсі гомотопічної теорії типів індукція і коіндукція даються як теоретико-типові примітиви категорної мета-теоретичної моделі спряжень поліноміальних функторів Ламбека-Бома. Ці способи доведень дозволяють безпосередньо маніпулювати ініціальними та термінальними алгебрами, алгебраїчними рекурсивними типами даних, нескінченними процесами.

Вищі індуктивні доведення, де конструкторами крім точок можуть виступати також простори шляхів, також моделюються поліноміальними функторами, але на відміну F-алгебр Ламбека-Бома тут використовуються монади-алгебри та комонади-коалгебри Люмсдейна-Шульмана-Веццозі.

Геометричні доведення

Для потреб диференціальної геометрії в теорію типів вбудовують примітиви-аксіоми категорної мета-теоретичної моделі трьох функторів Шрайбера-Шульмана: 1) Інфінітезімального околу (Im); 2) Редукованої модальності (Re); 3) Інфінітезімального дискретного околу (&).