Я имею в виду вопрос здесь: мощные алгоритмы слишком сложны для реализации .
Если алгоритм является мощным, но слишком сложным для реализации, как вы можете быть уверены, что алгоритм правильный? Без реализации вы не сможете протестировать алгоритм в реальном сценарии, и такой сложный алгоритм может содержать ошибки, которые могут сделать алгоритм недействительным.
Это то, что я не понимаю; если у вас есть методы, чтобы доказать правильность алгоритма, то у вас уже есть алгоритм для его реализации, не так ли? Или как мы можем быть уверены, что техника доказывания верна?
Извините, если я звучу элементарно!
Обновление от Kaveh (воспроизведено здесь, потому что аргумент лучше!):
Если вы можете формально доказать правильность алгоритма в формальной системе, такой как Coq, то вы также можете извлечь алгоритм (потому что по сути вы реализовали алгоритм), но ключевой факт заключается в том, что для большинства алгоритмов мы не даем формальных доказательств Для корректности алгоритма мы используем неформальные доказательства правильности. Доказательства могут быть ложными, что случается время от времени, и даже формальное доказательство правильности не сделает нас абсолютно уверенными в правильности алгоритма.
источник
Ответы:
Несколько лет назад были (довольно резкие) дебаты на тему, подобную этой. Все началось, когда несколько сложных доказательств оказались неверными, и некоторые исследователи начали сомневаться в самой природе доказательств (ну, я должен был сказать «доказуемую криптографию», но ради общности я этого не сделал) , Обе стороны спора обвинили другую в неправильном понимании концепций. Вот ссылка для получения дополнительной информации .
Доказательства - это наши (математические) инструменты для доказательства правильности теорем / алгоритмов, но когда они стали слишком сложными, мы можем ошибиться и доказать, что они не правы. Недавно 100-или-около-страницы , на доказательство P ≠ NP является отличным примером. Однако это не исключает самой природы доказательств: с ними все в порядке.
И последний момент: я думаю, что изучение философии науки даст нам больше понимания этого. (По данной ссылке см. Маркер " Как мы узнаем, правильное ли математическое доказательство? ")
источник