Почему у Coq есть опора?

35

Coq имеет тип Prop несущественных доказательств, которые отбрасываются при извлечении. Какова причина этого, если мы используем Coq только для доказательств? Prop является непредсказуемым, поэтому Prop: Prop, однако, Coq автоматически выводит индексы юниверса, и мы можем использовать Type (i) вместо этого везде. Кажется, Prop все сильно усложняет.

Я читал, что в книге Луо есть философские причины разделения Set и Prop, однако я не нашел их в книге. Кто они такие?

Константин Соломатов
источник
6
«Если мы будем использовать Coq только для доказательств»: я думаю, что вы определили ключевой момент здесь. Coq не используется только для доказательств.
Жиль "ТАК - перестань быть злым"

Ответы:

34

очень полезно для извлечения программыпоскольку она позволяет удалять части кода, которые бесполезны. Например, чтобы извлечь алгоритм сортировки, мы должны доказать утверждение «для каждого списка существует список k такой, что k упорядочено, а k является перестановкой ». Если мы запишем это в Coq и извлечем без использования P r o p , мы получим:PropkkkProp

  1. «для всех есть к » даст нам карту , которая принимает списки в списки,ksort
  2. «такой, что упорядочено» даст функцию, которая проходит через k и проверяет, что она отсортирована, иkverifyk
  3. « перестановка л » даст перестановку , которая принимает л к к . Обратите внимание, что это не только отображение, но и обратное отображение вместе с программами, проверяющими, что две карты действительно являются обратными.kpikpi

Хотя лишние вещи не являются абсолютно бесполезными, во многих приложениях мы хотим от них избавиться и сохранить справедливость sort. Это может быть достигнуто, если мы используем чтобы указать, что « k упорядочено» и « k является перестановкой », но не «для всех существует k ».Propkkk

В общем, распространенным способом извлечения кода является рассмотрение оператора вида где x - вход, y - выход, а ϕ ( x , y ) объясняет, что означает, что y является правильным выводом. (В приведенном выше примере A и B являются типами списков, и ϕ ( , k ) - это « k упорядочено, а k - перестановка .») Если ϕ находится в P r o p, то извлечение дает отображение f :x:A.y:B.ϕ(x,y)xyϕ(x,y)yABϕ(,k)kkϕProp такойчто φ ( х , е ( х ) ) выполняется для всех х . Если ϕ находится в S e t, то мы также получаем функцию g такую, что g ( x ) является доказательством того, что ϕ ( x , f ( x ) ) выполняется для всех x Af:ABϕ(x,f(x))xAϕSetgg(x)ϕ(x,f(x))xA, Часто доказательство бесполезно в вычислительном отношении, и мы предпочитаем от него избавляться, особенно когда оно глубоко вложено в какое-то другое утверждение. дает нам возможность сделать это.Prop

Добавлено 2015-07-29: Существует вопрос , можно ли избежать в целом, автоматически оптимизируя прочь «бесполезный выделенный код». В некоторой степени мы можем сделать это, например, весь код, извлеченный из отрицательного фрагмента логики (материал, построенный из пустого типа, типа модуля, продуктов), бесполезен, поскольку он просто перемещается вокруг модуля. Но есть настоящие дизайнерские решения приходится делать при использовании Р г о р . Вот простой пример, где Σ означает, что мы находимся в T y p e, а означает, что мы находимся в P p o p . Если мы извлекаем из PropPropΣTypeProp мы получим программу, которая разбивает n на младший бит b и оставшиеся биты k , т. е. вычисляет все. Если мы извлечем из Π n : N Σ b : { 0 , 1 }k : N

Πn:NΣb:{0,1}Σk:Nn=2k+b
nbk тогда программа будет вычислять только младший бит b . Машина не может сказать, какая из них правильная, пользователь должен сказать ей, что он хочет.
Πn:NΣb:{0,1}k:Nn=2k+b
b
Андрей Бауэр
источник
1
Я немного смущен. Вы говорите, что без было бы невозможно распознать в извлеченной программе, что g ( x ) не способствует выводу (то есть, что он просто проверяет это)? Существуют ли сценарии, в которых нельзя было бы извлечь такой бесполезный код обычными средствами, доступными оптимизаторам кода? Propg(x)
Пользователь
1
Из извлеченной программы можно сказать: «Я хочу » и вернуться оттуда. Я не смог придумать сценарий, настолько запутанный, что мы не смогли бы оптимизировать что-либо, что не способствовало бы непосредственному определению перестановки, без того, чтобы это фактически было необходимо для вычисления упомянутой перестановки (в любом случае, с точки зрения глобальной оптимизации) ). k
пользователь
1
У вас нет информации "Я хочу ". Это дополнительное предположение, и, очевидно, когда они скажут вам, какого именно результата они хотят, вы можете просто оптимизировать мертвый код. На самом деле, я думал , что лучший ответ: это дизайн вопрос , какие вещи положить в Р г о р . Вы должны знать, что хочет пользователь, и он говорит вам, что он хочет, используя P r o p . Легко придумать примеры, где есть несколько вариантов. Я добавлю один к моему ответу. kPropProp
Андрей Бауэр
2
Насколько я знаю, никто не может сказать, как извлечь что-либо из -типа. Понятно, что они содержат некоторый вычислительный контент, но не то, что это может быть. (1)
Андрей Бауэр
3
Ах хорошо. Использование а способ определения проектных решений делает намного больше смысла для меня , чем как способ удаления бесполезного кода. Prop
пользователь
19

являетсянепредсказуемым, что создает очень выразительную систему доказательств. Однако это «слишком» выразительно в следующем смысле:Prop

impredicative Prop+large elimination+excluded middle

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

Coq сделал оба! Они переименовали предикативную Проповеди в Сет, и отключили большое устранение в Проп.

Выразительность, полученная благодаря непредсказуемости, является «обнадеживающей» в том смысле, что с ее помощью можно формализовать 99% «разумной» математики, и, как известно, она последовательна по отношению к теории множеств. Это делает вероятным, что они не ослабят это до чего-то вроде Агды, которая имеет только предикативные вселенные.

Коди
источник
8
О, и я забыл упомянуть: это не тот случай Prop : Prop, который будет противоречивым. Скорее количественное определение по всем предложениям снова предложение.
cody
Не могли бы вы указать мне больше ресурсов об этом? Все, что я могу найти, кажется очень рассеянным.
user833970
1
@ user833970 какие-нибудь конкретные вещи, на которые вы бы хотели указатели? Боюсь, что на самом деле нет всеобъемлющей ссылки на мета теорию зависимых типов. Это обсуждение (которое указывает здесь!) Может быть полезно: github.com/FStarLang/FStar/issues/360
cody
спасибо, сейчас я работаю над документом о парадоксе Берарди, думаю, это прояснит мою путаницу.
user833970
14

Даже если вы не заинтересованы в извлечении программ, тот факт, что Propэто непредсказуемо, позволяет вам создавать некоторые модели, которые вы не можете построить с использованием предикативной башни вселенных. У IIRC Торстена Альтенкирх есть модель Системы F, использующая непредсказуемость Кока.

Gallais
источник