Гомотопическая теория типов на пальцах.
Гомотопическая теория типов Воеводского - это оригинальная попытка взглянуть на «классические» теории типов со стороны топологии. В HoTT тип - это теперь категория с изоморфизмами, тут же подключаются гомотопии, определяющие отношения эквивалентности, и т. д. Примитивно выражаясь, мы оперируем группоидами из теории категорий (преобразованиями пространств типов друг в друга), или даже группами отображений исходного множества состояний системы объектов на целевое (отображения возможны в обе стороны).
Неформально говоря, от теории Мартина-Лёфа гомотопическая теория отличатся лишь предложенной Воеводским аксиомой унивалентности (если между объектами можно установить эквивалентность, то их можно считать равными). Сильная сторона HoTT в том, что данная аксиома позволяет избавиться от множества формальных конструкций, уточняющих эквивалентность. Условно, мы принимаем несколько объектов за равные, пусть даже они и устроены внутри совершенно по-разному, если они в рамках нашей модели ведут себя идентично.
Пожалуй, главный недостаток HoTT в том, что она явно провозглашает (пока) отсутствие в себе известных редукций (примитивно говоря, механизмов упрощений) со свойством Чёрча-Россера - именно из-за аксиомы унивалентности. Теорема Чёрча-Россера позволяет доказывать равенства групп/полугрупп, корректность различных теорий формальных алгебр; обычно, считают, что эта теорема задаёт свойство конфлюентности (если в процессе вычислений мы, выйдя из некоторой вершины, можем пройти в разные вершины, то в будущем обязательно сможем и сойтись снова), но корректнее сказать, что она также определяет и конечность вычислений.
И вот без этого свойства HoTT пока смотрится преимущественно теоретической, так как отбрасывается огромный пласт ранее наработанных механизмов редукций. По этой причине многое в самой HoTT приходится изобретать с нуля, и до относительно массового (как Agda или Coq) применения ей пока далеко (годы и годы).
Но конечно гениальный Воеводский эти проблемы предвидел. Он исходно замыслил HoTT не только как чистую теорию, но и сразу же как формальный язык, отлично пригодный для реализации на компьютере. Можно сказать, что математикам теперь становится существенно проще выражать различные формализации на математическом языке, аки на языке программирования. По сей день для этого используется теория множеств, и вот на замену ей предлагается существенно более высокоуровневая HoTT. По этой причине то расстояние, что Coq прошёл за 10 лет, HoTT может преодолеть гораздо быстрее.
Сделаем теперь небольшую итерацию по HoTT применительно к нашим нуждам. Пока компьютерный движок Воеводского весьма далёк от прозаических нужд IT-мэйнстрима, может быть, сама теория нам даст какие-то полезные рекомендации?
Ключевой момент HoTT - это способ установления эквивалентности между типами (под типом мы понимаем также допустимые над объектом операции). У нас есть некий набор частных преобразований типов друг в друга (например, отображение модели базы данных на модель логики вычислений), и если эти преобразования непрерывны и возможны в обе стороны, то мы можем считать типы эквивалентными.
Вот тут мы приходим к концепции identity types - сам этот набор преобразований мы считаем таким «типом идентичности»! Identity type (по сути, топологические пути) доказывает, что два типа эквивалентны. В свою очередь, эквивалентность можно задавать и для этих identity types, и т. д.
Что это нам даёт? HoTT разрешает нам определить identity type, в частности, как индуктивный (определяемый единственной рекурсивной функцией). И вот в результате мы теперь можем утверждать, что такой identity type всегда будет вычислим (хотя и не известно, как)!
Это означает, что если некоторая функция/программа реализует identity type, то она является доказанной - корректно вычислимой! Для этого нам надо «всего лишь» организовать нашу функцию так, чтобы она использовала только корректно рекурсивно реализованные внутренние «типы идентичности».
http://naufsb.ru/mathematics/m45_hott/
Неформально говоря, от теории Мартина-Лёфа гомотопическая теория отличатся лишь предложенной Воеводским аксиомой унивалентности (если между объектами можно установить эквивалентность, то их можно считать равными). Сильная сторона HoTT в том, что данная аксиома позволяет избавиться от множества формальных конструкций, уточняющих эквивалентность. Условно, мы принимаем несколько объектов за равные, пусть даже они и устроены внутри совершенно по-разному, если они в рамках нашей модели ведут себя идентично.
Пожалуй, главный недостаток HoTT в том, что она явно провозглашает (пока) отсутствие в себе известных редукций (примитивно говоря, механизмов упрощений) со свойством Чёрча-Россера - именно из-за аксиомы унивалентности. Теорема Чёрча-Россера позволяет доказывать равенства групп/полугрупп, корректность различных теорий формальных алгебр; обычно, считают, что эта теорема задаёт свойство конфлюентности (если в процессе вычислений мы, выйдя из некоторой вершины, можем пройти в разные вершины, то в будущем обязательно сможем и сойтись снова), но корректнее сказать, что она также определяет и конечность вычислений.
И вот без этого свойства HoTT пока смотрится преимущественно теоретической, так как отбрасывается огромный пласт ранее наработанных механизмов редукций. По этой причине многое в самой HoTT приходится изобретать с нуля, и до относительно массового (как Agda или Coq) применения ей пока далеко (годы и годы).
Но конечно гениальный Воеводский эти проблемы предвидел. Он исходно замыслил HoTT не только как чистую теорию, но и сразу же как формальный язык, отлично пригодный для реализации на компьютере. Можно сказать, что математикам теперь становится существенно проще выражать различные формализации на математическом языке, аки на языке программирования. По сей день для этого используется теория множеств, и вот на замену ей предлагается существенно более высокоуровневая HoTT. По этой причине то расстояние, что Coq прошёл за 10 лет, HoTT может преодолеть гораздо быстрее.
Сделаем теперь небольшую итерацию по HoTT применительно к нашим нуждам. Пока компьютерный движок Воеводского весьма далёк от прозаических нужд IT-мэйнстрима, может быть, сама теория нам даст какие-то полезные рекомендации?
Ключевой момент HoTT - это способ установления эквивалентности между типами (под типом мы понимаем также допустимые над объектом операции). У нас есть некий набор частных преобразований типов друг в друга (например, отображение модели базы данных на модель логики вычислений), и если эти преобразования непрерывны и возможны в обе стороны, то мы можем считать типы эквивалентными.
Вот тут мы приходим к концепции identity types - сам этот набор преобразований мы считаем таким «типом идентичности»! Identity type (по сути, топологические пути) доказывает, что два типа эквивалентны. В свою очередь, эквивалентность можно задавать и для этих identity types, и т. д.
Что это нам даёт? HoTT разрешает нам определить identity type, в частности, как индуктивный (определяемый единственной рекурсивной функцией). И вот в результате мы теперь можем утверждать, что такой identity type всегда будет вычислим (хотя и не известно, как)!
Это означает, что если некоторая функция/программа реализует identity type, то она является доказанной - корректно вычислимой! Для этого нам надо «всего лишь» организовать нашу функцию так, чтобы она использовала только корректно рекурсивно реализованные внутренние «типы идентичности».
http://naufsb.ru/mathematics/m45_hott/