OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 29 Март, 2024 01:46

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




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

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


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

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Info21 писал(а):
Илья Ермаков писал(а):
Кажется, что можно?
Креститца, креститца и ишшо раз креститца!


Тогда поставлю вопрос по-другому.
Неужели правильно и аккуратно (WHILE по Дейкстре) составленный цикл можно проверять автоматически?

Я всегда думал, что даже если говорить только о "нормальных" циклах, то всё равно справедливо, что задача об их завершимости неразрешима алгоритмически, а человеком разрешима.
Собственно, изначально мой ответ Кузьмицкому был именно с этим подтекстом (что алгоритмически неразрешимая задача успешно разрешается человеком, допускает "человеческое" доказательство).


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

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1428
Превзойти машину через Геделя (или через Тьюринга) не выйдет. :)
Если машина не может, то и человеку не дано. Разве что, через откровение.


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

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1428
Илья Ермаков писал(а):
Ну, пусть будет дан какой-либо немыслимый цикл с break-ами - его можно постепенно распутать и преобразовать в эквивалентный, в котором уже либо найдётся ошибка, либо окажется, что он всё-таки правилен. Кажется, что можно?

Так пролема не в "правильности" цикла, а в его завершимости.
Умение давать заключение о завершимости любого цикла равносильно умению доказывать (или опровергать) любую формулу, даже недоказуемую.


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

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


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


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

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
Trurl писал(а):
Если машина не может, то и человеку не дано.
Либо я не понимаю чего-то, либо всё с точностью до наоборот.


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

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Вообще да - если машина не может, то берётся человек и необязательно алгоритмически находит решение. При этом приобретает новое знание, часть которого может передать машине.
Наверное, связано с тем, что любой алгоритмический исполнитель (а равно и его формальная модель) - это представление не всех возможностей сознания, а только их части.


Последний раз редактировалось Владислав Жаринов Вторник, 04 Октябрь, 2011 19:04, всего редактировалось 1 раз.

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

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Trurl писал(а):
...
Умение давать заключение о завершимости любого цикла равносильно умению доказывать (или опровергать) любую формулу, даже недоказуемую.
О связи истинности утверждения и его доказуемости (в смысле Гёделя) см. здесь 5-е размышление. На первый взгляд парадоксально, но потом...
Кстати, насчёт доказательства через предъявление для проверки тоже интересно...


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

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1428
Илья Ермаков писал(а):
А человеческий мозг? Можно ли уверенно говорить, что он не может быть мощнее, чем алгоритмическая машина?

Скорее всего не может. Но это не важно. Даже если кто-то постиг истину, хоть бы и сверхъестественным образом, как бы он убеждал других?
Например, я просветлился и понял, что Евклид был прав, а Лобачевский и пр. только путают людей. Но вот способа убедить других я не вижу. Разве что, основать Церковь Пятого Постулата.


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

Зарегистрирован: Вторник, 13 Сентябрь, 2011 07:32
Сообщения: 49
Сергей Губанов писал(а):
Иван Кузьмицкий писал(а):
Сергей Губанов писал(а):
всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике
Вы имеете в виду отладку ПО "методом эксплуатации" :) ?
Я имел ввиду, что формальная арифметика сама по себе, а программы - сами по себе. Для программ Гёдель ничего не доказывал.

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


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

Зарегистрирован: Вторник, 13 Сентябрь, 2011 07:32
Сообщения: 49
Драконограф писал(а):
Вообще да - если машина не может, то берётся человек и необязательно алгоритмически находит решение. При этом приобретает новое знание, часть которого может передать машине.
Наверное, связано с тем, что любой алгоритмический исполнитель (а равно и его формальная модель) - это представление не всех возможностей сознания, а только их части.

"необязательно алгоритмически" - это вопрос веры. Можно считать что мозг ищет решение каким-то тайным мистическим образом, а можно считать что в мозгу работает некий не до конца изученый алгоритм. А если исходить из модели нейронных сетей, то тогда можно считать что достаточно изученный алгоритм. Просто, как мне кажется, при неприменимости "быстрых" алгоритмов мозг запускает переборы с теми или инными эвристиками. За 100, 200 а то и 300 лет нескольким поколениям учёных сообществ удаётся совместными усилиями найти приемлемое решение.


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

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Элементарная задача: смоделируйте алгоритмически непрерывную систему, например, простую электрическую цепь с катушками индуктивности. У Вас это не получится - получится только приближение.
Точно такое же (даже гораздо меньшее) отношение имеют "нейронные сети" к нейронным сетям.
Так что не всё так просто. Об алгоритме работы непрерывной физической системы можно говорить только условно.


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

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Типа да, и я об этом... :) Природа (включая человеческую) непрерывна, а наше представление процессов в ней (конкретное, т.е. "численное") дискретно... как и процесс накопления этого знания (см. "отслаивание" у Леонтьева). Вот если натурно смоделировать... те же катушки - катушками, а нейроны - нейронными аналоговыми схемами... м.б. приближение будет точнее... :)


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

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1428
Драконограф писал(а):
Природа (включая человеческую) непрерывна


А про атомы и т.п. разве в школе не рассказывают?


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

Зарегистрирован: Вторник, 13 Сентябрь, 2011 07:32
Сообщения: 49
Естественно что условно. А о чём можно говорить неусловно? Все расчёты реальных физических систем выполняются приближённо. Но мы же используем простые электрические цепи с ёмкостями и транзисторами для выполнения алгоритмов, пишем программы для них, даже жизни свои доверяем этим системам. Время от времени модели и реальные процессы перестают соответствовать друг другу и тогда начинается поиск новых, более адекватных моделей. Что тут таинственного? Я ничего мистического здесь не вижу. Если есть какие-то конкретные примеры мне будет очень интересно о них узнать.


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

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


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

Тезис Тьюринга-Чёрча-Маркова... говорит о том, что никакая алгоритмическая "штука" не может быть "мощнее", чем МТ, лямбда-исчисление, нормальные алгорифмы, машина Минского, алгоритмы Колмогорова.... и т.д. И этот тезис - гипотеза, которая подкреплена только тем, что каждая из предложенных алгоритмических абстракций оказывалась эквивалентной остальным. Доказательна здесь только эквивалентность. Плюс есть эмпирическая уверенность, что вряд ли можно придумать нечто, что будет мощнее, раз всё оно эквивалентно... Но напомню, что речь идёт именно про АЛГОРИТМИЧЕСКИЕ "штуки". При этом нет определения, что это такое. Только множество разных абстракций и возможность всегда придумать ещё одну, и опыт, подсказывающий, что для неё потом докажется эквивалентность.
Но нет вообще никаких оснований для сравнения их с возможностями физических систем в целом. Такой вопрос в теории алгоритмов даже и поставлен быть не может, потому что это теория формальная, а не естественнонаучная.
Насколько я знаю этот вопрос.


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

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

Скорее всего не может. Но это не важно. Даже если кто-то постиг истину, хоть бы и сверхъестественным образом, как бы он убеждал других?
Например, я просветлился и понял, что Евклид был прав, а Лобачевский и пр. только путают людей. Но вот способа убедить других я не вижу. Разве что, основать Церковь Пятого Постулата.
В точку.

Каким бы ни был отдельный человеческий мозг, он должен произвести убедительный аргумент, являющийся конечной строкой литер.
Вот в этом вся и штука.
Гедель как раз про конечные строки литер.


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

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Trurl писал(а):
Драконограф писал(а):
Природа (включая человеческую) непрерывна
А про атомы и т.п. разве в школе не рассказывают?
Природа процессов, конечно же... неточно выразился... :) Но насчёт того, что потом всё равно выводить отчуждаемую часть как конечные строки литер - это да.


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

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


Конечно, но ещё можно убедить по-другому: указать способ опытной проверки, который доступен другим.
Тогда доказательство будет всё-таки прошито не в самой строке литер, а где-то в объективной реальности. Мы же просто отсылаем к ней за проверкой.

Тот же Принцип Калашникова какой-нибудь: надёжней всего отправить за доказательством проверять на собственной ж... тех, кто сомневается :)


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

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Илья Ермаков писал(а):
Info21 писал(а):
Каким бы ни был отдельный человеческий мозг, он должен произвести убедительный аргумент, являющийся конечной строкой литер.
Конечно, но ещё можно убедить по-другому: указать способ опытной проверки, который доступен другим.
Ну, это будет конечный набор телодвижений.
Описываемый конечным набором литер.

Илья Евгеньевич, не надо мистики. КонкретнЕе.


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

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


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

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


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

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