Каковы негативные последствия расширения CIC с аксиомами?

13

Правда ли, что добавление аксиом в CIC может оказать негативное влияние на вычислительное содержание определений и теорем? Я понимаю , что в нормальном поведении теории, любой замкнутый терм сведет к канонической нормальной форме, например , если верно, то п должен сводиться к слагаемому виду ( S у с с . . . ( S U c c ( 0 ) ) ) . Но при постулировании аксиомы - скажем, аксиомы экстенсиональности функции - мы просто добавляем новую константу в системуN:NN(sUсс,,,(sUсс(0)))funext

еUNеИксT:ΠИкс:Aе(Икс)знак равнограмм(Икс)езнак равнограмм

это просто «волшебным образом» производит доказательство из любого доказательства Π x : A f ( x ) = g ( x ) , без какого-либо вычислительного значения вообще ( в том смысле, что мы не можем извлечь из них какой-либо код? )езнак равнограммΠИкс:Aе(Икс)знак равнограмм(Икс)

Но почему это "плохо"?

Для funext, я прочитал в этой записи Coq и этот mathoverflow вопросе , что это приведет систему к любой свободной каноничности или разрешимой проверке. Запись coq, кажется, представляет собой хороший пример, но я все еще хотел бы еще несколько ссылок на это - и почему-то я не могу найти их.

Как такое добавление дополнительных аксиом может привести к ухудшению поведения CIC? Любые практические примеры были бы великолепны. (Например, аксиома однолистности?) Боюсь, что этот вопрос слишком мягкий, но если бы кто-то мог пролить свет на эти вопросы или дать мне некоторые ссылки, было бы здорово!


PS: В записи Coq упоминается, что «Тьерри Коканд уже заметил, что сопоставление с образцом по интенциональным семьям несовместимо с экстенсиональностью в середине 90-х». Кто-нибудь знает, в какой газете или что-то?

StudentType
источник

Ответы:

7

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

  • Теоретически, каноничность позволяет вам доказать ценности своего языка, не прибегая к конкретной модели. Это очень приятное свойство думать о вашей системе; в частности, он поддерживает утверждения о реальном мире - мы можем думать о natтипе, формализованном в системе, как о действительно «натуральных числах», потому что мы можем доказать, что его замкнутые нормальные жители действительно являются натуральными числами. В противном случае легко подумать, что вы правильно смоделировали что-то в своей системе, но на самом деле работаете с другими объектами.

  • На практике сокращение - это основной актив теорий зависимого типа, потому что это облегчает доказательство. Доказательство пропозиционального равенства может быть сколь угодно сложным, в то время как доказательство равенства определений (реже возможно), но гораздо проще, так как термин доказательства тривиален. В более общем смысле, вычисления являются ключевым аспектом пользовательского опыта помощника по проверке, и обычно определяют вещи просто так, чтобы они правильно сокращались, как вы ожидаете. (Вам не нужны аксиомы, чтобы усложнить вычисления; например, использование принципа преобразования для пропозициональных равенств уже может блокировать сокращения). Весь бизнес доказательства отражениемоснован на использовании вычислений, чтобы помочь доказательствам. Это серьезное различие в силе и удобстве в отношении других основанных на логике помощников по проверке (например, HOL-light, который поддерживает только рассуждения о равенстве; или см. Zombie для другого подхода) и использования непроверенных аксиом или других стилей программирования, может вывести вас из этой зоны комфорта.

gasche
источник
+1 Спасибо за ваш ответ! Не могли бы вы дать мне несколько примеров аксиом, которые имеют вычислительную интерпретацию (или, может быть, какую-либо ссылку на предмет)?
StudentType
Одним из примеров аксиомы, имеющей вычислительную интерпретацию, является Prop-Нерелевантность: утверждение, что все обитатели некоторого семейства типов (в данном конкретном случае, те, что Propв помощниках по доказательству Coq, соответствуют чисто логическим утверждениям; Prop-Нерелевантность соответствуют игнорировать внутреннюю структуру доказательств этих утверждений) можно сделать в основном, не заботясь о них больше, это не должно влиять на вычисления - но это нужно делать осторожно, чтобы не сделать систему несовместимой.
Гаше
Другое семейство вычислительных интерпретаций происходит из соответствий между классическим рассуждением и управляющим эффектом. Более известной частью этого является то, что исключенной середине может быть дана вычислительная семантика путем захвата продолжения, но существуют ограниченные формы управления (исключения при положительных типах), которые дают более тонкие логические принципы (например , принцип Маркова ). См. Интуиционистскую логику Хьюго Гербелина , доказывающую принцип Маркова , 2010.
Гаш
5

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

  • В теории типов наблюдений можно постулировать доказательство любого непротиворечивого, Propне теряя каноничности. Действительно, все доказательства считаются равными, и система обеспечивает это, полностью отказываясь рассматривать термины. Как следствие, тот факт, что доказательство было построено вручную или просто постулировано, не имеет никакого значения. Типичным примером может служить доказательство «сплоченности»: если у нас есть доказательство eqэтого, A = B : Typeто для любого tтипа A, t == coerce A B eq tгде coerceпросто переносится член вдоль доказательства равенства.

  • В MLTT можно постулировать любую отрицательную последовательную аксиому без потери каноничности . Интуиция позади этого состоит в том, что отрицательные аксиомы (аксиомы формы A -> False) когда-либо используются только, чтобы отклонить несущественные ветви. Если аксиома непротиворечива, то она может использоваться только в тех ветвях, которые действительно не имеют значения и поэтому никогда не будут приниматься при оценке терминов.

Gallais
источник
4

Практический пример плохого поведения аксиомы вы спрашиваете, а как насчет этого?

 0 = 1

Упомянутая статья Coquand может быть [1], где он показывает, что зависимый ITT (интуиционистская теория типов Мартина-Лёфа), расширенная с помощью сопоставления с образцом, позволяет вам доказать UIP (аксиома уникальности доказательств идентичности ). Позже Штрайхер и Хоффманн [2] представляют модель ITT, которая фальсифицирует UIP. Следовательно, сопоставление с образцом не является консервативным расширением ITT.


  1. Т. Coquand, сопоставление с образцом зависимых типов .

  2. М. Хофманн, Т. Штрайхер, Группоидная интерпретация теории типов .

Мартин Бергер
источник