Ответ 1

В основном я знаком с Coq и не имею большого опыта работы с Isabelle/HOL, но я мог бы немного помочь. Возможно, другие, имеющие больше опыта работы с Isabelle/HOL, могут помочь улучшить это.

Существуют две большие точки расхождения между двумя системами: лежащие в основе теории и стиль взаимодействия. Я попытаюсь дать краткий обзор основных различий в каждом случае.

Теория

Оба Coq и Isabelle/HOL основаны на мощных, очень выразительных логиках более высокого порядка. Однако эти логики отличаются несколькими особенностями:

Зависимые типы

Coq-логика - это теория зависимого типа, известная как исчисление индуктивных конструкций (короткое замыкание на CIC). "Зависимый тип" здесь означает, что типы в Coq могут относиться к обычным значениям. Например, можно написать функцию умножения матрицы mult с типом

mult : forall (n m p : nat), matrix n m -> matrix m p -> matrix n p

Тип этой функции говорит о том, что в качестве входов используются две матрицы: один из размерности n x m и другой размерности m x p, и возвращает матрицу размерности n x p. С другой стороны, теория Изабель /HOL не обладает зависимыми типами; следовательно, нельзя написать функцию mult с тем же типом, что и выше. Вместо этого нужно написать функцию, которая работает для любой матрицы, и доказать апостериорные определенные свойства этой функции, когда она получает аргументы правильных видов. Другими словами, некоторые свойства, которые проявляются в типах Coq, должны утверждаться как отдельные теоремы при работе с Isabelle/HOL.

В то время как зависимые типы интересны для некоторых вещей, неясно, насколько они полезны в целом. У меня сложилось впечатление, что некоторые считают, что они очень сложны в использовании, и что преимущество наличия определенных свойств, выраженных на уровне типа, в сравнении с их как отдельными теоремами, не стоит этой дополнительной сложности. Лично мне нравится использовать зависимые типы в нескольких случаях, когда есть явные причины для этого.

Общие аксиомы

Теория Кок по умолчанию не имеет многих основополагающих принципов, которые являются обычными в математической практике, таких как закон исключенной середины (т.е. способность рассуждать неконструктивно), расширение (например, способность сказать, что функции, которые дают равные результаты, сами по себе равны) и аксиома выбора. С другой стороны, в Isabelle/HOL такие принципы встроены.

В теории, это не большая проблема, потому что логика Coq была разработана, чтобы позволить людям безопасно добавлять эти принципы рассуждения в качестве дополнительных аксиом. Тем не менее, у меня сложилось впечатление, что легче рассуждать по Isabelle/HOL, поскольку логика была построена с нуля, чтобы поддержать их.

Стиль взаимодействия

Оба Coq и Isabelle/HOL являются интерпретаторами интерактивных теорем. Это языки для написания определений и доказательств о них; эти доказательства проверяются компьютером, чтобы убедиться, что у них нет ошибок. В обеих системах один записывает доказательство, предоставляя команды, которые объясняют, как что-то доказывать. Однако, как это происходит в каждой системе, меняется.

Isabelle/HOL, как правило, имеет более зрелую поддержку для "кнопочной" автоматизации. Например, он имеет известную тактику sledgehammer, которая вызывает несколько внешних автоматических теоретических предсказателей и решателей, чтобы попытаться доказать теорему. Coq также поставляется со многими мощными процедурами автоматизации доказательств, такими как omega или congruence, но они не так общеприменимы, и многие теоремы, которые могут быть решены с помощью одной команды в Isabelle/HOL, требуют более явных доказательств в Coq.

Конечно, это удобство поставляется с ценой. Мне сказали, что сложнее иметь контроль над одним доказательством в Isabelle/HOL, потому что система пытается сделать многое сама по себе. Это не проблема при доказательстве простых теорем, но это становится проблемой, когда автоматизация доказательств недостаточно сильна, и вам нужно сообщить теорему о том, как действовать более подробно.

Ситуация немного отличается при поддержке пользовательских процедур проверки достоверности. Coq поставляется с тактическим языком для написания доказательств, известных как Ltac, который является языком программирования. Несмотря на то, что у Ltac есть некоторые проблемы с дизайном, он позволяет пользователям легко кодировать довольно сложные процедуры автоматизации процедур. Для более тяжелых задач Coq также позволяет пользователям писать плагины на языке реализации Coq, OCaml. Напротив, в Isabelle/HOL нет языка автоматизации более высокого уровня, такого как Ltac, и единственный способ, которым пользователь может программировать процедуры автоматической проверки подлинности, - с плагинами.

Ответ 2

Поскольку вопрос "Isabelle/HOL" задан в вопросе, я расскажу о логике HOL, используемой в Isabelle, которая, по моему мнению, является лучшей для сравнения с Coq. Я не специалист в системах типов и логике, но я думаю, что я говорю здесь правильно, по крайней мере примерно. Это также, безусловно, вопрос вкуса;-), и мой ответ может быть субъективным.

Наиболее глубокие различия заключаются в системах типов и логике.

Я бы сказал, что сила должна быть более естественной для тех, кто знает функциональный язык семейства ML (и даже больше того, кто знает SML), и он использует прагматичный подход для решения проблем, например, использование классическая логика как основа. Его система типов близка к Hindley Milner one и завершается по умолчанию (если она не изменена пользователем).

С другой стороны, Coq является более строгим и использует интуиционистскую логику. Он имеет специализированную систему типов с несколькими заказами и позволяет зависимостям типов, которые могут быть сложнее обрабатывать и в некоторых случаях могут не прерываться. Он также позволяет извлекать программы из доказательств (которые могут быть относительно неэффективными), что невозможно в Isabelle.

Ответ 3

Одним из аспектов, который я проиллюстрирую, "кнопочной" эффективностью Isabelle/HOL является его автоматизация классического "диагонализации" Кантора (напомним, что это говорит о том, что не существует сюръекции от naturals к его силовому набору или, вообще говоря, никакого набора его набора мощности).

theorem Cantor: "∄f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x"
proof
  assume "∃f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x"
  then obtain f :: "'a ⇒ 'a set" where *: "∀A. ∃x. A = f x" ..
  let ?D = "{x. x ∉ f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a ∈ ?D ⟷ a ∉ f a" by blast
  ultimately show False by blast
qed

То, что я только что представил вам, станет переводом классического аргумента Кантора в Изабель /HOL. Без сомнения, изобретательный! Однако Isabelle/HOL может автоматизировать проницательность даже из этого доказательства:

theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A"
  by best

theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A"
  by force

Система доказательств может автоматически доказывать оператор Кантора. Для исследователя, с одной стороны, это полезно, но есть смысл, в котором это обоюдоострый меч. Я могу счесть полезным, что истинным утверждениям, столь сложным, как аргумент диагонализации, можно доверять, чтобы быть внутренне доказанными для Изабель /HOL, так как мои теоремы более сложны. С другой стороны, чем дальше я продвигаюсь в своих исследованиях благодаря автоматизированному прогрессу компьютера, я все меньше и меньше объясняю, почему или по какому принципу теорема верна. Только компьютер знает, почему, если только мы можем спросить об этом!