OberonCore
https://forum.oberoncore.ru/

Гёдель и программирование
https://forum.oberoncore.ru/viewtopic.php?f=27&t=3582
Страница 1 из 3

Автор:  Иван Кузьмицкий [ Воскресенье, 02 Октябрь, 2011 20:12 ]
Заголовок сообщения:  Гёдель и программирование

Попалась в руки ссылка: http://elementy.ru/trefil/21142
Цитата:
...формулировка первой,или слабой теоремы Гёделя о неполноте: «Любая формальная система аксиом содержит неразрешенные предположения». Но на этом Гёдель не остановился, сформулировав и доказав вторую, или сильную теорему Гёделя о неполноте: «Логическая полнота (или неполнота) любой системы аксиом не может быть доказана в рамках этой системы. Для ее доказательства или опровержения требуются дополнительные аксиомы (усиление системы)».


Если перенести это на программирование, то можно ли сказать — разработчик софта занимается формированием системы аксиом, выраженной в исходных текстах программ? Мне кажется, это очевидно.

А вот теорема Гёделя ясно нам говорит — как бы ты не парился, проектируючи архитектуру, вылизываючи и рефакторя исходные тексты, твоя программная система никогда не будет идеальной. И в силу обязательного наличия неразрешённых предположений, где-то обязательно вылезут огрехи, потребующие всяческих вмешательств в виде, например, отладки.

Такое умозрение наводит на мысль, что пресловутая "читабельность" кода, всяческие утиные типизации и прочие пейтоны с хаскеллями суть жалкие попытки усилить ся немощного, дабы достичь недостижимого — а именно, полностью доказанной системы аксиом.

Автор:  Илья Ермаков [ Воскресенье, 02 Октябрь, 2011 21:27 ]
Заголовок сообщения:  Re: Гёдель и программирование

Теоремы Гёделя имеют очень конкретный, точный смысл, понятный математикам-теоретикам.
Не думаю, что стоит их так вольно трактовать.

Понятно, что возможности формализации и формального доказательства имеют ограничения.
Но проверка правильности - это не чисто формальный процесс.
Нельзя построить формальную систему, которая проверит завершимость цикла.
Но человек легко это проверяет.

Да и как-то сравнение пейтонов с хаскелями очень странное. При чём тут хаскель и утиная типизация? Утиная типизация и какая-либо доказательность (доказательность - это обязательно какое-нибудь статическое средство, а утиная типизация - принципиальный отказ от статики)?

Автор:  Info21 [ Воскресенье, 02 Октябрь, 2011 21:55 ]
Заголовок сообщения:  Re: Гёдель и программирование

Илья Ермаков писал(а):
Нельзя построить формальную систему, которая проверит завершимость цикла.
Но человек легко это проверяет.
Илья Евгеньевич. Следите за.

Автор:  Илья Ермаков [ Воскресенье, 02 Октябрь, 2011 22:10 ]
Заголовок сообщения:  Re: Гёдель и программирование

В смысле?

Можно перефразировать:
нельзя создать формальную систему (алгоритм), которая даст ответ о произвольном цикле, завершим он или нет, но человек даёт такой ответ.

Автор:  Валерий Лаптев [ Воскресенье, 02 Октябрь, 2011 23:43 ]
Заголовок сообщения:  Re: Гёдель и программирование

Мне кажется, что теоремы о неполноте играют рояль в контексте доказательства правильности. Можно доказать правильность программы, но!... Это не означает, что правильная программа СООТВЕТСТВУЕТ техническому заданию (требуются дополнительные аксиомы... :) )

Автор:  Пётр Кушнир [ Понедельник, 03 Октябрь, 2011 01:30 ]
Заголовок сообщения:  Re: Гёдель и программирование

Гугл отсылает к некоему Успенскому, который не столь строг в интерпретации теоремы, и даже применяет её к теории алгоритмов (насколько я успел понять).
А если уж даже он неправ, то Гёдель может дальше оставаться строгим - копирайты же на теоремы не распространяются? :D

Автор:  Trurl [ Понедельник, 03 Октябрь, 2011 07:18 ]
Заголовок сообщения:  Re: Гёдель и программирование

Илья Ермаков писал(а):
нельзя создать формальную систему (алгоритм), которая даст ответ о произвольном цикле, завершим он или нет, но человек даёт такой ответ.

Ну, разве что: "мамой клянусь, завершим".

Автор:  Trurl [ Понедельник, 03 Октябрь, 2011 07:45 ]
Заголовок сообщения:  Re: Гёдель и программирование

Цитата:
...формулировка первой,или слабой теоремы Гёделя о неполноте: «Любая формальная система аксиом содержит неразрешенные предположения».


Имеем случай так называемого вранья.

Автор:  Иван Кузьмицкий [ Понедельник, 03 Октябрь, 2011 07:46 ]
Заголовок сообщения:  Re: Гёдель и программирование

Илья Ермаков писал(а):
Да и как-то сравнение пейтонов с хаскелями очень странное. При чём тут хаскель и утиная типизация? Утиная типизация и какая-либо доказательность (доказательность - это обязательно какое-нибудь статическое средство, а утиная типизация - принципиальный отказ от статики)?
Сравнения нету, потому что наверняка есть нужда в удобстве построения системы непротиворечивых утверждений, отсюда и любовь к "читабельности", краткой записи, динамической типизации и прочим ухищрениям. Мне кажется, что теоремы Гёделя имеют гораздо более глубокий (широкий) смысл, чем кажется многим математикам. И так кажется не только мне: http://awas1952.livejournal.com/824361.html

Автор:  Илья Ермаков [ Понедельник, 03 Октябрь, 2011 07:49 ]
Заголовок сообщения:  Re: Гёдель и программирование

Trurl писал(а):
Илья Ермаков писал(а):
нельзя создать формальную систему (алгоритм), которая даст ответ о произвольном цикле, завершим он или нет, но человек даёт такой ответ.

Ну, разве что: "мамой клянусь, завершим".


Драсте. А как мы доказываем, когда циклы пишем? Что вектор переменных сойдётся к условию цикла.
Понятное дело, что если цикл запутанный, то это трудно, но можно и "распутать" - и показать, что либо он правилен, либо нет.

Автор:  Илья Ермаков [ Понедельник, 03 Октябрь, 2011 07:54 ]
Заголовок сообщения:  Re: Гёдель и программирование

Иван Кузьмицкий писал(а):
Сравнения нету, потому что наверняка есть нужда в удобстве построения системы непротиворечивых утверждений, отсюда и любовь к "читабельности", краткой записи, динамической типизации и прочим ухищрениям.


Ну, Иван, Вы бы эта... не переоценивали. Любовь к выпендрёжу, лень, презрение к дисциплине у них - и причём тут Гёдель? :)
Автор Питона писал:
Цитата:
Я бы назвал прагматизм. Если вы чрезмерно озабочены такими теоретическими понятиями, как скрытие данных, контроль доступа, абстракции или спецификации, то не станете настоящим Python-программистом и будете напрасно терять время на борьбу с языком вместо того, чтобы пользоваться им
(получая удовольствие); кроме того, в этом случае ваше применение языка, скорее всего, окажется неэффективным. Python подойдёт вам, если вы любите немедленно получать вознаграждение, как я сам.

Короче, там принцип один "чо тут думать, прыгать надо, банан вот он".

Цитата:
Мне кажется, что теоремы Гёделя имеют гораздо более глубокий (широкий) смысл, чем кажется многим математикам. И так кажется не только мне: http://awas1952.livejournal.com/824361.html

[/quote]
Дык я не спорю. Только расширять смыслы нужно осторожно...

Автор:  Иван Кузьмицкий [ Понедельник, 03 Октябрь, 2011 08:31 ]
Заголовок сообщения:  Re: Гёдель и программирование

Илья Ермаков писал(а):
...Короче, там принцип один "чо тут думать, прыгать надо, банан вот он".
Возможно, что создатель Питона нашёл быстрый и приматичный способ формулирования аксиом :)

Автор:  Trurl [ Вторник, 04 Октябрь, 2011 07:39 ]
Заголовок сообщения:  Re: Гёдель и программирование

Илья Ермаков писал(а):
Драсте. А как мы доказываем, когда циклы пишем?

А мы пишем такие циклы, про которые можем что-то доказать.

Автор:  Info21 [ Вторник, 04 Октябрь, 2011 09:52 ]
Заголовок сообщения:  Re: Гёдель и программирование

Trurl писал(а):
Илья Ермаков писал(а):
Драсте. А как мы доказываем, когда циклы пишем?
А мы пишем такие циклы, про которые можем что-то доказать.
В каковом выборе как раз и заключена высокая роль человеческого интеллекта.

Автор:  Илья Ермаков [ Вторник, 04 Октябрь, 2011 10:17 ]
Заголовок сообщения:  Re: Гёдель и программирование

Ну, пусть будет дан какой-либо немыслимый цикл с break-ами - его можно постепенно распутать и преобразовать в эквивалентный, в котором уже либо найдётся ошибка, либо окажется, что он всё-таки правилен. Кажется, что можно?

Автор:  Info21 [ Вторник, 04 Октябрь, 2011 12:32 ]
Заголовок сообщения:  Re: Гёдель и программирование

Илья Ермаков писал(а):
Кажется, что можно?
Креститца, креститца и ишшо раз креститца!

Автор:  Владислав Жаринов [ Вторник, 04 Октябрь, 2011 12:33 ]
Заголовок сообщения:  Re: Гёдель и программирование

Пётр Кушнир писал(а):
Гугл отсылает к некоему Успенскому, который не столь строг в интерпретации теоремы, и даже применяет её к теории алгоритмов (насколько я успел понять).
А если уж даже он неправ, то Гёдель может дальше оставаться строгим - копирайты же на теоремы не распространяются? :D
Некий Успенский - это вот этот. :) Правда, про Гёделя в основном в самой "Апологии математики" (статье).
Валерий Лаптев в viewtopic.php?p=65963#p65963 писал(а):
Мне кажется, что теоремы о неполноте играют рояль в контексте доказательства правильности. Можно доказать правильность программы, но!... Это не означает, что правильная программа СООТВЕТСТВУЕТ техническому заданию (требуются дополнительные аксиомы... )
Вы имеете в виду, что если мы формализовали ТЗ, скажем, для проверки моделей - то это только при некоторых ограничениях (текстуально конечные типы)?
Ежели эти ограничения выполняются и в моделируемой системе (данные-код-аппаратура), то формальная верификация, видимо, заменяет отладку. Но требует формулировать все требования к системе. Что, вероятно, не всегда возможно сразу. :) Кстати, здесь многое связано не с Гёделем, а с алгоритмической разрешимостью (в частности, насчёт завершения цикла - и вообще алгоритма на конкретных исхданных). Хотя эти вещи, возможно, глубинно пересекаются как-то...
У Фридланда, кстати, интересный обзор - там, где про формализацию и алгоритмизацию. О том, что информатическое решение (представляемое через алгоритм) не всегда возможно при исходной постановке задачи, тоже... :)

Автор:  Сергей Губанов [ Вторник, 04 Октябрь, 2011 13:31 ]
Заголовок сообщения:  Re: Гёдель и программирование

Иван Кузьмицкий писал(а):
А вот теорема Гёделя ясно нам говорит — как бы ты не парился, проектируючи архитектуру, вылизываючи и рефакторя исходные тексты, твоя программная система никогда не будет идеальной.
Как бы ты ни парился над архитектурой своей программы, а так же над рефакторингом её исходных текстов, всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике.


http://ru.wikipedia.org/wiki/Теорема_Гёделя_о_неполноте
Цитата:
...непротиворечивость формальной арифметики не может быть доказана средствами этой теории. Однако существуют доказательства непротиворечивости формальной арифметики, использующие средства, невыразимые в ней.

Автор:  Иван Кузьмицкий [ Вторник, 04 Октябрь, 2011 13:41 ]
Заголовок сообщения:  Re: Гёдель и программирование

Сергей Губанов писал(а):
всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике
Вы имеете в виду отладку ПО "методом эксплуатации" :) ?

Автор:  Сергей Губанов [ Вторник, 04 Октябрь, 2011 14:07 ]
Заголовок сообщения:  Re: Гёдель и программирование

Илья Ермаков писал(а):
Ну, пусть будет дан какой-либо немыслимый цикл с break-ами - его можно постепенно распутать и преобразовать в эквивалентный
Изничтожение break-ов это и есть уход в более сильную теорию.

Непротиворечивость какого-то конкретного цикла с break-ами будет доказана не в рамках теории "циклов с break-ами", а (прямо как Гёдель прописал) в рамках более сильной теории каких-нибудь там дейкстровских циклов.

Что касается самой "теории дейкстровских циклов", то она, видимо, в гёделевском смысле не полна.

Страница 1 из 3 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/