Как «тактика» работает в помощниках по проверке?

Вопрос: Как работает «тактика» у помощников по проверке? Похоже, они являются способами указания того, как переписать термин в эквивалентный термин (для некоторого определения «эквивалентный»). Предположительно, есть формальные правила для этого, как я могу узнать, кто они и как они работают? Они включают в себя больше, чем выбор порядка для бета-сокращения?

Предыстория моего интереса: Несколько месяцев назад я решил, что хочу изучать формальную математику. Я решил пойти с теорией типов, потому что из предварительных исследований это похоже на «Правильный способ делать вещи», и потому что это, кажется, объединяет программирование и математику, что интересно . Я думаю, что моя конечная цель состоит в том, чтобы иметь возможность использовать и понимать помощника по проверке, такого как Coq (особенно мне кажется, что я могу использовать зависимые типы, поскольку мне любопытно, например, представлять типы матриц). Сначала я знал очень мало, даже не элементарного функционального программирования, но я делаю медленный прогресс. Я прочитал и понял большие куски типов и языков программирования (Пирс) и выучил некоторые из Haskell и ML.

$A$$B$$A\wedge B$$A\wedge B$$A$$B$с теми же гипотезами), примените лемму (~ применение функции), разделите лемму о некотором индуктивном типе на случай для каждого конструктора и так далее. Основные тактики могут быть успешными или неудачными в зависимости от контекста, в котором они применяются. Более продвинутая тактика похожа на маленькие функциональные программы, которые запускают базовую тактику, выполняют сопоставление с образцом по терминам в цели и / или предположениям, делают выбор на основе успеха или неудачи тактики и так далее. Более продвинутая тактика связана с арифметикой и другими специфическими теориями. Ключевым документом по тактическому языку Coq является следующее:

• Д. Делахай. Тактический язык для системы Coq . В книге «Труды логики для программирования и автоматического рассуждения» (LPAR), Остров Реюньон, том 1955 «Конспект лекций в области компьютерных наук», стр. 85–95. Springer-Verlag, ноябрь 2000 г.

Формальные правила, которые составляют суть основной тактики, определены в руководстве пользователя Coq здесь или в главе 4 pdf .

Весьма поучительный документ по реализации тактики и тактики (по сути, тактики, которая использует в качестве аргументов другую тактику):

• Эми Фелти. Внедрение тактики и тактики в языке программирования высших порядков журнала автоматического рассуждения, 11 (1): 43-81, август 1993 г.

У тактического языка Кока есть ограничение, заключающееся в том, что написанные с его помощью доказательства едва ли напоминают доказательства, сделанные вручную. Было предпринято несколько попыток дать более четкие доказательства. К ним относятся Изара (для Изабель / HOL) и язык доказательства Мицар .

В сторону: Знаете ли вы, что язык программирования ML изначально был разработан для реализации тактики для доказательства теорем LCF ? Многие идеи, разработанные для ML, такие как вывод типов, повлияли на современные языки программирования.

LCF действительно является прародителем всех этих систем: Coq, Isabelle, HOL, включая язык программирования ML (который мы видим сегодня как OCaml, SML, также F #). Да, я включаю Coq как члена большей семьи LCF. По сравнению с американо-американскими помощниками по доказательствам (в частности, ACL2) или совершенно не связанным с ним Мизаром, Кок культурно довольно близок к Изабель и HOL, главным образом из-за общей идеи тактики .

Так что же такое тактика, лишенная случайных наблюдений за переписыванием, преобразованием, введением или устранением связок?

Основной принцип наслоения здесь унаследован от LCF Милнера:

• Основные выводы (прямое рассуждение), либо как абстрактный тип данных thmв исходном LCF-подходе, либо с отдельной проверкой проверочных терминов в ветви семейства «Теория типов» (Coq, Matita). Это дает вам определенную логическую основу для результатов, которые проверяющий считает теоремами. Таким образом, у вас может быть примитивный вывод, который принимает ⊢ A и ⊢ B и дает вам ⊢ A ∧ B. Другой примитивный вывод может дать вам ⊢ t = u, где u - бета-нормальная форма t. Ни один из этих механизмов не является тактикой, хотя они являются правилами вывода, как в стандартной логике.

• Целенаправленное доказательство (обратное рассуждение). Идея в том, что вы оперируете некоторым понятием «целевого состояния», уточняя его, разделяя его на все больше и больше подцелей, закрывая подцели, пока все не будет решено. Завершая состояние цели, из процесса выскочит определенная теорема. LCF ввел некоторую экстралогическую инфраструктуру для целей, которая все еще присутствует в HOL: тактика - это некоторая функция ML, которая уточняет цель и дает некоторое обоснование для уточнения. В самом конце доказательства, судебные разбирательства воспроизводятся в обратном порядке, чтобы произвести доказательство в прямом направлении в соответствии с примитивными выводами, нарисованными выше.

Coq и Matita все еще довольно близки к этому принципу LCF. Изабель здесь иная: еще в 1989 году Ларри Полсон реформировал понятия цели и тактики, чтобы приблизить их к логике, которая является «чистой» логической основой Изабель здесь. Изабель / Pure обеспечивает минимальную логику высшего порядка с импликацией ==> и квантификатором !! которые указывают как на структуру естественных правил удержания, так и на целевые состояния.

Например, ⊢ A ==> B ==> A ∧ B - это правило введения конъюнкции (объектной логики) как теорема логической структуры.

Состояния целей также являются просто теоремами, начиная с ⊢ C ==> C для вашего начального утверждения C, которое уточняется до ⊢ X ==> Y ==> Z ==> C в промежуточных состояниях, где X, Y, Z являются текущими подцелями, и процесс завершается с помощью ⊢ C (без подцелей).

Теперь вернемся к тактике, которая является более унифицированной для всех этих пруверов: учитывая некоторое представление о состоянии цели (например, Изабель выше), тактика - это функция, которая отображает состояние цели в (0, 1 или более) последующих действий. цель государства. Кроме того, тактический является комбинатором таких тактических функций, например , для выражения последовательной композиции, выбора, повторить и т.д. На самом деле, язык тактики и tacticals связан с «перечнем успехов» подход синтаксического анализатора комбинаторов.

Тактика позволяет систематически описывать определенные стратегии уточнения целей. Они оказались довольно успешными с момента их изобретения в LCF в 1970/80-х годах, но они производят общеизвестно нечитаемые сценарии доказательства.

Недавний обзор некоторых аспектов тактических языков приведен в документе А. Асперти и др., PLMMS 2009, см. Материалы семинара, стр. 22.

Мизар и Изабель / Изар были упомянуты как альтернативные подходы к понятным для человека структурированным рассуждениям , и в этом смысле они не основаны на тактике. Мизар не имеет отношения к семье LCF, поэтому он не знает этой тактической терминологии. Изабель / Изар в некоторой степени включает в себя тактическую традицию, но ее понятие метода доказательства немного более структурировано (с явным контекстом доказательства Изара, явным указанием связанных цепей фактов и избеганием внутреннего взлома целей в ходе рассуждений).

В последние десятилетия произошло гораздо больше реформ и пересмотров тактических языков. Например, недавняя ветвь сообщества Coq предпочитает SSReflect (G. Gonthier) вместо традиционного Ltac.

Как «тактика» работает в помощниках по проверке?

Я подозреваю, что этот ответ будет немного бессмысленным.

Во-первых, недостаточно спросить «как работают тактики в помощниках по проверке», потому что они работают по-разному в разных помощниках по проверке. Сегодня используются два основных класса помощников: те, которые получены из оригинального LCF, такие как Isabelle, HOL и HOL light, и ассистенты, основанные на теории типов, такие как Coq и Matita. В этих двух разных классах помощника по доказательству тактика работает по-разному, отражая то, что то, что происходит под капотом, например, в Изабель, совершенно отличается от того, что происходит под капотом, например, в Матите.

Спросите себя: что происходит, когда мы пытаемся доказать утверждение P в Матите? Мы вводим мета-переменную X с типом P. Затем мы, так сказать, играем в игру, где мы уточняем X, добавляя все больше и больше структур к неполному члену, пока не получим полный лямбда-член (то есть не содержащий больше метавариабельных переменных). Как только мы получим полный лямбда-термин, мы проверяем его тип относительно P, чтобы убедиться, что он содержит требуемый тип. Затем мы видим, что в Coq и Matita тактика - это просто функция от неполных терминов доказательства до неполных терминов доказательства, что, мы надеемся, добавляет немного структуры к термину после применения (это наблюдение мотивировало довольно недавнюю работу, например, Джойгова). , Пентка и др.)

Например, тактика Matita «intro» вводит лямбда-абстракцию над существующим термином, «case» вводит выражение соответствия в этом термине, а «apply» вводит применение одного термина к другому. Эти основные тактики можно связать вместе, используя функции более высокого порядка, чтобы создать более сложные. Основная идея всегда одна и та же: тактика всегда нацелена на добавление некоторой структуры к неполному доказательству.

Обратите внимание, что разработчики стремятся вернуть термин, который снова проверяется после каждого тактического приложения. Строго говоря, для них нет необходимости делать это, поскольку все, что имеет значение для помощников по доказательству на основе теории типов, состоит в том, что, когда пользователь приходит к Qed доказательству, мы располагаем термином доказательства, который обитает в предложении P. Как мы Пришедший к этому доказательству термин в значительной степени не имеет значения. Однако и Coq, и Matita стремятся вернуть пользователю (возможно, неполный) проверочный термин, который проверяет тип после каждого применения тактики. Тем не менее, этот инвариант может (и часто не работает) терпеть неудачу, особенно в том, что касается двух синтаксических проверок, которые должны выполнять корректоры на основе CIC.

В частности, мы можем выполнить то, что представляется убедительным доказательством, применяя серию тактик, пока не останется открытых целей. Затем мы приходим к Кеду предполагаемому доказательству, только чтобы обнаружить, что проверка завершения Матиты или ее строгая проверка положительности жалуются, поскольку термин доказательства, сгенерированный тактикой, лишил законной силы одну из этих синтаксических проверок (т. Е. Мета-переменную в позиции аргумента для был создан экземпляр рекурсивного вызова с термином, который синтаксически не меньше исходного аргумента). Это является отражением того, что теория типов CIC в некотором смысле не является «достаточно сильной» и не отражает синтаксические требования позитивности или размера в ее типах (наблюдение, мотивирующее размерные типы Абеля, и некоторые недавние работы над типами позитивности). ).

С другой стороны, ассистенты в стиле LCF совсем другие. Здесь ядро ​​состоит из модуля (обычно реализуемого в варианте ML), содержащего абстрактный тип «thm», и функций, которые реализуют правила вывода логики ассистента проверки, отображения «thm» в «thm» и т. Д. вперед. Мы полагаемся на типизацию дисциплины ML, чтобы гарантировать, что единственный способ конструировать значение типа «thm» - это правила вывода (базовая тактика). Ядро Изабель здесь .

Доказательства затем состоят из ряда применений этих основных тактик (или более сложных, более масштабных тактик, которые снова создаются путем объединения более простых тактик с использованием функций высшего порядка) - в Изабель функции высшего порядка, называемые тактическими, могут быть увиденным здесь ). В отличие от помощников по доказательству, основанных на теории типов, в помощнике в стиле LCF нет необходимости хранить явный термин «доказательство» в качестве свидетеля. Правильность доказательства гарантируется конструкцией и нашим доверием к дисциплине набора текста в ML (однако многие помощники, например Изабель, генерируют термины доказательства для своих доказательств).