Добавление аксиом к COQ часто делает доказательства проще, но также вводит некоторые побочные эффекты. Например, при использовании аксиомы классическая выходит из интуиционистского царства, и доказательства больше не могут быть вычислены. Мой вопрос в том, что является недостатком использования функциональной расширяемости axiom?Что является недостатком использования функциональной расширяемости в COQ
Для меня недостатки использования функциональной расширяемости более или менее одинаковы с использованием любой другой аксиомы в Coq: она увеличивает сложность системы и насколько нам нужно доверять. Хотя теоретически мы хорошо понимаем логические последствия работы с этими известными аксиомами (например, какие комбинации аксиом следует избегать для обеспечения согласованности), на практике нас иногда застигают врасплох. Например, было recently found out, что аксиома высказывания была несовместима с теорией Кока в версии 8.4, хотя считалось, что она считается последовательной. Это, казалось бы, естественная аксиома, просто говорит, что эквивалентные предложения равны, и принимаются во многих разработках Coq:
Axiom propositional_extensionality :
forall P Q : Prop, (P <-> Q) -> P = Q.
В ответе linked above, Андрей Бауэр говорит о том, что эта хрупкость может быть связана с этими аксиомами не имеющие правило вычислений, связанное с их, вопреки остальной теории Кока.
Помимо этого общего замечания, я слышал, что люди говорят, что функциональная расширяемость по умолчанию может быть нежелательной, поскольку она приравнивает функции с очень разными компьютерными поведением об этих различиях. Я лично не покупаю этот аргумент, так как Coq уже приравнивает множество значений , которые вычисляются совсем по-другому, например 0 и 47^1729 - 47 mod 1729. Я не знаю других причин, по которым я не хочу предполагать функциональную расширяемость.
Я думаю, что ваше сравнение в последнем абзаце немного испорчено. Вы можете упростить формулу мод до нуля, но вы не можете упростить сортировку пузырьков и быстрый сортировку по каноническому алгоритму сортировки. Кроме того, формулу мод можно предварительно вычислить, но функция по бесконечному индуктивному типу всегда должна быть рассчитана по требованию. – Cryptostasis
Я согласен с Артуром в том, что аксиома функциональной актуализации безвредна, и есть несколько убедительных аргументов, чтобы отвергнуть ее. Его «провал» в Coq можно рассматривать как ограничение синтаксических методов больше, чем любая другая более глубокая причина. Лично я стараюсь избегать аксиом, поэтому, если возможно, я представляю функции в виде канонически отсортированных таблиц всякий раз, когда требуется расширение. – ejgallego
Просто прочитал Адам Члипала, что даже простое равенство: «Теорема two_funs: (fun n => n) = (fun n => n + 0)' не доказуема в COQ без аксиом функциональной актуализации. Это создает у меня впечатление, что без этой аксиомы не будет далеко. – Cryptostasis
Аналогичный [вопрос] (http://mathoverflow.net/questions/156238/function-extensionality-does-it-make-a-difference-why-would-one-keep-it-out-of) - см. часть 2 и [принятый ответ] (http://mathoverflow.net/a/156295). –