Гомотопическая теория типов
Оригинал взят у akuklev в По просьбе os80 пишу ещё раз об унивалентности в ЖЖ
(P.S. Кажется, я научился быстро писать. Весь нижеследующий пост написался за 15 минут за едой.)
Гомотопическая теория типов HoTT это такой фреймворк для деланья математики и одновременно язык программирования. Среди довольно обширного семейства таких систем* HoTT примечательна тем, что gets equality right. То есть понятие равенства в ней соответствует понятию равенства, как оно используется математиками на практике в рассуждениях и доказательствах. Теория множеств хоть и является сейчас де юре основанием математики, но на практике как раз используют не теоретикомножественное равенство, а равенство по существу. Майк Шульман очень хорошо об этом пишет: http://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html
(* Коканд придумал называть такие системы исчислениями построений и это прекрасно отражает их суть: на языке этих систем описывается одинаково просто и как построить из произвольного списка отсортированный, и как построить для данного треугольника описанную окружность, и как построить для данного топологического пространства его одноточечную компактификацию, и как строится из предпосылок и постулатов доказательство. Типизированность языка означает, что записать можно только корректные построения/доказательства, иначе "не компилируется". Сила исчислений построений в том, что в них мир однородный: доказательства такие же объекты, как, например, множества, с ними тоже можно работать в рамках самой системы. Математику не нужно делить на математику и метаматематику.)
Все разработанные на данный момент исчисления построений базируются на Intensional Martin-Löf Dependent Type Theory. А с этой штукой была нерешенная проблема, о которой хорошо написано вот тут:
"In Intensional Type Theory we differentiate between a decidable definitional equality and a propositional equality type (for any given type) which requires proof. Typing only depends on definitional equality and hence is decidable. In Intensional Type Theory the type corresponding to the principle of extensionality /"отображения, равные на равных аргументах, равны" -- прим/ is not inhabited. It has been an open problem how to extend Intensional Type Theory s.t. Ext is inhabited without destroying other fundamental properties. Ext is provable in Extensional Type Theory, where propositional and definitional equality are identified, but then equality and type checking become undecidable."
А если у нас typechecking undecidable, то это жопа и практически no go. Но хочется чтобы равные по-существу объекты таки воспринимались теорией как равные. Какая без этого жопа, знает всякий, кто пытался писать нетривиальные доказательства на Agda: проблема в том, что мы сформулировали теорему для объекта x и хотим применить к объекту y, но тут выясняется, что мы не можем этого сделать, потому что x и y равны только "по-существу", но не в рамках теории. Требуется большой инструментарий извращений, чтобы осуществить трансфер теоремы для x-ов в теорему для y-ов. Ну и если не касаться теорем, а только программирования, то такая фигня иногда вылезает в хитрых полиморфных функциях: должны бы сразу работать, ан нет, надо писать хитрый трансформер.
Позже Альтенкирх и МакБрайд разработали Observational Type Theory, в которой typechecking остаётся разрешимым, но при этом для отображений (и вообще всех коданных) верна экстенциональность в сильном смысле: "неотличимые внешне объекты коданных равны". Проясню: объекты коданных это черные ящики, к которым можно применять ограниченный набор операторов и получать какие-то результаты. К возможно бесконечной последовательности натуральных чисел (тип коданных Seq[Nat]) можно применять оператор "взять первое значение" takeLast: Seq[Nat] -> (value: Nat, rest: Seq[Nat]), такие последовательности неотличимы, если сколько take не применяй, результаты будут совпадать. Функция A -> B это чёрный ящик с оператором apply: A -> B, который принимает значения типа A и возвращает значения типа B. Если для всех равных A результаты B будут равны, то и функции между собой равны.
OTT не решает две проблемы:
1) Проблема фактортипов T/G, т.е. типов данных, где мы что-то отождествляем. Простые примеры это тип неупорядоченых пар, который получается из обычного типа пар (a: T, b: T) факторизацией по группе, переставляющей a и b местами. У этого типа есть два нужных обобщения для списков: неупорядоченные списки (known as multiset or collection) и кольцевые списки. В первом случае мы делим List[T] на группу перестановок элементво нужной длины: Collection[T] = l: List[T] / (length l)!, где оператор ! для всякого числа n вычисляет группу перестановок из n элементов. CircList[T] изготавливается факториацией по группе сдвигов. Для коданных фактортипы вообще интересны. Тип Seq[Boolean] это возможно бесконечная последовательность нулей и единичек, что очень и очень похоже на двоичную "десятичную" дробь, представляющую число от 0 до 1. Но чтобы это стало правдой, надо произвести отождествления, что b0.1 = b0.100.. = b0.0111.. (это как случай 0.099999.. для десятичных дробей). В ITT/ETT/OTT такого типа опять же не определишь, нет там действительных чисел. Они неадекватны для математики уровня анализа и, соответственно, корректной типизации программ обработки сигналов и идеализированных численных методов (те и другие, имеют дело с настоящими действительными числами).
2) Эквивалентные типы такие как List[T] и (∃n: Nat, Vec[T, length = n]) или Nat и Int ↾ (_ ≥ 0) между собой не равны, эквивалентные структуры, такие как упорядоченное полукольцо натуральных чисел, определенное на типе Nat, та же структура определенная на неотрицательных целых, та же структура определенная на нумералах Чёрча между собой попарно не равны. Получается, что трансфер математических теорем вдоль структурных изоморфизмов проблематичен. А на уровне программирования это означает, что затруднена инкапсуляция (написание функций, ингорящих представление данных и опирающихся только на структуру), и работа с типами-орнаментами.
Все эти проблемы автомагически решаются в HoTT, гомотопической теории типов, где берется интуиционистская теория типов, из неё убирается аксиома что равенство между объектами бывает только одно (т.е. типы a = b теперь интерпретируются не как тип доказательств равенства a и b, а как тип сохраняющих структуру обратимых переходов от a к b) и добавляется аксиома унивалентности, утверждающая что эквивалентные сущности равны. Эта теория впервые в истории математики описывает равенство объектов в настолько же сильном смысле, как оно используется на практике в неформальных доказательствах. Поэтому HoTT на данный момент лучший претендент на использования в системах записи и автоматической верификации математических доказательств. Без HoTT доказательства на этапе формализации их "с бумаги в компьютер" заведомо разрастаются в разы, при том что ничего существенного это разрастание не превносит, только лишние подробности, для обхода слабостей системы проверки доказательств.
Пока, конечно, HoTT ещё слишком молода: во-первых, только-только сделали первый прототип её вычислительной интерпретации (т.е. виртуальную машину, для которой она является языком программирования), и ещё не доказали full canonicity и прочих ценных плюшек. Но это не единственное, что служит барьером к использованию HoTT в качестве оснований математики. ZFC/NBG проявила себя как мощный инструмент, там можно всякие Стоун-Чеховские компактификации строить, всякие универсальные замыкания, ультрафильтры... Форсингом заниматься. В общем, не так-то просто уйти из фреймворка с такой развитой инфраструктурой, даже если почему-то хочется. Нужно убедиться, что всё это можно делать в HoTT + HoTT (в отличие от ZFC/NBG) служит хорошей базой для построения теории категорий, включая высшие категории.
Ну и, кмк, использование HoTT в качестве основания математики будет возможно не раньше, чем будут четко выделены фрагменты/обобщения HoTT консервативные (в классической модальности) над Z2 (арифметика второго порядка), и ZFC/NBG с разными вариантами аксиомами выбора и разными аксиомы о больших кардиналах. А использование её в Reverse mathematics будет возможно не раньше, чем будет выявлен фрагмент, консервативный над explicit mathematics товарища Фефермана.
Все подробности про HoTT, исключая совсем новенькое, есть в The HoTT book (http://homotopytypetheory.org/book/), которую я всецело рекомендую.
(P.S. Кажется, я научился быстро писать. Весь нижеследующий пост написался за 15 минут за едой.)
Гомотопическая теория типов HoTT это такой фреймворк для деланья математики и одновременно язык программирования. Среди довольно обширного семейства таких систем* HoTT примечательна тем, что gets equality right. То есть понятие равенства в ней соответствует понятию равенства, как оно используется математиками на практике в рассуждениях и доказательствах. Теория множеств хоть и является сейчас де юре основанием математики, но на практике как раз используют не теоретикомножественное равенство, а равенство по существу. Майк Шульман очень хорошо об этом пишет: http://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html
(* Коканд придумал называть такие системы исчислениями построений и это прекрасно отражает их суть: на языке этих систем описывается одинаково просто и как построить из произвольного списка отсортированный, и как построить для данного треугольника описанную окружность, и как построить для данного топологического пространства его одноточечную компактификацию, и как строится из предпосылок и постулатов доказательство. Типизированность языка означает, что записать можно только корректные построения/доказательства, иначе "не компилируется". Сила исчислений построений в том, что в них мир однородный: доказательства такие же объекты, как, например, множества, с ними тоже можно работать в рамках самой системы. Математику не нужно делить на математику и метаматематику.)
Все разработанные на данный момент исчисления построений базируются на Intensional Martin-Löf Dependent Type Theory. А с этой штукой была нерешенная проблема, о которой хорошо написано вот тут:
"In Intensional Type Theory we differentiate between a decidable definitional equality and a propositional equality type (for any given type) which requires proof. Typing only depends on definitional equality and hence is decidable. In Intensional Type Theory the type corresponding to the principle of extensionality /"отображения, равные на равных аргументах, равны" -- прим/ is not inhabited. It has been an open problem how to extend Intensional Type Theory s.t. Ext is inhabited without destroying other fundamental properties. Ext is provable in Extensional Type Theory, where propositional and definitional equality are identified, but then equality and type checking become undecidable."
А если у нас typechecking undecidable, то это жопа и практически no go. Но хочется чтобы равные по-существу объекты таки воспринимались теорией как равные. Какая без этого жопа, знает всякий, кто пытался писать нетривиальные доказательства на Agda: проблема в том, что мы сформулировали теорему для объекта x и хотим применить к объекту y, но тут выясняется, что мы не можем этого сделать, потому что x и y равны только "по-существу", но не в рамках теории. Требуется большой инструментарий извращений, чтобы осуществить трансфер теоремы для x-ов в теорему для y-ов. Ну и если не касаться теорем, а только программирования, то такая фигня иногда вылезает в хитрых полиморфных функциях: должны бы сразу работать, ан нет, надо писать хитрый трансформер.
Позже Альтенкирх и МакБрайд разработали Observational Type Theory, в которой typechecking остаётся разрешимым, но при этом для отображений (и вообще всех коданных) верна экстенциональность в сильном смысле: "неотличимые внешне объекты коданных равны". Проясню: объекты коданных это черные ящики, к которым можно применять ограниченный набор операторов и получать какие-то результаты. К возможно бесконечной последовательности натуральных чисел (тип коданных Seq[Nat]) можно применять оператор "взять первое значение" takeLast: Seq[Nat] -> (value: Nat, rest: Seq[Nat]), такие последовательности неотличимы, если сколько take не применяй, результаты будут совпадать. Функция A -> B это чёрный ящик с оператором apply: A -> B, который принимает значения типа A и возвращает значения типа B. Если для всех равных A результаты B будут равны, то и функции между собой равны.
OTT не решает две проблемы:
1) Проблема фактортипов T/G, т.е. типов данных, где мы что-то отождествляем. Простые примеры это тип неупорядоченых пар, который получается из обычного типа пар (a: T, b: T) факторизацией по группе, переставляющей a и b местами. У этого типа есть два нужных обобщения для списков: неупорядоченные списки (known as multiset or collection) и кольцевые списки. В первом случае мы делим List[T] на группу перестановок элементво нужной длины: Collection[T] = l: List[T] / (length l)!, где оператор ! для всякого числа n вычисляет группу перестановок из n элементов. CircList[T] изготавливается факториацией по группе сдвигов. Для коданных фактортипы вообще интересны. Тип Seq[Boolean] это возможно бесконечная последовательность нулей и единичек, что очень и очень похоже на двоичную "десятичную" дробь, представляющую число от 0 до 1. Но чтобы это стало правдой, надо произвести отождествления, что b0.1 = b0.100.. = b0.0111.. (это как случай 0.099999.. для десятичных дробей). В ITT/ETT/OTT такого типа опять же не определишь, нет там действительных чисел. Они неадекватны для математики уровня анализа и, соответственно, корректной типизации программ обработки сигналов и идеализированных численных методов (те и другие, имеют дело с настоящими действительными числами).
2) Эквивалентные типы такие как List[T] и (∃n: Nat, Vec[T, length = n]) или Nat и Int ↾ (_ ≥ 0) между собой не равны, эквивалентные структуры, такие как упорядоченное полукольцо натуральных чисел, определенное на типе Nat, та же структура определенная на неотрицательных целых, та же структура определенная на нумералах Чёрча между собой попарно не равны. Получается, что трансфер математических теорем вдоль структурных изоморфизмов проблематичен. А на уровне программирования это означает, что затруднена инкапсуляция (написание функций, ингорящих представление данных и опирающихся только на структуру), и работа с типами-орнаментами.
Все эти проблемы автомагически решаются в HoTT, гомотопической теории типов, где берется интуиционистская теория типов, из неё убирается аксиома что равенство между объектами бывает только одно (т.е. типы a = b теперь интерпретируются не как тип доказательств равенства a и b, а как тип сохраняющих структуру обратимых переходов от a к b) и добавляется аксиома унивалентности, утверждающая что эквивалентные сущности равны. Эта теория впервые в истории математики описывает равенство объектов в настолько же сильном смысле, как оно используется на практике в неформальных доказательствах. Поэтому HoTT на данный момент лучший претендент на использования в системах записи и автоматической верификации математических доказательств. Без HoTT доказательства на этапе формализации их "с бумаги в компьютер" заведомо разрастаются в разы, при том что ничего существенного это разрастание не превносит, только лишние подробности, для обхода слабостей системы проверки доказательств.
Пока, конечно, HoTT ещё слишком молода: во-первых, только-только сделали первый прототип её вычислительной интерпретации (т.е. виртуальную машину, для которой она является языком программирования), и ещё не доказали full canonicity и прочих ценных плюшек. Но это не единственное, что служит барьером к использованию HoTT в качестве оснований математики. ZFC/NBG проявила себя как мощный инструмент, там можно всякие Стоун-Чеховские компактификации строить, всякие универсальные замыкания, ультрафильтры... Форсингом заниматься. В общем, не так-то просто уйти из фреймворка с такой развитой инфраструктурой, даже если почему-то хочется. Нужно убедиться, что всё это можно делать в HoTT + HoTT (в отличие от ZFC/NBG) служит хорошей базой для построения теории категорий, включая высшие категории.
Ну и, кмк, использование HoTT в качестве основания математики будет возможно не раньше, чем будут четко выделены фрагменты/обобщения HoTT консервативные (в классической модальности) над Z2 (арифметика второго порядка), и ZFC/NBG с разными вариантами аксиомами выбора и разными аксиомы о больших кардиналах. А использование её в Reverse mathematics будет возможно не раньше, чем будет выявлен фрагмент, консервативный над explicit mathematics товарища Фефермана.
Все подробности про HoTT, исключая совсем новенькое, есть в The HoTT book (http://homotopytypetheory.org/book/), которую я всецело рекомендую.