Комментарии 35
Остаётся только надеяться, что и другие авторы последуют их примеру.
Для чего HoTT? Что в перспективе? Писать программы вместо доказательств?
Для минусующего (в том числе карму) стада, которому что-то там померещилось, и почему-то воспринимающем мои вопросы как «нафига Haskell, если есть Basic», и которое является, по-видимому, знатоком HoTT в третьем поколении, позвольте дать более развернутый вопрос от новичка, впервые прочитавшем о HoTT.
Является ли HoTT, как основание математики «не на множествах», мостом к автоматизации математических доказательств? На упомянутом в статье языке Agda, если я правильно понял, эти вещи уже частично делаются.
(мои познания в HoTT ограничены только этим постом, и по этому поводу найденной шикарной статьёй про «Но ведь это одно и то же» 2*9 и 9*2, половину которой слёту неосилил, это действительно — новая математика)
Является ли HoTT, как основание математики «не на множествах», мостом к автоматизации математических доказательств? На упомянутом в статье языке Agda, если я правильно понял, эти вещи уже частично делаются.
(мои познания в HoTT ограничены только этим постом, и по этому поводу найденной шикарной статьёй про «Но ведь это одно и то же» 2*9 и 9*2, половину которой слёту неосилил, это действительно — новая математика)
Возможно, следующий отрывок интервью Владимира Воеводского (кстати говоря, лауреата Филдсовской премии), в котором он описывает историю создания HoTT, поможет понять, зачем нужна эта теория и что вообще происходит:
… Параллельно я искал подходы к проблеме накопления ошибок в работах по чистой математике. Было ясно, что единственное решение — это создание языка, на котором математические доказательства могут писаться людьми в такой форме, что это можно будет проверять на компьютере. Вплоть до 2005 года мне казалось, что это задача намного более сложная чем задача исторической генетики, которой я занимался. Во многом это ощущение было результатом устоявшегося и очень распространенного среди математиков мнения, что абстрактную математику невозможно разумным образом формализовать настолько аккуратно, чтобы ее «понимал» компьютер.
В 2005 мне удалось сформулировать несколько идей, которые неожиданно открыли новый подход к одной из основных проблем в основаниях современной математики. Проблему эту можно неформально сформулировать как вопрос о том, как правильно формализовать интуитивное понимание того, что «одинаковые» математические объекты имеют одинаковые свойства. Аргументы, основанные на этом принципе, очень часто используются в современных математических доказательствах, но существующие основания математики (теория множеств Цермело-Френкеля) совершенно неприспособлены для формализации таких аргументов.
Я был очень хорошо знаком с этой проблемой и думал о ней еще в 1989 году, когда Миша Капранов и я работали над теорией поли-катергорий. Тогда нам казалось, что ее решить невозможно. То, что мне удалось понять в 2005 году, скомбинировав идеи теории гомотопий (части современной топологии) и теории типов (части современной теории языков программирования), было совершенно удивительно, и открывало реальные возможности построения того самого языка, на котором люди могут писать доказательства, которые сможет проверять компьютер. Дальше был большой перерыв в моей математической деятельности. [...] К идеям, связанным с компьютерной проверкой доказательств, я вернулся только летом 2009, когда мне стало окончательно ясно, что с исторической генетикой ничего не получается. И буквально через несколько месяцев случились два события, которые продвинули эти идеи от общих наметок, над которыми, я думал, придется работать еще не один год, до стадии, на которой я смог заявить, что я придумал новые основания математики, которые позволят решить проблему компьютерной проверки доказательств. Сейчас это называется «унивалентные основания математики» и ими занимаются как математики, так и теоретики языков программирования. Я почти не сомневаюсь, что эти основания вскоре заменят теорию множеств и что проблему языка абстрактной математики, который будут «понимать» компьютеры можно считать в основном решенной. [...] Первые примеры языков того класса с которыми я работаю, были созданы в конце 1970-ых и известны под названием «Martin-Lof type theories». Удивительным образом языки были, программные системы использующие эти языки создавались и даже становились популярными (особенно система «Coq» которую создали французы), но понимания того, о чем эти языки позволяют говорить, не было. Получалось, что используется только очень небольшая часть возможностей языка, та, которая, как теперь ясно, позволяет говорить про множества. Язык же в целом позволяет говорить про гомотомические типы любого уровня сложности. Разрыв, как ты понимаешь, огромный. Как следствие сами языки не совершенствовались, потому что было не ясно, что можно менять, а что нельзя. Теперь, когда мы понимаем, что в этих языках существенно, а что нет, открывается возможность сделать их значительно более «мощными» и, как следствие, более удобными для практического использования.
… Параллельно я искал подходы к проблеме накопления ошибок в работах по чистой математике. Было ясно, что единственное решение — это создание языка, на котором математические доказательства могут писаться людьми в такой форме, что это можно будет проверять на компьютере. Вплоть до 2005 года мне казалось, что это задача намного более сложная чем задача исторической генетики, которой я занимался. Во многом это ощущение было результатом устоявшегося и очень распространенного среди математиков мнения, что абстрактную математику невозможно разумным образом формализовать настолько аккуратно, чтобы ее «понимал» компьютер.
В 2005 мне удалось сформулировать несколько идей, которые неожиданно открыли новый подход к одной из основных проблем в основаниях современной математики. Проблему эту можно неформально сформулировать как вопрос о том, как правильно формализовать интуитивное понимание того, что «одинаковые» математические объекты имеют одинаковые свойства. Аргументы, основанные на этом принципе, очень часто используются в современных математических доказательствах, но существующие основания математики (теория множеств Цермело-Френкеля) совершенно неприспособлены для формализации таких аргументов.
Я был очень хорошо знаком с этой проблемой и думал о ней еще в 1989 году, когда Миша Капранов и я работали над теорией поли-катергорий. Тогда нам казалось, что ее решить невозможно. То, что мне удалось понять в 2005 году, скомбинировав идеи теории гомотопий (части современной топологии) и теории типов (части современной теории языков программирования), было совершенно удивительно, и открывало реальные возможности построения того самого языка, на котором люди могут писать доказательства, которые сможет проверять компьютер. Дальше был большой перерыв в моей математической деятельности. [...] К идеям, связанным с компьютерной проверкой доказательств, я вернулся только летом 2009, когда мне стало окончательно ясно, что с исторической генетикой ничего не получается. И буквально через несколько месяцев случились два события, которые продвинули эти идеи от общих наметок, над которыми, я думал, придется работать еще не один год, до стадии, на которой я смог заявить, что я придумал новые основания математики, которые позволят решить проблему компьютерной проверки доказательств. Сейчас это называется «унивалентные основания математики» и ими занимаются как математики, так и теоретики языков программирования. Я почти не сомневаюсь, что эти основания вскоре заменят теорию множеств и что проблему языка абстрактной математики, который будут «понимать» компьютеры можно считать в основном решенной. [...] Первые примеры языков того класса с которыми я работаю, были созданы в конце 1970-ых и известны под названием «Martin-Lof type theories». Удивительным образом языки были, программные системы использующие эти языки создавались и даже становились популярными (особенно система «Coq» которую создали французы), но понимания того, о чем эти языки позволяют говорить, не было. Получалось, что используется только очень небольшая часть возможностей языка, та, которая, как теперь ясно, позволяет говорить про множества. Язык же в целом позволяет говорить про гомотомические типы любого уровня сложности. Разрыв, как ты понимаешь, огромный. Как следствие сами языки не совершенствовались, потому что было не ясно, что можно менять, а что нельзя. Теперь, когда мы понимаем, что в этих языках существенно, а что нет, открывается возможность сделать их значительно более «мощными» и, как следствие, более удобными для практического использования.
Спасибо!
Но насчет замены оснований математики — с этим трудно согласиться.
Но насчет замены оснований математики — с этим трудно согласиться.
Важно понимать, что множества сами по себе никуда не денутся. Замена, о которой говорит Воеводский, происходит на более низком уровне: связка «логика первого порядка + аксиомы ZFC» заменяется на HoTT. Считается, что аксиомы ZFC работающих математиков всё равно не интересуют (кроме специалистов по логике), и в современном виде необходимая математикам теория множеств гораздо лучше формализуется с помощью ETCS.
ETCS инспирирована теорией категорий (но не базируется на ней): в качестве базовых объектов берутся функция и множество (в ZFC базовые объекты — множество и элемент множества), и элементы множества A в ETCS определяются как функции из фиксированного одноэлементного множества в множество A (т.к. эти функции взаимно-однозначно соответствуют элементам A), а «одноэлементность» в свою очередь можно определить как свойство множества иметь ровно одну функцию из любого множества в себя. Подробное изложение для нематематиков можно найти здесь: arxiv.org/abs/1212.6543 Там же можно узнать, почему математики не используют ZFC (например, потому, что число пи в этой системе аксиом является множеством).
В HoTT в свою очередь можно строить объекты, которые работают ровно так, как те штуки, которые описывает ETCS. Эти штуки в HoTT называются множества.
ETCS инспирирована теорией категорий (но не базируется на ней): в качестве базовых объектов берутся функция и множество (в ZFC базовые объекты — множество и элемент множества), и элементы множества A в ETCS определяются как функции из фиксированного одноэлементного множества в множество A (т.к. эти функции взаимно-однозначно соответствуют элементам A), а «одноэлементность» в свою очередь можно определить как свойство множества иметь ровно одну функцию из любого множества в себя. Подробное изложение для нематематиков можно найти здесь: arxiv.org/abs/1212.6543 Там же можно узнать, почему математики не используют ZFC (например, потому, что число пи в этой системе аксиом является множеством).
В HoTT в свою очередь можно строить объекты, которые работают ровно так, как те штуки, которые описывает ETCS. Эти штуки в HoTT называются множества.
т.е. если математика — это химия, текущие основания математики (на множествах) — это атомы, то HoTT — это элементарные частицы, которыми можно описать основания математики, и которые позволяют более точно (т.к. оперируют более фундаментальными понятиями) работать с математикой?
Судя по нику, вы являетесь явным поклонником HoTT.
Спасибо за отрывок из интервью, стало понятней.
Спасибо за отрывок из интервью, стало понятней.
Если я правильно понял, то на пальцах эту теорию можно объяснить так: в нынешнем основании много аксиом, а новое основание превращает их в теоремы и доказывает исходя из меньшего числа аксиом, при этом новое открывает новые возможности, но на текущей математики они не отразятся. Или, аналогия, Математика — язык, компилятор которого написан на Си, нынешнее основание — сам Си, а новое — ассемблер :)
Не являюсь профессиональным математиком, чтобы судить, но на первый дилетансткий взгляд — отличная новая теория, берущаяся за основания математики с неожиданной стороны.
Вот тут можно прочесть краткую историческую справку, чтобы понять, зачем она вообще нужна.
А вот тут — пояснение, что именно в ней нового и чем она отличается от ОТТ.
Вот тут можно прочесть краткую историческую справку, чтобы понять, зачем она вообще нужна.
А вот тут — пояснение, что именно в ней нового и чем она отличается от ОТТ.
Интересно как была организована работа. Какие были соглашения, учитывающие специфику git — он всё же на строки ориентирован, а книга вещь такая — слово вставил и все строки полезли.
Предполагаю, что за вёрстку самой книги, кто-то отвечал отдельно. Но это идея для отличного нового сервиса, что-то вроде вики, но сразу на основе полиграфических шаблонов, у Adobe, возможно, уже что-то в этом роде есть.
man tex
man latex
man latex
У меня уже после комменты мысль мелькнула, что что-то вроде html использовалось. Жаль — путь не для всех.
для всех причастных к науке, это точно
Причем тут наука? Меня интересовала методология совместной работы над книгами вообще.
я про latex имею в виду. В мире исследований математики\программирования его положено знать.
А про методологию совместной работы у меня создаётся впечатление, что её и не было вовсе — кроме той, что подразумевается гитхабом
А про методологию совместной работы у меня создаётся впечатление, что её и не было вовсе — кроме той, что подразумевается гитхабом
Я в курсе. В принципе вы на вопрос ответили, правда в несколько неприятной форме.
Методология и задавалась связкой git и latex (хотя на его месте мог быть любой другой язык логической разметки, в котором переводы строк и прочее форматирование если и есть, то не приветствуется, например html). В диффах были видны целые замененные абзацы, в исходниках представляемые одной строкой, а при хорошем инструменте показывались буквы/слова/предложения.
Просто я надеялся, что можно как-то обойтись без языка разметки (или его не видеть под TUI/GUI) и при этом комфортно просматривать диффы.
Методология и задавалась связкой git и latex (хотя на его месте мог быть любой другой язык логической разметки, в котором переводы строк и прочее форматирование если и есть, то не приветствуется, например html). В диффах были видны целые замененные абзацы, в исходниках представляемые одной строкой, а при хорошем инструменте показывались буквы/слова/предложения.
Просто я надеялся, что можно как-то обойтись без языка разметки (или его не видеть под TUI/GUI) и при этом комфортно просматривать диффы.
...
private
ℕ-get-S : ℕ → ℕ
ℕ-get-S 0 = 42
...
Действительно, очень важная константа для описания множества целых чисел.
Интересно а что дали исследования по основаниям математики в прикладнеом аспекте, их значение для прояснения здания математики я не оспариваю
> «Github был моим фейсбуком (только без милых котиков)»
Очень даже с котиками!
Очень даже с котиками!
классно, в книге есть справочник символов. Как же я ненавидел, когда в учебнике по матану внезапно появлялся какой-нибудь крючок, который автор не удосуживался объяснить!
Заказал в твёрдом переплёте. Хоть и уверен, что ничего не пойму в этой книге, но такие проекты надо поддерживать.
Хотелось бы видеть больше книг по современной высшей математике, написанных в более доступной манере. Я уважаю сухой академический стиль, но всё же сложно переоценить простоту и красочность естественного языка при описании абстрактных понятий. Я не имею в виду научно-популярные труды вроде книг Брайана Грина, в которых вообще нет формул. Ведь мой опыт чтения книг по программированию показывает, что даже сложные практические концепции можно наглядно продемонстрировать и пояснить. Также с большим теплом вспоминаю книги вроде «Наглядная геометрия и топология» и издания «Кванта»…
Спасибо за ваш труд, постараюсь выделить время и полистать вашу книгу.
Спасибо за ваш труд, постараюсь выделить время и полистать вашу книгу.
Интересно, как они работу распределяли. Когда каждый пишет свою главу — все достаточно просто. Кажется достаточно сложным мержить изменения одного файла — что бы правки разных людей не приводили к стилистическим ошибкам.
А планируется ли создание какого-нибудь proof assistants, основанного на HoTT? Мне, как пользователю Coq, очень интересно.
Кажется, да.
>Вместо этого нам нужна децентрализованная система эндорсмента (рекомендаций — прим.)
Endorsement – это скорее поощрение, чем рекомендация.
А статья интересная. И видео тоже занимательное :)
Endorsement – это скорее поощрение, чем рекомендация.
А статья интересная. И видео тоже занимательное :)
Мне кажется движок вроде MediaWiki (с установленным Math extension) лучше бы подошел для этой цели. Хотя признаюсь честно с GitHub знаком весьма поверхностно.
А как бы вот теперь всё это перевести бы на много языков, включая русский, и поддерживать в актуальном состоянии?
Желательно, средствами всё того же github-а…
Желательно, средствами всё того же github-а…
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Команда математиков за полгода написала 600-страничную книгу, используя GitHub