OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Среда, 19 Июнь, 2019 18:30

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 47 ]  На страницу 1, 2, 3  След.
Автор Сообщение
 Заголовок сообщения: Гёдель и программирование
СообщениеДобавлено: Воскресенье, 02 Октябрь, 2011 20:12 

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


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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Воскресенье, 02 Октябрь, 2011 21:27 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9122
Откуда: Россия, Орёл
Теоремы Гёделя имеют очень конкретный, точный смысл, понятный математикам-теоретикам.
Не думаю, что стоит их так вольно трактовать.

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Воскресенье, 02 Октябрь, 2011 21:55 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8134
Откуда: Троицк, Москва
Илья Ермаков писал(а):
Нельзя построить формальную систему, которая проверит завершимость цикла.
Но человек легко это проверяет.
Илья Евгеньевич. Следите за.


Последний раз редактировалось Info21 Понедельник, 03 Октябрь, 2011 11:20, всего редактировалось 1 раз.

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Воскресенье, 02 Октябрь, 2011 22:10 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9122
Откуда: Россия, Орёл
В смысле?

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Воскресенье, 02 Октябрь, 2011 23:43 

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Понедельник, 03 Октябрь, 2011 01:30 

Зарегистрирован: Вторник, 29 Август, 2006 12:32
Сообщения: 2585
Откуда: Россия, Ярославль
Гугл отсылает к некоему Успенскому, который не столь строг в интерпретации теоремы, и даже применяет её к теории алгоритмов (насколько я успел понять).
А если уж даже он неправ, то Гёдель может дальше оставаться строгим - копирайты же на теоремы не распространяются? :D


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Понедельник, 03 Октябрь, 2011 07:18 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1194
Илья Ермаков писал(а):
нельзя создать формальную систему (алгоритм), которая даст ответ о произвольном цикле, завершим он или нет, но человек даёт такой ответ.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Понедельник, 03 Октябрь, 2011 07:45 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1194
Цитата:
...формулировка первой,или слабой теоремы Гёделя о неполноте: «Любая формальная система аксиом содержит неразрешенные предположения».


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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Понедельник, 03 Октябрь, 2011 07:46 

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Понедельник, 03 Октябрь, 2011 07:49 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9122
Откуда: Россия, Орёл
Trurl писал(а):
Илья Ермаков писал(а):
нельзя создать формальную систему (алгоритм), которая даст ответ о произвольном цикле, завершим он или нет, но человек даёт такой ответ.

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


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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Понедельник, 03 Октябрь, 2011 07:54 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9122
Откуда: Россия, Орёл
Иван Кузьмицкий писал(а):
Сравнения нету, потому что наверняка есть нужда в удобстве построения системы непротиворечивых утверждений, отсюда и любовь к "читабельности", краткой записи, динамической типизации и прочим ухищрениям.


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

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Понедельник, 03 Октябрь, 2011 08:31 

Зарегистрирован: Четверг, 17 Ноябрь, 2005 11:51
Сообщения: 2931
Откуда: г. Ярославль
Илья Ермаков писал(а):
...Короче, там принцип один "чо тут думать, прыгать надо, банан вот он".
Возможно, что создатель Питона нашёл быстрый и приматичный способ формулирования аксиом :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Вторник, 04 Октябрь, 2011 07:39 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1194
Илья Ермаков писал(а):
Драсте. А как мы доказываем, когда циклы пишем?

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Вторник, 04 Октябрь, 2011 09:52 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8134
Откуда: Троицк, Москва
Trurl писал(а):
Илья Ермаков писал(а):
Драсте. А как мы доказываем, когда циклы пишем?
А мы пишем такие циклы, про которые можем что-то доказать.
В каковом выборе как раз и заключена высокая роль человеческого интеллекта.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Вторник, 04 Октябрь, 2011 10:17 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9122
Откуда: Россия, Орёл
Ну, пусть будет дан какой-либо немыслимый цикл с break-ами - его можно постепенно распутать и преобразовать в эквивалентный, в котором уже либо найдётся ошибка, либо окажется, что он всё-таки правилен. Кажется, что можно?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Вторник, 04 Октябрь, 2011 12:32 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8134
Откуда: Троицк, Москва
Илья Ермаков писал(а):
Кажется, что можно?
Креститца, креститца и ишшо раз креститца!


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Вторник, 04 Октябрь, 2011 12:33 

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


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

Зарегистрирован: Пятница, 25 Ноябрь, 2005 18:55
Сообщения: 2272
Откуда: Россия, Нижний Новгород
Иван Кузьмицкий писал(а):
А вот теорема Гёделя ясно нам говорит — как бы ты не парился, проектируючи архитектуру, вылизываючи и рефакторя исходные тексты, твоя программная система никогда не будет идеальной.
Как бы ты ни парился над архитектурой своей программы, а так же над рефакторингом её исходных текстов, всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике.


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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Гёдель и программирование
СообщениеДобавлено: Вторник, 04 Октябрь, 2011 13:41 

Зарегистрирован: Четверг, 17 Ноябрь, 2005 11:51
Сообщения: 2931
Откуда: г. Ярославль
Сергей Губанов писал(а):
всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике
Вы имеете в виду отладку ПО "методом эксплуатации" :) ?


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

Зарегистрирован: Пятница, 25 Ноябрь, 2005 18:55
Сообщения: 2272
Откуда: Россия, Нижний Новгород
Илья Ермаков писал(а):
Ну, пусть будет дан какой-либо немыслимый цикл с break-ами - его можно постепенно распутать и преобразовать в эквивалентный
Изничтожение break-ов это и есть уход в более сильную теорию.

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

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


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 47 ]  На страницу 1, 2, 3  След.

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2019, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB