Неглубокие и глубокие вложения

При кодировании логики в ассистенте доказательства, таком как Coq или Isabelle, необходимо сделать выбор между использованием поверхностного и глубокого встраивания. При неглубоком встраивании логические формулы записываются непосредственно в логику доказательства теоремы, тогда как при глубоком встраивании логические формулы представляются в виде данных.

• Каковы преимущества и ограничения различных подходов?
• Есть ли какие-либо руководящие принципы для определения, что использовать?
• Можно ли переключаться между двумя представлениями любым систематическим способом?

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

Каковы преимущества и ограничения различных подходов?

• Плюсы глубоких вложений: Вы можете доказать и определить вещи по индукции в структуре формул. Примерами интересов являются размеры формулы.

• Минусы глубоких вложений: Вы имеете дело с привязкой переменных. Это обычно очень трудоемко.

Есть ли какие-либо руководящие принципы для определения, что использовать?

Неглубокие вложения очень полезны для импорта результатов, доказанных в логике объекта. Например, если вам нужно что-то доказать в небольшой логике (например, в логике разделения), мелкие вложения могут быть предпочтительным инструментом для импорта вашего результата в Coq.

С другой стороны, глубокое встраивание почти обязательно, когда вы хотите доказать мета-теоремы об объектной логике (например, обрезание-исключение).

Можно ли переключаться между двумя представлениями любым систематическим способом?

Идея, лежащая в основе мелкого встраивания, заключается в том, чтобы работать непосредственно в модели формул объекта. Обычно люди привязывают формулу объекта P напрямую (используя нотации или делая перевод вручную) к жителю Prop. Конечно, есть жители Prop, которые нельзя получить, внедрив формулу объектной логики. Поэтому вы теряете какую-то полноту.

Таким образом, можно отправить каждый результат, полученный в режиме глубокого встраивания, через функцию интерпретации.

Вот небольшой пример coq:

Индуктивная формула: Set: =
    Ftrue: формула
  | Ffalse: формула
  | Фанд: формула -> формула -> формула
  | Для: формула -> формула -> формула.

Интерпретация фиксированной точки (F: формула): Prop: = соответствует F с 
    Ftrue => Правда
  | Ложь => Ложь
  | Fand ab => (интерпретировать a) / \ (интерпретировать b)
  | Для ab => (интерпретировать a) \ / (интерпретировать b)
 конец.

Индуктивный вывод: формула -> Опора: = 
    deep_axiom: производное Ftrue
  | deep_and: вывод ab, выводимый a -> выводимый b -> выводимый (Fand ab)
  | deep_or1: все ab, производные a -> производные (для ab)
  | deep_or2: все ab, производные b -> производные (для ab).

Индуктивный sderivable: Опора -> Опора: = 
    shallow_axiom: sderivable True 
  | shallow_and: все ab, sderivable a -> sderivable b -> sderivable (a / \ b)
  | shallow_or1: все ab, sderivable a -> sderivable (a \ / b)
  | shallow_or2: для всех ab, sderivable b -> sderivable (a \ / b).

(* Вы можете доказать следующую лемму: *)
Лемма shallow_deep: 
   для F, вывод F -> srerivable (интерпретировать F).

(* Вы не можете доказать следующую лемму: *)
Лемма т: 
   для всего P, можно найти P -> существует F, интерпретировать F = P.

Грубо говоря, с глубоким встраиванием логики вы (1) определяете тип данных, представляющий синтаксис вашей логики, и (2) задаете модель синтаксиса , и (3) доказываете, что аксиомы о вашем синтаксисе являются правильными в отношении к модели. При неглубоком встраивании вы пропускаете шаги (1) и (2), просто начинаете с модели и доказываете соответствия между формулами. Это означает, что мелкие встраивания, как правило, требуют меньше усилий, чтобы оторваться от земли, поскольку они представляют собой работу, которую вы обычно выполняете в любом случае с глубоким встраиванием.

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

Правильная последовательность, которую вы должны принять: (1) попытаться обойтись мелким вложением. (2) Когда это закончится, попробуйте использовать тактику и цитату, чтобы выполнить процедуры принятия решения, которые вы хотите выполнить. (3) Если и этого не хватает, откажитесь и используйте синтаксис с зависимой типизацией для глубокого внедрения.

• Запланируйте пару месяцев на (3), если это ваш первый раз. Вам будет необходимо ознакомиться с фантазии особенности вашего доказательства помощника остаться в здравом уме. (Но это инвестиции, которые в целом окупятся.)
• Если у вашего помощника по проверке нет зависимых типов, оставайтесь на уровне 2.
• Если ваш объектный язык сам по себе типизирован, оставайтесь на уровне 2.

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

РЕДАКТИРОВАТЬ: Вот комментарий, объясняющий, почему подниматься вверх по лестнице постепенно так заманчиво, и почему это приводит (в целом) к страданиям.

В частности, предположит , что у вас есть неглубокое вложение логики разделения, с связками и блоком . Затем вы докажете теоремы типа и и так далее. Теперь, когда вы попытаетесь фактически использовать логику, чтобы доказать правильность программы, у вас будет что-то вроде и вы действительно захотите что-то вроде .$A \star B$$I$$A \star B \iff B \star A$$(A \star B) \star C \iff A \star (B \star C)$$(I \star A) \star (B \star C)$$A \star (B \star (C \star I))$

На этом этапе вы будете раздражены необходимостью повторного связывания формул и подумаете: «Я знаю! Я буду интерпретировать тип данных списков как список отдельных формул. Таким образом, я могу интерпретировать как объединение этих списков, и тогда приведенные выше формулы будут определенно равны! »$\star$

Это правда и работает! Тем не менее, обратите внимание, что соединение также ACUI, как и дизъюнкция. Таким образом, вы пройдете тот же процесс в других доказательствах с разными типами данных списка, а затем у вас будет три синтаксиса для разных фрагментов логики разделения, и у вас будут метатеоремы для каждого из них, которые неизбежно будут разными, и вы обнаружите, что вам нужен метатеорем, который вы доказали для разделения соединения для дизъюнкции, и затем вы захотите смешать синтаксисы, и тогда вы сойдете с ума.

Лучше нацеливаться на самый большой фрагмент, который вы можете обработать с разумным усилием, и просто сделайте это.

Важно понимать, что существует спектр от глубокого до неглубокого. Вы глубоко моделируете части своего языка, которые должны каким-то образом участвовать в некоем индуктивном споре о его построении, остальное лучше оставить в мелком представлении о прямой семантике субстрата логики.

Например, если вы хотите рассуждать о Hoare Logic, вы можете поверхностно смоделировать язык выражений, но набросок языка assign-if-while должен представлять собой конкретный тип данных. Вам не нужно вводить структуру x + y или a <b, но вам нужно работать с whileт. Д.

В других ответах были намеки на зависимые типы. Это напоминает о древней проблеме представления языков со связующими в разумном виде, чтобы они были как можно более мелкими, но все же допускали некоторые индуктивные аргументы. У меня сложилось впечатление, что жюри все еще судит обо всех различных подходах и документах, которые появились за последние 10-20 лет на эту тему. «Проблема POPLmark» для различных сообществ помощников по проверке также была в некоторой степени такой же.

Как ни странно, в классической HOL без зависимых типов подход HOL-Nominal К. Урбана работал достаточно хорошо для поверхностного связывания, хотя он и не догонял культурные сдвиги в этих сообществах формализации на языке программирования.