Русская Википедия:Гомотопическая теория типов

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Гомотопическая теория типов (HoTT, от Шаблон:Lang-en) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, Шаблон:Нп5 и типах в логике и языках программирования.

Унивалентные основания математики — программа построения средствами гомотопической теории типов универсального формального языка, являющегося конструктивными основаниями для современных разделов математики и обеспечивающего возможность автоматической проверки правильности доказательств на компьютере. Инициирована Владимиром Воеводским в конце 2000-х годов; толчком к более широкому интересу к унивалентным основаниям послужила написанная Воеводским библиотека формализованной математики «Foundations», ставшая к середине 2010-х годов частью библиотеки UniMath и послужившая основой для многих других библиотекШаблон:Переход; в рамках программы большим коллективом математиков была написана книгаШаблон:Переход.

Математическое доказательство в гомотопической теории типов состоит в установлении «обитаемости» необходимого типа, то есть, в построении выражения соответствующего типа. Использование систем автоматического доказательства для теории эксплуатирует идею изоморфизма Карри — Ховарда, а благодаря математическому содержанию, вложенному в теоретико-типовые понятия, на формальном языке теории удаётся выразить и проверить достаточно сложные результаты из абстрактных разделов математики, которые ранее считались не формализуемыми программными средствами.

Ключевая идея теории — аксиома унивалентностиШаблон:Переход, постулирующая равенство объектов, между которыми может быть установлена эквивалентность, то есть, в гомотопической теории типов как равные рассматриваются изоморфные, гомеоморфные, гомотопически эквивалентные структуры; эта аксиома отражает важные свойства интерпретации высшей категории, а также обеспечивает техническое упрощение формального языка.

История

Идея использования интуиционистской теории типов Пера Мартин-Лёфа для формализации высших категорий восходит к работе Шаблон:Нп2, в которой была построена система FOLDS (Шаблон:Lang-en)[1]. Ключевым отличием унивалентных оснований от идей Маккаи является принцип, согласно которому фундаментальными объектами математики являются не высшие категории, а высшие группоиды. Поскольку высшие группоиды отвечают по соответствию Гротендика гомотопическим типам, можно сказать, что математика, с точки зрения унивалентных оснований, изучает структуры на гомотопических типах. Возможность прямого использования теории типов Мартин-Лёфа для описания структур на гомотопических типах является следствием построения Воеводским унивалентной модели теории типов. Построение этой модели требовало решения многочисленных технических проблем связанных с так называемыми свойствами когерентности и, хотя основные идеи унивалентных оснований были сформулированны им в 2005—2006 годы, полная унивалентная модель в категории симплициальных множеств появилась только в 2009 году. В те же годы, что и эти исследования Воеводского, велись и другие работы по изучению различных связей между теорией типов и теорией гомотопий, в частности, одним из исторически важных событий, собравшим учёных, работавших в этом направлении, стал семинар в Уппсале в ноябре 2006 года[2].

В феврале 2010 года Воеводский начал создавать библиотеку на Coq, выросшую впоследствии в совместно разрабатываемую широким кругом учёных «библиотеку унивалентных оснований»Шаблон:Переход.

По инициативе Воеводского, 2012—2013 академический год в Институте перспективных исследований был объявлен «годом унивалентных оснований», в сотрудничестве с Ауди и Коканом была открыта специальная исследовательская программа и в её рамках группа из математиков и специалистов по информатике работали над развитием теории. Одним из результатов года стало совместное создание участниками шестисотстраничной книги «Гомотопическая теория типов: унивалентные основания математики», выложенной на сайте программы в свободный доступ под лицензией CC-SA; для совместной работы над книгой был создан проект на GitHub[3].

Участники программы, представленные во введении к книгеШаблон:Sfn: Шаблон:Кол

Шаблон:Конец кол

Файл:Hott book cover.png
Обложка книги

Кроме того, во введении указано, что значительный вклад внесли также шестеро студентов, а также отмечен вклад более 20-ти учёных и практиков, посетивших в течение «года унивалентых оснований» Институт высших исследований (среди которых создатель семантики λ-исчисления Дана Скотт и разработчик формализаций на Coq доказательств задачи о четырёх красках и теоремы Фейта — Томпсона Шаблон:Iw). Книга построена из двух частей — «Основания» и «Математика», в первой части излагаются основные положения и определяется инструментарий, во второй — строятся реализации введёнными средствами теории гомотопий, теории категорий, теории множеств, вещественных чисел.

Основные положения

Теория основывается на интенсиональном варианте интуиционистской теории типов Мартин-Лёфа и использует интерпретацию типов как объектов теории гомотопий и высших категорий. Так, с этой точки зрения отношение принадлежности точки пространству <math>a \in A</math> рассматривается как терм соответствующего типа: <math>a: A</math>, расслоение с базой <math>X</math> — как зависимый тип <math>A(x)</math>. При этом отпадает необходимость представлять пространства в виде множеств точек, снабжённых топологией, и представлять непрерывные отображения между пространствами — как функции сохраняющие или отражающие соответствующие поточечные свойства пространств. Гомотопическая теория типов рассматривает пространства-типы и термы этих типов (точки) как элементарные понятия, а конструкции над пространствами, такие как гомотопии и расслоения, — как зависимые типы.

В формальном построении теории типов используется тип-универсум <math>\mathcal U_0</math>, термы которого — все прочие неуниверсальные («малые») типы, далее строятся типы <math>\mathcal U_1, \mathcal U_2, \dots</math> такие, что <math>U_i: U_{i+1}</math>, притом все термы типа <math>\mathcal U_i</math> также являются термами типа <math>\mathcal U_{i+1}</math>. Зависимые типы (семейства типов) определяются как функции <math>B: A \to \mathcal U</math>, кообласть которых — некоторый тип-универсум.

В гомотопической теории типов существует несколько способов конструирования новых типов из уже имеющихся. Базовые примеры такого рода — <math>\boldsymbol \Pi</math>-типы (зависимые функциональные типы, типы-произведения) и <math>\boldsymbol \Sigma</math>-типы (зависимые типы-суммы). Для данного типа <math>A: \mathcal U</math> и семейства <math>B: A \to \mathcal U</math> можно построить тип <math>\boldsymbol \Pi_{x:A} B(x)</math>, термы которого — функции, кообласть которых зависит от элемента области определения (геометрически такие функции можно представлять как сечения некоторого расслоения), а также тип <math>\boldsymbol \Sigma_{x:A}B(x)</math>, термы которого геометрически соответствуют элементам тотального пространства расслоения.

Равенство термов одного и того же типа в гомотопической теории типов может быть либо равенством «по определению» (<math>a_1 : = a_2</math>), либо пропозициональным равенством. Равенство по определению влечёт пропозициональное равенство, но не наоборот. В общем случае, пропозициональное равенство термов <math>a_1</math> и <math>a_2</math> типа <math>A</math> представляется в виде непустого типа <math>\mathsf {Id}_A (a_1,a_2)</math>, который называют типом тождества; термы этого последнего типа — это пути вида <math>p : a_1 \rightsquigarrow a_2</math> в пространстве <math>A</math>; тип тождества <math>\mathsf {Id}_A (a_1, a_2)</math>, таким образом, рассматривается как пространство путей (то есть непрерывных отображений единичного отрезка <math>\mathbb I</math> в <math>A</math>) из точки <math>a_1</math> в точку <math>a_2</math>.

Аксиома унивалентности

Интуиционистская теория типов позволяет определить понятие эквивалентности типов (для типов принадлежащих одному универсуму) и построить каноническим образом функцию из типа тождества <math>A = B</math> в тип эквивалентности <math>A \simeq B</math>:

<math>(A = B) \to (A \simeq B)</math>.

Аксиома унивалентности, сформулированная Воеводским, утверждает, что эта функция также является эквивалентностью:

<math>(A = B) \simeq (A \simeq B)</math>,

то есть, тип тождества двух данных типов эквивалентен типу эквивалентности этих типов. В случае если <math>A</math> и <math>B</math> — пропозициональные типы, аксиома имеет особенно прозрачный смысл и сводится к утверждению, который иногда называют принципом экстенсиональности Чёрча: равенство высказываний логически эквивалентно их логической эквивалентности; использование этого принципа означает, что во внимание принимаются только истинностные значения высказываний, но не их смысл. Следствием аксиомы является Шаблон:Iw, то есть утверждение о том, что функции, значения которых равны для всех равных значений их аргументов, равны между собой. Это свойство функций имеет важное значение в информатике.

Аксиома рассматривается некоторыми философами математики в качестве точной математической формулировки основного тезиса философии Шаблон:Iw, которая опирается на распространённую практику математических рассуждений «с точностью до изоморфизма» или «с точностью до эквивалентности»[4].

Логика, множества, группоиды

Высказывание (Шаблон:Lang-en2, «голое высказывание») в гомотопической теории типов определяется как тип <math>P</math>, который либо пуст, либо содержит единственный терм <math>p</math>; такие типы называются пропозициональными. Если тип <math>P</math> пуст, то соответствующее высказывание ложно, если <math>P</math> содержит терм <math>p</math> (символически — <math>p : P</math>), то соответствующее высказывание <math>P</math> истинно, а терм <math>p</math> рассматривается как его доказательство. Таким образом, в теории используется интуиционистская концепция истины, согласно которой истинность высказывания понимается как возможность предъявить доказательство этого высказывания.

Фрагмент гомотопической теории типов, который ограничивается операциями с пропозициональными типами, то есть с высказываниями, можно описать как логический фрагмент (логику) этой теории. Логическая дизъюнкция <math>A\vee B</math> соответствует в пропозициональном фрагменте типу-сумме <math>A+B</math>, конъюнкция <math>A\wedge B</math> — типу-произведению <math>A \times B</math>, импликация <math>A\Rightarrow B</math> — функциональному типу <math>A\to B</math>, отрицание <math>\lnot A</math> — типу <math>A\to \mathbf 0</math>, где <math>\mathbf 0</math> — это пустой тип (нуль-тип). Логика, соответствующая таким конструкциям, является вариантом интуиционистской логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего.

Всякий тип <math>X</math>, который содержит два или больше различных термов <math>x, y, \dots</math> может быть поставлен в однозначное соответствие с пропозициональным типом, который получается в результате отождествления всех термов типа <math>X</math>, такая операция называется пропозициональным обрезанием (Шаблон:Lang-en2). Это позволяет провести различие между «пропозициональным уровнем» (уровнем высказываний) теории и гомотопической иерархии «высших» непропозициональных её уровней.

За уровнем высказываний следует уровень множеств. Множество в гомотопической теории типов определяется как пространство (тип) с дискретной топологией. Эквивалентно, множество <math>A</math> можно описать в теории как тип, такой что для любых его термов <math>a_1, a_2 :A</math> тип <math>\mathsf {Id}_A (a_1,a_2)</math> является высказыванием, то есть либо пуст (случай когда <math>a_1</math> и <math>a_2</math> — это различные элементы множества <math>A</math>), либо содержит единственный элемент (случай, когда <math>a_1</math> и <math>a_2</math> — это один и тот же элемент). Вслед за уровнем множеств идёт уровень группоидов (множество точек и множество путей между каждой парой точек), и уровни <math>n</math>-группоидов всех порядков.

Различные интерпретации теоретико-типовых понятий

Интуиционистская теория типов Логика Теория множеств Теория гомотопий
тип <math>A</math> высказывание <math>A</math> множество <math>A</math> пространство <math>A</math>
<math>a:A</math> доказательство высказывания <math>A</math> <math>a</math> — элемент множества <math>A</math> <math>a</math> — точка пространства <math>A</math>
зависимый тип <math>B(x)</math> предикат <math>B(x)</math> семейство множеств расслоение <math>B_x</math>
<math>b(x) : B(x)</math> условное доказательство семейство элементов Шаблон:Iw
<math>\mathbf 0</math>, <math>\mathbf 1</math> <math>\bot</math>, <math>\top</math> <math>\varnothing</math>, <math>\{ \varnothing \}</math> <math>\varnothing</math>, <math>\ast</math>
<math>A + B</math> <math>A \vee B</math> <math>A \uplus B</math> (дизъюнктное объединение) <math>A \oplus B</math> (копроизведение)
<math>A \times B</math> <math>A \wedge B</math> <math>A \times B</math> (декартово произведение) <math>A \times B</math> (произведение пространств)
<math>A\to B</math> <math>A \Rightarrow B</math> множество функций <math>\{ f \mid f: A \to B \}</math> функциональное пространство <math>B^A</math>
<math>\boldsymbol \Sigma_{x:A} B(x)</math> <math>\exists_{x:A}B(x)</math> <math>\biguplus_{x \in A}B(x)</math> (дизъюнктное объединение) тотальное пространство
<math>\boldsymbol \Pi_{x:A} B(x)</math> <math>\forall_{x:A}B(x)</math> <math> \prod_{x \in A}B(x)</math> (декартово произведение) пространство сечений
<math>\mathsf{Id}_{A}</math> равенство (<math>=</math>) <math>\{ (x, x) \mid x \in A \}</math> пространство путей <math>A^\mathbb I</math>

Библиотеки и реализации HoTT

Библиотеки HoTT — несколько проектов, ведущихся на GitHub (в том же репозитории, где и размещены исходные коды книги), в которых создаются формальные описания различных разделов математики средствами систем автоматического доказательства с использованием построений гомотопической теории типов.

В проекте Владимира Воеводского, названном «Библиотека унивалентных оснований»[5], использовано специально разработанное минимальное безопасное подмножество Coq, обеспечивающее идеологическую чистоту и надёжность построений в согласовании с теорией. Проект HoTT[6] ведётся стандартными средствами Coq, реализуется в рамках исследовательской программы Института перспективных исследований, и в целом следует книгеШаблон:Переход, по состоянию Шаблон:На в проекте участвуют 48 разработчиков, наиболее активные — Джейсон Гросс, Майкл Шульман, Али Каглаян и Андрей Бауэр[7]. Также ведётся параллельный проект на языке Agda[8].

Существует несколько экспериментальных систем интерактивного доказательства, целиком основанных на HoTT: Arend, RedPRL, redtt, cooltt, а в Agda версии 2.6.0 добавлен так называемый «кубический режим», позволяющий полноценно использовать гомотопические типы.

Примечания

Шаблон:Примечания

Литература

Ссылки

Шаблон:Rq

Партнерские ресурсы
Криптовалюты
Магазины
Хостинг
Разное

  1. ↑ Шаблон:Cite web
  2. ↑ Шаблон:Cite web
  3. ↑ Шаблон:GitHub
  4. ↑ Шаблон:Статья
  5. ↑ Шаблон:GitHub
  6. ↑ Шаблон:GitHub
  7. ↑ HoTT Mar 20, 2011 — Oct 02, 2020 Contributions to master, excluding merge commits.
  8. ↑ Шаблон:GitHub
Источник — http://wikihandbk.com/ruwiki/index.php?title=Русская_Википедия:Гомотопическая_теория_типов&oldid=9584648