Re: Несколько вопросов вразброс
On Tue, Jul 03, 2012 at 06:41:49PM +0400, "Артём Н." wrote:
> > Вообще, есть такая теорема Гёделя о неполноте, согласно которой в любой
> > формальной системе, сводимой в определённом смысле к арифметике,
> > существуют недоказуемые утверждения.
> Которая, думаю, сюда не очень подходит: есть набор правил, которые должны
> выполняться для доказательства непротиворечивости.
> Т.е., имеются некоторые утверждения от которых возможно отталкиваться.
> К Гёделю и проблемам Гильберта это отношения не имеет. К счастью. :-D
Связь между "проблемой останова" в теории алгоритмов (из которой
вытекает отсутствие общей процедуры доказательства правильности
программ) и теоремой Гёделя, тем не менее прямая. Обитающие здесь
математики могут подтвердить.
> К тому же, в данном частном случае, система, как правило, дискретна.
> И, в теории, возможно перечислить все её состояния, подав на вход все комбинации
> "нулей и единиц" (даже, если система с памятью).
Если система обладает неограниченной памятью, как машина Тьюринга с бесконечной
лентой, то в общем случае нельзя. На практике нельзя уже при сколько-нибудь
значительном объёме памяти, просто в силу потребного времени.
> > Т.е., общей процедуры доказательства правильности программ в принципе не
> > существует. Однако, это не означает, что в частных случаях такое
> > доказательство провести нельзя.
> Вопрос -то там был изначально в другом.
> А. Чуприна написал, что:
> "В данном случае компиляция выполняется вместо тестов. Тесты, в отличие от
> доказательства корректности, не являются гарантией надежности."
Верное утверждение.
> Т.е., подразумевал, что в этом случае возможен отказ от тестов.
На самом деле, он просто утверждает, что тестирование на примерах (т.е.,
твоё "перечисление всех состояний, подав на вход все комбинации нулей и
единиц") ничего не гарантирует. Можно 1000 раз успешно прогнать *все*
комбинации входных переменных некой процедуры, а на 1001-м получить
ошибку, например, из-за утечки памяти, или из-за переполнения какой-нибудь
переменной-счётчика, которая не обнуляется между вызовами, и т.п.
> Мне кажется это сомнительным.
> По причине того, что полное доказательство, в принципе, провести невозможно (в
> зависимости от уровня сложности, конечно).
Похоже, что ты сам запутался в своих рассуждениях: тебя *принципиальная*
доказуемость интересует, или всё же доказуемость в частных случаях? С
первым всё ясно, а про второе тебе уже писали, что доказывать во многих
случаях можно, для этого есть методы, и методы эти не основаны на
переборе всех нулей и единиц.
> > Например, существуют языки программирования, которые вычисляют через
> > доказательство (через формальную процедуру вывода). PROLOG, например.
> > На таких языках можно писать программы, которые сами же являются
> > доказательствами своей правильности.
> Да, кстати, Пролог я не понимаю. :-(
> Изначально - всё просто. Затем, правила становятся какие-то дикие (к тому месту,
> где начинается рекурсия и прочее). Хотя, может, в книжке было плохо описано.
> Но почему программа является априори правильной?
Я такого не утверждал. Что я утверждал, отквочено выше.
> Ведь она там - просто набор отношений, а "Пролог" - система вывода.
> Кто сказал, что данный набор отношений будет давать верный с точки зрения
> условий задачи результат на любом подмножестве входных данных?
Никто не сказал, однако:
Чем ближе язык программирования по синтаксису и семантике к формальному
описанию задачи, тем проще на нем написать верную программу. В случае
пролога, текст программы просто перефразирует исходное условие на языке
логики предикатов. Т.е., программа получается автоматически верной, если
условие задачи было успешно выражено на языке формальной логики и затем
записано в синтаксисе пролога. По сути, это всё, что требуется. Меньше
уже нельзя, без наделения машины интеллектом и знаниями о внешнем мире.
В прологе есть ещё одна особенность: предикаты пролога работают "туда и
обратно". Например, имея предикат p(X), пролог может построить набор
значений X, при которых этот p(X) истинен. Используя это свойство можно
строить доказательства правильности, не выходя за рамки самого языка.
Например, если есть альтернативная реализация q(X), то проверка на
эквивалентность между p и q в прологе тривиальна.
В качестве ложки дёгтя замечу, что хотя, например, арифметику на прологе
можно реализовать прямо через аксиомы Пеано, так никто, ессно, не делает,
а вместо этого используются "is" и прочие встроенные примитивы. Ну а
поскольку в прологе нет типизации, то все это может закончиться теми
же ошибками, что и в любом другом языке...
> И на практике: будь всё так хорошо, как вы пишите, все бы уже давно писали на
> Прологе (по крайней мере, знали бы что это такое). :-)
Незнание, как говорится, не освобождает от ответственности. Плюс, в
идеальном мире все бы уже давно писали хотя бы на том же Haskell...
--
Stanislav
Reply to: