Иван Кузьмицкий писал(а):
Сергей Губанов писал(а):
всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике
Вы имеете в виду отладку ПО "методом эксплуатации" 
?| OberonCore https://forum.oberoncore.ru/ |
|
| Гёдель и программирование https://forum.oberoncore.ru/viewtopic.php?f=27&t=3582 |
Страница 2 из 3 |
| Автор: | Сергей Губанов [ Вторник, 04 Октябрь, 2011 14:17 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Иван Кузьмицкий писал(а): Сергей Губанов писал(а): всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике Вы имеете в виду отладку ПО "методом эксплуатации" ? |
|
| Автор: | Илья Ермаков [ Вторник, 04 Октябрь, 2011 15:35 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Info21 писал(а): Илья Ермаков писал(а): Кажется, что можно? Креститца, креститца и ишшо раз креститца!Тогда поставлю вопрос по-другому. Неужели правильно и аккуратно (WHILE по Дейкстре) составленный цикл можно проверять автоматически? Я всегда думал, что даже если говорить только о "нормальных" циклах, то всё равно справедливо, что задача об их завершимости неразрешима алгоритмически, а человеком разрешима. Собственно, изначально мой ответ Кузьмицкому был именно с этим подтекстом (что алгоритмически неразрешимая задача успешно разрешается человеком, допускает "человеческое" доказательство). |
|
| Автор: | Trurl [ Вторник, 04 Октябрь, 2011 16:05 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Превзойти машину через Геделя (или через Тьюринга) не выйдет. Если машина не может, то и человеку не дано. Разве что, через откровение. |
|
| Автор: | Trurl [ Вторник, 04 Октябрь, 2011 16:10 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Илья Ермаков писал(а): Ну, пусть будет дан какой-либо немыслимый цикл с break-ами - его можно постепенно распутать и преобразовать в эквивалентный, в котором уже либо найдётся ошибка, либо окажется, что он всё-таки правилен. Кажется, что можно? Так пролема не в "правильности" цикла, а в его завершимости. Умение давать заключение о завершимости любого цикла равносильно умению доказывать (или опровергать) любую формулу, даже недоказуемую. |
|
| Автор: | Илья Ермаков [ Вторник, 04 Октябрь, 2011 17:13 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Trurl писал(а): Превзойти машину через Геделя (или через Тьюринга) не выйдет. Если машина не может, то и человеку не дано. Разве что, через откровение. Тьюринг или Гёдель говорят ведь о дискретных способах решения. Алгоритм - это конечное дискретное решение. Любое доказательство - тоже дискретное. А человеческий мозг? Можно ли уверенно говорить, что он не может быть мощнее, чем алгоритмическая машина? |
|
| Автор: | Valery Solovey [ Вторник, 04 Октябрь, 2011 18:13 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Trurl писал(а): Если машина не может, то и человеку не дано. Либо я не понимаю чего-то, либо всё с точностью до наоборот.
|
|
| Автор: | Владислав Жаринов [ Вторник, 04 Октябрь, 2011 18:58 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Вообще да - если машина не может, то берётся человек и необязательно алгоритмически находит решение. При этом приобретает новое знание, часть которого может передать машине. Наверное, связано с тем, что любой алгоритмический исполнитель (а равно и его формальная модель) - это представление не всех возможностей сознания, а только их части. |
|
| Автор: | Владислав Жаринов [ Вторник, 04 Октябрь, 2011 19:00 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Trurl писал(а): ... О связи истинности утверждения и его доказуемости (в смысле Гёделя) см. здесь 5-е размышление. На первый взгляд парадоксально, но потом...Умение давать заключение о завершимости любого цикла равносильно умению доказывать (или опровергать) любую формулу, даже недоказуемую. Кстати, насчёт доказательства через предъявление для проверки тоже интересно... |
|
| Автор: | Trurl [ Вторник, 04 Октябрь, 2011 22:23 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Илья Ермаков писал(а): А человеческий мозг? Можно ли уверенно говорить, что он не может быть мощнее, чем алгоритмическая машина? Скорее всего не может. Но это не важно. Даже если кто-то постиг истину, хоть бы и сверхъестественным образом, как бы он убеждал других? Например, я просветлился и понял, что Евклид был прав, а Лобачевский и пр. только путают людей. Но вот способа убедить других я не вижу. Разве что, основать Церковь Пятого Постулата. |
|
| Автор: | Дмитрий Маслов [ Среда, 05 Октябрь, 2011 07:33 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Сергей Губанов писал(а): Иван Кузьмицкий писал(а): Сергей Губанов писал(а): всё равно для доказательства непротиворечивости формальной арифметики придётся использовать средства невыразимые в формальной арифметике Вы имеете в виду отладку ПО "методом эксплуатации" ?Я, может, не понял о чём речь, но не совсем понятно как это: "арифметика сама по себе, а программы - сами по себе"? А что в процессоре есть кроме формальной арифметики? Другое дело и это важно, когда речь идёт о непротиворечивости арифметики имеется ввиду непротиворечивость самой арифметики, её аксиом и систем аксиом содержащих аксиоматику арифметики, а вовсе не возможных доказательств в рамках самой арифметики. |
|
| Автор: | Дмитрий Маслов [ Среда, 05 Октябрь, 2011 07:46 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Драконограф писал(а): Вообще да - если машина не может, то берётся человек и необязательно алгоритмически находит решение. При этом приобретает новое знание, часть которого может передать машине. Наверное, связано с тем, что любой алгоритмический исполнитель (а равно и его формальная модель) - это представление не всех возможностей сознания, а только их части. "необязательно алгоритмически" - это вопрос веры. Можно считать что мозг ищет решение каким-то тайным мистическим образом, а можно считать что в мозгу работает некий не до конца изученый алгоритм. А если исходить из модели нейронных сетей, то тогда можно считать что достаточно изученный алгоритм. Просто, как мне кажется, при неприменимости "быстрых" алгоритмов мозг запускает переборы с теми или инными эвристиками. За 100, 200 а то и 300 лет нескольким поколениям учёных сообществ удаётся совместными усилиями найти приемлемое решение. |
|
| Автор: | Илья Ермаков [ Среда, 05 Октябрь, 2011 07:55 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Элементарная задача: смоделируйте алгоритмически непрерывную систему, например, простую электрическую цепь с катушками индуктивности. У Вас это не получится - получится только приближение. Точно такое же (даже гораздо меньшее) отношение имеют "нейронные сети" к нейронным сетям. Так что не всё так просто. Об алгоритме работы непрерывной физической системы можно говорить только условно. |
|
| Автор: | Владислав Жаринов [ Среда, 05 Октябрь, 2011 11:10 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Типа да, и я об этом... Природа (включая человеческую) непрерывна, а наше представление процессов в ней (конкретное, т.е. "численное") дискретно... как и процесс накопления этого знания (см. "отслаивание" у Леонтьева). Вот если натурно смоделировать... те же катушки - катушками, а нейроны - нейронными аналоговыми схемами... м.б. приближение будет точнее...
|
|
| Автор: | Trurl [ Среда, 05 Октябрь, 2011 11:28 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Драконограф писал(а): Природа (включая человеческую) непрерывна А про атомы и т.п. разве в школе не рассказывают? |
|
| Автор: | Дмитрий Маслов [ Среда, 05 Октябрь, 2011 11:28 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Естественно что условно. А о чём можно говорить неусловно? Все расчёты реальных физических систем выполняются приближённо. Но мы же используем простые электрические цепи с ёмкостями и транзисторами для выполнения алгоритмов, пишем программы для них, даже жизни свои доверяем этим системам. Время от времени модели и реальные процессы перестают соответствовать друг другу и тогда начинается поиск новых, более адекватных моделей. Что тут таинственного? Я ничего мистического здесь не вижу. Если есть какие-то конкретные примеры мне будет очень интересно о них узнать. |
|
| Автор: | Илья Ермаков [ Среда, 05 Октябрь, 2011 22:36 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Дмитрий Маслов писал(а): Но мы же используем простые электрические цепи с ёмкостями и транзисторами для выполнения алгоритмов, пишем программы для них, даже жизни свои доверяем этим системам. Ну так это обратный пример - ограничение пространства состояний физической системы до дискретного. Вопрос в том, что нет оснований утверждать, что никакая физическая система не может решить те задачи, которые неразрешимы на машине Тьюринга. Тезис Тьюринга-Чёрча-Маркова... говорит о том, что никакая алгоритмическая "штука" не может быть "мощнее", чем МТ, лямбда-исчисление, нормальные алгорифмы, машина Минского, алгоритмы Колмогорова.... и т.д. И этот тезис - гипотеза, которая подкреплена только тем, что каждая из предложенных алгоритмических абстракций оказывалась эквивалентной остальным. Доказательна здесь только эквивалентность. Плюс есть эмпирическая уверенность, что вряд ли можно придумать нечто, что будет мощнее, раз всё оно эквивалентно... Но напомню, что речь идёт именно про АЛГОРИТМИЧЕСКИЕ "штуки". При этом нет определения, что это такое. Только множество разных абстракций и возможность всегда придумать ещё одну, и опыт, подсказывающий, что для неё потом докажется эквивалентность. Но нет вообще никаких оснований для сравнения их с возможностями физических систем в целом. Такой вопрос в теории алгоритмов даже и поставлен быть не может, потому что это теория формальная, а не естественнонаучная. Насколько я знаю этот вопрос. |
|
| Автор: | Info21 [ Среда, 05 Октябрь, 2011 23:07 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Trurl писал(а): Илья Ермаков писал(а): А человеческий мозг? Можно ли уверенно говорить, что он не может быть мощнее, чем алгоритмическая машина? Скорее всего не может. Но это не важно. Даже если кто-то постиг истину, хоть бы и сверхъестественным образом, как бы он убеждал других? Например, я просветлился и понял, что Евклид был прав, а Лобачевский и пр. только путают людей. Но вот способа убедить других я не вижу. Разве что, основать Церковь Пятого Постулата. Каким бы ни был отдельный человеческий мозг, он должен произвести убедительный аргумент, являющийся конечной строкой литер. Вот в этом вся и штука. Гедель как раз про конечные строки литер. |
|
| Автор: | Владислав Жаринов [ Четверг, 06 Октябрь, 2011 09:06 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Trurl писал(а): Драконограф писал(а): Природа (включая человеческую) непрерывна А про атомы и т.п. разве в школе не рассказывают? Но насчёт того, что потом всё равно выводить отчуждаемую часть как конечные строки литер - это да.
|
|
| Автор: | Илья Ермаков [ Четверг, 06 Октябрь, 2011 09:37 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Info21 писал(а): Каким бы ни был отдельный человеческий мозг, он должен произвести убедительный аргумент, являющийся конечной строкой литер. Конечно, но ещё можно убедить по-другому: указать способ опытной проверки, который доступен другим. Тогда доказательство будет всё-таки прошито не в самой строке литер, а где-то в объективной реальности. Мы же просто отсылаем к ней за проверкой. Тот же Принцип Калашникова какой-нибудь: надёжней всего отправить за доказательством проверять на собственной ж... тех, кто сомневается
|
|
| Автор: | Info21 [ Четверг, 06 Октябрь, 2011 10:41 ] |
| Заголовок сообщения: | Re: Гёдель и программирование |
Илья Ермаков писал(а): Info21 писал(а): Каким бы ни был отдельный человеческий мозг, он должен произвести убедительный аргумент, являющийся конечной строкой литер. Конечно, но ещё можно убедить по-другому: указать способ опытной проверки, который доступен другим.Описываемый конечным набором литер. Илья Евгеньевич, не надо мистики. КонкретнЕе. |
|
| Страница 2 из 3 | Часовой пояс: UTC + 3 часа |
| Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |
|