Математическая логика
Гомотопическая теория типов
Гомотопическая теория типов объединяет математическое доказательство и вычисление: доказательство = программа, тип = спецификация. Аксиома унивалентности Воеводского делает изоморфные структуры идентичными - устраняет различие между 'равенством' и 'изоморфизмом' в математике.
- Lean 4 / Mathlib4: 250 000 формально верифицированных лемм включая теорему Ферма-Уайлса - результат прямого применения теории типов на основе HoTT
- Агда с кубической теорией типов (Agda Cubical): первый доказатель с вычислительной унивалентностью, в котором pi_1(S^1) = Z верифицируется как программа
- Синтетическая алгебраическая геометрия: формализация схем Гротендика в HoTT - активная область в UniMath (библиотека для Coq)
- Типы с зависимостями в языках программирования (Idris, Agda): прямое применение теории типов Мартина-Лёфа для верификации программ с точными инвариантами
HoTT: типы, пути и унивалентность
Владимир Воеводский в 2009 году предложил аксиому унивалентности, объединив теорию типов Мартина-Лёфа с гомотопической топологией. Книга HoTT (2013) написана за год совместно 50 математиками. Proof assistant Lean 4 (библиотека Mathlib4, 250 000 лемм) и Coq используют теорию типов, основанную на тех же принципах.
Что утверждает аксиома унивалентности в HoTT?
Аксиома унивалентности: (A ~ B) ~ (A = B). Типы, эквивалентные как математические объекты, идентичны как типы. Это позволяет заменять 'изоморфизм' на 'равенство' везде без потери строгости.
Высшие индуктивные типы и обрезки
Высшие индуктивные типы (HIT) позволяют определять пространства аксиоматически: задавать точки и пути между ними как конструкторы. Тип-обрезки (truncations) позволяют 'забывать' структуру путей выше заданного уровня - получать из произвольного типа пропозицию, множество или группоид.
HoTT открывает синтетическую гомотопическую теорию: классические теоремы алгебраической топологии (фундаментальная группа S^1, теорема Хопфа о расслоении) доказываются формально в доказателях Agda и Lean без классической топологии. Это объединяет теорему и её доказательство в один вычислительный объект.
Что такое высший индуктивный тип (HIT)?
Высший индуктивный тип (HIT): тип задаётся конструкторами как для элементов (точек), так и для путей (равенств) между ними. Пример: S^1 = {base: S^1; loop: base = base}.
Итоги
- Тип тождества a =_A b: тип доказательств равенства, элементы которого - пути; структура inf-группоида
- Аксиома унивалентности: (A ~ B) ~ (A = B) - эквивалентность типов равносильна их равенству в Universe
- Высшие индуктивные типы (HIT): конструкторы путей позволяют задавать пространства аксиоматически (S^1, T^2, K(G,1))
- Транспорт: путь p: a = b автоматически переносит доказательства предиката P(a) в P(b)
- Пропозициональные обрезки ||A||_{-1}: превращают тип в пропозицию 'A населён' без конкретного элемента
- Кубическая TT (Agda Cubical): унивалентность становится вычислительной через интервальный тип I = {0, 1, seg}