Учитывая темы, затронутые на конференции, такие как STOC, активно ли исследователи алгоритмов или сложности используют COQ или Изабель? Если да, то как они используют это в своих исследованиях? Я предполагаю, что большинство людей не будут использовать такие инструменты, потому что доказательства были бы слишком низкими. Кто-нибудь использует этих помощников в доказательстве таким образом, который имеет решающее значение для их исследований, в отличие от хорошего дополнения?
Мне интересно, потому что я мог бы начать изучать один из этих инструментов, и было бы интересно узнать о них в контексте доказательств сокращения, правильности или времени выполнения.
Ответы:
Общее эмпирическое правило заключается в том, что чем более абстрактной / экзотической математикой вы хотите заниматься, тем легче становится. И наоборот, чем конкретнее / знакомее математика, тем сложнее будет. Так (например) редкие животные, такие как предикативная топология без точек, гораздо легче механизировать, чем обычная метрическая топология.
Поначалу это может показаться немного удивительным, но это в основном потому, что конкретные объекты, такие как действительные числа, участвуют в большом разнообразии алгебраических структур, и доказательства с их помощью могут использовать любое свойство из любого их представления. Таким образом, чтобы иметь обыкновение рассуждать, к которому привыкли математики, вы должны механизировать все эти вещи. Напротив, высоко абстрактные конструкции обладают (намеренно) небольшим и ограниченным набором свойств, поэтому вам придется гораздо меньше механизировать, прежде чем вы добьетесь хороших результатов.
Доказательства в теории сложности и алгоритмах / структурах данных имеют тенденцию (как правило) использовать сложные свойства простых гаджетов, таких как числа, деревья или списки. Например, комбинаторные, вероятностные и теоретико-числовые аргументы обычно появляются одновременно в теоремах теории сложности. Получение поддержки библиотеки «Доказательство помощника» до такой степени, что это приятно делать - довольно много работы!
Один контекст, в который люди готовы вкладывать свои работы, - это криптографические алгоритмы. Существуют очень тонкие алгоритмические ограничения по сложным математическим причинам, и поскольку криптографический код выполняется в состязательной среде, даже малейшая ошибка может иметь катастрофические последствия. Так, например, проект Certicrypt построил много инфраструктуры верификации с целью создания проверенных компьютером доказательств правильности криптографических алгоритмов.
источник
Одним из наиболее ярких примеров является, конечно, формализация Gonthiers Coq теоремы о 4 цветах в Coq, в которой используется много комбинаторики.
Мой коллега Ули Шёпп использовал библиотеку ssreflect, разработанную Gonthier для этой цели, чтобы проверить (и немного расширить) также в Coq результат, полученный Cook и Rackoff на автоматах графа. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Формализованная нижняя граница достижимости неориентированного графа. В логике для программирования, искусственного интеллекта и рассуждения ( С. 621-635). Спрингер Берлин / Гейдельберг.)
источник