Здравствуйте, Bill Baklushi, Вы писали:

BB>·>Это какое-то заблуждение и вообще не в тему. Зачем анализатору запускать программу? На то он и Анализатор. Он может просто, например, искать бесконечные циклы.
BB> Против любого такого анализатора можно придумать хитрый цикл, который анализатор не находит.
А с чего ты это взял? Мамой клянёшься? Собственно Тьюринг это и сделал — он формально доказал теоретическую невозможность построения такого умного анализатора, который распознает _любой_ хитрый цикл. ИЧСХ, распознавать огромное число бесконечных циклов вполне таки возможно.

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

BB>Цикл может зависеть от довольно широкого контекста состояний программы (переменных). Для анализа состояний и понадобится выполнение.
Ты просто подгоняешь свои рассуждения под уже известный ответ.

Здравствуйте, GhostCoders, Вы писали:

GC>Сейчас в соседней ветке прочитал про диагональный элемент и неполноту Геделя.
GC>Возможно, это связано (и Тьюринг строил свое доказательство под впечатлением доказательства Геделя о неполноте арифметики Пеано, вводя диагонализатор).

Конечно, это связано. Если бы мы могли алгоритмически решать проблему остановки, мы могли бы написать алгоритм, который перебирает все доказательства в арифметике Пеано (или любой другой теории с рекурсивно перечислимыми теоремами), и останавливается как только находит доказательство противоречия. Затем, используя наш способ, мы определили бы, останавливается этот алгоритм или нет, что позволило бы нам узнать, является ли теория непротиворечивой. Но вопрос остановки алгоритма можно выразить в языке арифметики Пеано, и, более того, если алгоритм останавливается и выдаёт определённый результат, то это всегда тривиально доказуемо в арифметике Пеано. Это значит, что если бы существовал способ алгоритмически решать проблему остановки, то арифметика Пеано могла бы доказывать собственную непротиворечивость, что, как мы знаем из теоремы Гёделя, невозможно сделать в непротиворечивой теории. По сути, эти два результата эквивалентны.

Здравствуйте, nikov, Вы писали:

N>Конечно, это связано. .... По сути, эти два результата эквивалентны.
Спасибо! Сейчас бегло прочитал это, интуитивно понял, но не в деталях.
В данный момент я не обладаю детальными знаниями о теоремах Геделя, поэтому надо будет подтянуть.
P.S.: Я так понимаю, что вы профессионально этим занимаетесь? Статические анализаторы какие-то строите?

Здравствуйте, Bill Baklushi, Вы писали:

BB>Как ты определишь, что программа зависла? Может быть просто долго считает?
Я вот тут сделал кое-какие предположения

Автор: GhostCoders
Дата: 06.03.20

.

Это, конечно, в большинстве своем, наверное, предположения дилетанта,
часть из которых, наверное, известны, а часть неверна.

Если интересно, ознакомтесь. Возникнут какие-то уточняюшее вопросы или замечания — пишите — я отвечу по мере своих возможностей.

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

Реальные компьютеры могут зависать толко циклически (если нет потока информации из вне).

Здравствуйте, ·, Вы писали:

GC>>Типа человеку предсказали умереть через год, а он заключил пари с предстказателем, так вот этот человек, чтобы выиграть пари, специально прожил до ста лет.
GC>>Или наоборот. Предсказатель предсказал, что человек будет жить до 100 лет, а человек, заключил с ним пари, что предсказатель не прав,
GC>>и совершил самоубийство на следующий день, чтобы выиграть пари.
·>Ничего не понял. Что за g()? Каким ещё предсказателем?
На самом деле довольно просто.
Вместо русской вики я открыл английскую и сразу понял фокус.

def g():
    if halts(g):
        loop_forever()

Допустим анализатор (функция halts) решил, что функция g() зависнет.
То эта самая функция g(), назло анализатору (для того, чтобы ему "нагадить" и дискредитировать его) нагло возвращает какое-то значение.
То есть делает "предсказание" анализатора неверным.
И наоборот, если анализатора для g вернет что она не зависнет, то она зависает.
Но думаю, вы это и сами знали?

GC>>Хотя у меня останутся возражения, что, мол, Анализатор возвратил результат функции (зависла или нет)
GC>>для того гипотетического запуска (или запуска через интерпретацию) этой функции, который он сделал (или мог гипотетически сделать) сам,
GC>>а не того запуска, что запустил его самого.
·>В док-ве теоремы никто ничего запускать не должен и вообще такое понятие не используется. Анализатор не обязан говорить "зависла ли". Он может сказать "зависнет ли". Т.е. условоно говоря... анализатор может быть статическим — смотреть на код и определять его зависаемость без запуска этого кода на выполнение.
Да, все верно. Только может быть статическим, а может и интерпретировать программу, например.
При интерпретации программы сохранять список посещенных полных состояний МТ и проверять на каждом шагу,
что новое состояние не находится в этом списке. Если находится — то мы определили, что анализуруемый алгоритм
завис циклически за конечное число шагов. Ациклические зависания таким способом не определить.
Если интересно — почитайте тут

Автор: GhostCoders
Дата: 06.03.20

мои рассуждения дилетанта, может и найдете для себя что-нибудь новое и интересное.
И да, тут же описан случай "The halting problem is theoretically decidable for linear bounded automata (LBAs)",
который я и называю "зависнуть циклически".

GC>>— как в функции в функциональных языках программирования, а не императивных, с наличием глобальных переменных, и когда результат функции зависит от предыдыщих (разные всякие undefined behaviour)
GC>>вызовов. Проще говоря, Тьюринг не допускает дребезга результатов алгоритмов (типа как undefined behaviour).
·>У тебя всё смешалось в кучу. Теорема об алгоритмах. А ЯП это лишь способ записи алгоритмов. Undefined behaviour это не свойство алгоритма, это относится к семантике ЯП, об его спецификации. Т.е. когда человек глядит на код и видит некую конструкцию, но не может сказать как сработает всё окружение начиная от компиляторов, их версий, линковщиков, железа, таймингов и т.п. о том что именно произойдёт.
Вот тут я с вами согласен. Смешалось, да.

Здравствуйте, GhostCoders, Вы писали:

GC>В данный момент я не обладаю детальными знаниями о теоремах Геделя, поэтому надо будет подтянуть.

Очень советую почитать на эту тему:

---

Верещагин Н.К., Шень А. Лекции по математической логике и теории алгоритмов, выложены авторами в свободный доступ: https://www.mccme.ru/free-books, ftp://ftp.mccme.ru/users/shen/logic
• Часть 1. Начала теории множеств
• Часть 2. Языки и исчисления
• Часть 3. Вычислимые функции

---

Torkel Franzén, Inexhaustibility: A Non-Exhaustive Treatment. Wellesley, Massachusetts: A K Peters, Ltd. 2004. Lecture Notes in Logic, #16, Association for Symbolic Logic. ISBN 1-56881-174-8

---

Pavel Pudlák, Logical foundations of mathematics and computational complexity. A gentle introduction, Springer 2013. Springer Monographs in Mathematics. ISBN 978-3-319-00118-0

---

Все они излагают материал очень подробно, изначально требуя лишь понимания математики на школьном уровне.

GC>P.S.: Я так понимаю, что вы профессионально этим занимаетесь? Статические анализаторы какие-то строите?

Да, я занимался компиляторами и статическим анализом раньше. Последнее время я работаю над построением индексов и поиском в документах.

Здравствуйте, ·, Вы писали:

·>А с чего ты это взял? Мамой клянёшься? Собственно Тьюринг это и сделал — он формально доказал теоретическую невозможность построения такого умного анализатора,
Вы оба доказываете друг другу одно и тоже — то что Анализатор нельза построить, ошибочно предполагая, что собеседник придерживается противоположного мнения.

Здравствуйте, GhostCoders, Вы писали:

GC>·>Ничего не понял. Что за g()? Каким ещё предсказателем?
GC>На самом деле довольно просто.
GC>Вместо русской вики я открыл английскую и сразу понял фокус.
GC>

GC>def g():
GC>    if halts(g):
GC>        loop_forever()
GC>

GC>Допустим анализатор (функция halts) решил, что функция g() зависнет.
Анализатор на вход берёт собственно сам текст этого самого g().

GC>То эта самая функция g(), назло анализатору (для того, чтобы ему "нагадить" и дискредитировать его) нагло возвращает какое-то значение.
Функция уже определена в виде этого кода. Покажи где в этом коде оператор нагаживания, я что-то не вижу.

GC>То есть делает "предсказание" анализатора неверным.
GC>И наоборот, если анализатора для g вернет что она не зависнет, то она зависает.
GC>Но думаю, вы это и сами знали?
У тебя какие-то хитрые алгоритмы, обладающие сознанием, волей и желанием нагадить. С такими алгоритмами да, теоремы доказывать не получится, их только уговаривать можно, Кнутом и Страуструпом.

GC>Да, все верно. Только может быть статическим, а может и интерпретировать программу, например.
GC>При интерпретации программы сохранять список посещенных полных состояний МТ и проверять на каждом шагу,
GC>что новое состояние не находится в этом списке. Если находится — то мы определили, что анализуруемый алгоритм
И что с этим можно сделать полезного?

GC>завис циклически за конечное число шагов. Ациклические зависания таким способом не определить.
И как мы отличим ациклический алгоритм от циклического? Ну сделали мы TREE(3) шагов — цикла не нашлось. Что это значит? Да ничего. Т.е. и циклические алгоритмы таким способом тоже не определить. Можно определить лишь алгоритмы работающие не дольше некоего N кол-ва шагов. Собственно всё. Для этого можно просто счётчик операций запустить и не выпендриваться с запоминанием состояний.

Здравствуйте, ·, Вы писали:

·>Функция уже определена в виде этого кода. Покажи где в этом коде оператор нагаживания, я что-то не вижу.
В википедии все есть.

·>У тебя какие-то хитрые алгоритмы, обладающие сознанием, волей и желанием нагадить.
Не алгоритмы, а программисты и математики, которые такие алгоримы пишут

·> С такими алгоритмами да, теоремы доказывать не получится, их только уговаривать можно, Кнутом и Страуструпом.
Ну вообще-то я уже признал, что я ошибался, и в доказательстве Тьюринга нет ошибки, еще пару постов выше.
А этот пост, с которым ты споришь, я привел как объяснение свой собственной неправоты.
Тут вообще нет предмета спора.

·>И что с этим можно сделать полезного?
Просто показал, что какие-то методы нахождения зависаний все такие есть.

GC>>завис циклически за конечное число шагов. Ациклические зависания таким способом не определить.
·>И как мы отличим ациклический алгоритм от циклического? Ну сделали мы TREE(3) шагов — цикла не нашлось. Что это значит? Да ничего.
Пока никак.

Здравствуйте, GhostCoders, Вы писали:

GC>·>А с чего ты это взял? Мамой клянёшься? Собственно Тьюринг это и сделал — он формально доказал теоретическую невозможность построения такого умного анализатора,
GC>Вы оба доказываете друг другу одно и тоже — то что Анализатор нельза построить, ошибочно предполагая, что собеседник придерживается противоположного мнения.
Он перепутал причину со следствием. Он утверждает, что "Против любого такого анализатора можно придумать хитрый цикл" — но это следствие теоремы остановки, а не её обоснование. Т.е. иначе говоря, хитрые циклы можно придумывать потому что Анализатор невозможен, а не то что хитрость циклов каким-то образом обосновывает невозможность Анализатора.

Здравствуйте, GhostCoders, Вы писали:

GC>·>Функция уже определена в виде этого кода. Покажи где в этом коде оператор нагаживания, я что-то не вижу.
GC>В википедии все есть.
Видимо, я не понимаю что ты имеешь в виду, в вики вроде ничего такого нет.

GC>·>У тебя какие-то хитрые алгоритмы, обладающие сознанием, волей и желанием нагадить.
GC>Не алгоритмы, а программисты и математики, которые такие алгоримы пишут
Но теорема-то об алгоритмах, а не о математиках. Не понимаю к чему ты это всё говоришь.

GC>·>И что с этим можно сделать полезного?
GC>Просто показал, что какие-то методы нахождения зависаний все такие есть.
Это какой-то бессмысленный метод. Можно просто ограничивать алгоритм по памяти и/или времени. И собственно всё.

Здравствуйте, ·, Вы писали:

·>Здравствуйте, GhostCoders, Вы писали:

GC>>·>Функция уже определена в виде этого кода. Покажи где в этом коде оператор нагаживания, я что-то не вижу.
GC>>В википедии все есть.
·>Видимо, я не понимаю что ты имеешь в виду, в вики вроде ничего такого нет.

Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. For any program f that might determine if programs halt, a "pathological" program g called with an input can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do. No f can exist that handles this case.

Выделил жирным. "Специально сделать обратно" — это очень вольно можно интерпретировать как "нагадить" .

GC>>·>У тебя какие-то хитрые алгоритмы, обладающие сознанием, волей и желанием нагадить.
GC>>Не алгоритмы, а программисты и математики, которые такие алгоримы пишут
·>Но теорема-то об алгоритмах, а не о математиках. Не понимаю к чему ты это всё говоришь.
Забудь, просто неудачная шутка.

GC>>·>И что с этим можно сделать полезного?
GC>>Просто показал, что какие-то методы нахождения зависаний все такие есть.
·>Это какой-то бессмысленный метод. Можно просто ограничивать алгоритм по памяти и/или времени. И собственно всё.
Может быть и так. С другой стороны этот метод позволяет находить зависания в очень хитрых циклах (вложенных в друг друга,
или в переплетении спагетти goto) в случае циклического зависания и относительно небольшого периода цикла зависания.

Здравствуйте, GhostCoders, Вы писали:

GC> specifically do the opposite of what f predicts g will do. No f can exist that handles this case.
GC> Выделил жирным. "Специально сделать обратно" — это очень вольно можно интерпретировать как "нагадить" .
Если оператор логического отрицания считать нагаживанием... ок теперь понятно откуда столько говнокода

GC> ·>Это какой-то бессмысленный метод. Можно просто ограничивать алгоритм по памяти и/или времени. И собственно всё.
GC> Может быть и так. С другой стороны этот метод позволяет находить зависания в очень хитрых циклах (вложенных в друг друга,
GC> или в переплетении спагетти goto) в случае циклического зависания и относительно небольшого периода цикла зависания.
Достаточно чтобы в цикле был какой-нибудь long++ счётчик (а это практически наверняка в каком-нибудь не совсем уж тривиальном коде) то Солнце скорее прогорит, чем ты дождёшься когда состояние повторится. Правда память под состояния у тебя закончится гораздо раньше. Т.е. работать такой подход на практике может только в очень специфических сценариях.

Здравствуйте, GhostCoders, Вы писали:

GC>Я вот тут в форуме Алгоритмы

Автор: GhostCoders
Дата: 08.03.20

(тоже на rsdn) написал про ошибку в доказательстве Тьюринга о неразрешимости проблемы остановки.
GC>Но что-то тот форум какой-то вялый.
GC>Может кто-то здесь прокомментирует?

Я професионально занимаюсь компиляторами и мой коментарий следующий: на данный момент эта задача находится на грани человеского познания.

Существующие материалы часто оперируют формулировкой из ряда "нетривиальные циклы (неразрешимо)". И тем самым замыливают возможность детального рассмотрения нетривиальности в течении последних 70-ти лет.

Однако, если убрать из формулировки машины Тьюринга возможность самомодификации кода (архитектура фон Неймана), и урезать ее до Гарвардской архитектуры, то интуитивно задача останова могла бы иметь решение с помошью анализа графов потока управления и данных с выводом граничных значений в местах ветвлений.

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

Эта и есть та самая граница научного познания.

Если вы спросите меня возможно ли это — то интуитивно я вам скажу, что может быть. Когда это могло бы произойти — через 50 лет как мимнимум, а может и через 200.

N>Очень советую почитать на эту тему:

N>

---

N>Верещагин Н.К., Шень А. Лекции по математической логике и теории алгоритмов, выложены авторами в свободный доступ: https://www.mccme.ru/free-books, ftp://ftp.mccme.ru/users/shen/logic
N>• Часть 1. Начала теории множеств
N>• Часть 2. Языки и исчисления
N>• Часть 3. Вычислимые функции
N>

---

N>Все они излагают материал очень подробно

Но не всегда верно, а именно, в Началах теории множеств приводится широко распространённое неверное доказательство теоремы о том, что в каждом бесконечном множестве содержится счётное подмножество.

Здравствуйте, σ, Вы писали:

σ>Но не всегда верно, а именно, в Началах теории множеств приводится широко распространённое неверное доказательство теоремы о том, что в каждом бесконечном множестве содержится счётное подмножество.

Ну они предупреждают, что излагают "наивную" теорию множеств, просто чтобы дать представление о предмете, достаточное для понимания 2-й и 3-й части. Там они почти всегда обходятся счётными множествами и используют конструктивный подход (за исключением обсуждения моделей и всяких там лёвенгеймов и скулемов).

Конечно же, их доказательство этой теоремы не настоящее. Они доказывают её через "и т.д.", и не приводят перед доказательством ни определения бесконечного множества, ни списка аксиом, на которые можно опираться. А существует ведь много разных определений бесконечного множества, доказательство эквивалентности которых требует аксиомы выбора. С некоторыми определениями и без аксиомы выбора эта теорема может и не выполняться: https://en.wikipedia.org/wiki/Axiom_of_choice#Statements_consistent_with_the_negation_of_AC). С другой стороны, одно из определений просто говорит, что "бесконечное множество — это множество, которое содержит счётное подмножество", и тут уже дажё аксиома выбора не нужна. 🙂

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

Здравствуйте, ·, Вы писали:

·>Правда память под состояния у тебя закончится гораздо раньше.

Это же классика — алгоритм черепахи и зайца. Достаточно хранить только два состояния.
Запускаем две машинки: медленную и быструю. Если есть цикл — то быстрая врежется состоянием в состояние медленной.

Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>·>Правда память под состояния у тебя закончится гораздо раньше.
EP>Это же классика — алгоритм черепахи и зайца. Достаточно хранить только два состояния.
EP>Запускаем две машинки: медленную и быструю. Если есть цикл — то быстрая врежется состоянием в состояние медленной.
Хорошая оптимизация, но не ничем поможет в контексте обсуждения. Этот алгоритм предназначен чтобы находить _длину_ цикла в списке про который заведомо известно, что в нём конечное число элементов. Этот алгоритм неприменим если мы этого не знаем.
Если это применить для обсуждаемой задачи, то это будет эквивалентно тупому счётчику шагов.
Да, по пространству машина работать сможет. Но с точки зрения практики это всё равно не поможет, т.к. с т.з. времени мы всё равно не сможем обнаруживать циклы, т.к. нужно конечное число шагов. Грубо говоря, если мы сделали N шагов, но цикл так и не обнаружили — мы всё ещё не знаем есть ли цикл или нет. А если просто выполнить машинку до N-го шага, то это будет быстрее и эффективнее чем запускать две машинки.

По-моему, из этого можно даже сделать вывод, что интерпретирующие Анализаторы сложнее тупого счётчика бессмысленны.

Возможно, конкретный ответ на заданный вопрос уже был дан выше (всю тему не читал, каюсь), но тем не менее.

Для ответа на вопрос, удобно рассмотреть проблему остановки в терминах множеств. Теорема Тьюринга, по сути, доказывает неразрешимость множества алгоритмов, останавливающихся на заданном наборе входных данных, являясь при этом частным случаем теоремы Райса-Успенского, которая доказывает ровно то же самое, но для любого нетривиального свойства, а не только остановки.

GC>"Странное" тут в том, что Тьюринг допускает анализатор, который зависает сам.
GC>И не рассматривает остальные варианты.

Это называется "полуразрешающий алгоритм". Если для элементов множества существует такой алгоритм, то оно является перечислимым.

GC>Другой (мой) вариант существования анализатора, это случай, когда анализатор всегда останавливается
GC>и возвращает 1 или 0 в зависимости от того, зависла или нет анализируемая программа.

А это называется "разрешающий алгоритм". Множества, для элементов которого такой алгоритм существует, являются разрешимыми.

Диагональный аргумент, заимствованный Тьюрингом у Гёделя (который, в свою очередь позаимствовал его у Кантора) доказывает неперечислимость множества алгоритмов, останавливающихся на заданном наборе данных. По теореме Поста, для того, чтобы оно было разрешимым, его дополнение (т.е. множество всех алгоритмов, зависающих на заданном наборе данных) должно быть перечислимым. Но с помощью того же самого диагонального аргумента можно показать неперечислимость также и дополнения, следовательно рассматриваемое изначально множество является неразрешимым.

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

Здравствуйте, ·, Вы писали:
·>Хорошая оптимизация, но не ничем поможет в контексте обсуждения. Этот алгоритм предназначен чтобы находить _длину_ цикла в списке про который заведомо известно, что в нём конечное число элементов. Этот алгоритм неприменим если мы этого не знаем.
Этот алгоритм применим к любым машинам с ограниченной памятью. Он не работает на МТ ровно потому, что её память ничем не ограничена: мы запросто можем получить неостановимый алгоритм без циклов.
Физические машины имеют ограниченную память, так что рано или поздно алгоритм либо остановится, либо войдёт в состояние, которое уже было.