Что является эквивалентом ошибки изоморфизма Карри-Ховарда?
Проще говоря, соответствие Карри-Говарда утверждает, что тип является теоремой и что программа, возвращающая этот тип, является доказательством соответствующей теоремы.
Соответствие основано на формализации математических доказательств в таких языках, как исчисление предикатов, ограниченных интуиционистской логикой. Но когда математические доказательства написаны на этих официальных языках, их ошибки могут быть обнаружены компьютерами. Например, Mizar - это математический язык относительно высокого уровня, плюс компилятор, который проверяет написанные на нем доказательства.
Поэтому Curry-Howard связывает программы с математическими доказательствами без ошибок. Следовательно, как Карри-Ховард переводит концепцию программной ошибки в математический мир? По вышесказанному, это не логическая ошибка в доказательстве.
1 ответ
Программы с ошибками соответствуют корректным доказательствам, которые отличаются от доказательств, которым программы соответствовали бы без ошибок. Другими словами, программы с ошибками соответствуют корректным доказательствам, но разным доказательствам. По аналогии, путь - это особая последовательность шагов, которые вы совершаете перед входом. Вы можете намереваться пройти путь до продуктового магазина. Возможно, вы ошиблись и оказались в парикмахерской. Ты все еще прошел путь, но не тот, который хотел.
Логические ошибки в доказательствах больше похожи на ошибки времени выполнения или синтаксические ошибки в языке программирования. В таких случаях дело не в том, что вы вычислили, доказали или пошли не так; но что вы не смогли ничего вычислить, доказать или пройтись вообще. В нашей аналогии это может быть похоже на забвение ходьбы и попытку сделать несколько шагов, используя только левый локоть и подбородок. Вы не сможете завершить свой путь - любой путь, правильный или неправильный - потому что вы пытаетесь сделать что-то, что не считается шагом.
Интересная задача, которую вы могли бы рассмотреть - написать правильный, действительный алгоритм, который не подходит для любой возможной проблемы.
К сожалению, я не думаю, что Patrick87 полностью прав. Важно понимать, что подразумевается под "ошибкой" в вопросе. Я предполагаю, что "ошибки" включают ошибки, влияющие на типы, и ошибки, которые не влияют.
Важно отметить, что при соответствии теоремы относятся только к характеристикам типа программы, а не к характеристикам значений. Так программные заявления, такие как x := x + 1 а также x := x + 2 полностью эквивалентны с точки зрения теоремы. Важно понимать, что в обычной интерпретации это просто абстрактные теоремы, а не теоремы о программе (например, о ее корректности).
Отсюда легко увидеть, что многие (может быть, большинство) ошибок вообще не влияют на соответствующие теоремы. Например, если у нас есть финансовая программа, и мы хотим рассчитать чистую прибыль от валовой прибыли, было бы правильно написать NetProfit := GrossProfit * 0.8, Но мы могли бы ввести ошибку и рассчитать налог вместо NetProfit := GrossProfit * 0.2, Он не влияет на типы, поэтому не влияет на соответствие. Многие, многие настоящие ошибки похожи на это: отдельные ошибки, ошибки переполнения, неправильное понимание поведения подпрограммы, числовые и строковые опечатки...
Для ошибок, которые влияют на соответствие, это зависит от того, приводят ли они к действительной теореме или нет. Если это приводит к правильной теореме, более вероятно, что ваша программа будет скомпилирована, запущена без сбоев и т. Д. Однако это означает, что вы ошиблись в одном из типов, например, если вы хотите соединить 2 числа вместе, например 1 и 3 -> 13. Но вы забыли преобразовать их в строки, поэтому вместо них вы получите 1 и 3 -> 4. С другой стороны, если это не приводит к правильной теореме, то это означает, что вы, вероятно, что-то серьезно ошиблись, и программа не скомпилируется, или она застрянет в бесконечном цикле, или что-то в этом роде.
Подводя итог, если у вас есть программа с соответствующей теоремой, которая является действительной, это не говорит вам много. В программе все еще могут быть ошибки. С другой стороны, если вы пытаетесь создать программу, у которой нет соответствующей теоремы, то это хороший признак того, что вы, вероятно, ошибаетесь. Так что это зависит от вида ошибки, большинство из них вообще не появляются.