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

G>>Существует алгоритм-анализатор, который для любого начального состояния машины размером S, ограниченного в памяти размером M >> S,
G>>может предсказать останавливаемость за количество шагов T. Причем, S << T << M

Pzz>Существует. Заключается в запуске этой программы и ожидании, пока она либо не остановится, либо не переберет все свои возможные состояния. Только этот алгоритм настолько медленный, что лишен практического смысла

Тогда T = O(2^M), что противоречит условию S << T << M

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


G>>Не, ну так не интересно, ведь вся соль проблемы в том, что анализатор должен находить нетривиальный способ предсказания остановки.
S>Не факт, что такой способ существует.

Ну так это же и есть суть проблемы. Определить, есть такой способ или нет.
Смысл именно в том, чтобы найти эквивалентную формулировку проблемы останова, где можно обойтись без парадоксов бесконечностей, типа сумм Рамануджана.

S>Эмпирическое правило вычислимости: все мало-мальски интересные задачи либо невычислимы, либо NP-полны.
S>А вы хотите не просто полиномиальности, а линейности алгоритма.

Отнюдь.
Если анализатор окажется NP-полной проблемой, или даже S << T = O(2^exp(S)) << M, это тоже будет очень шикарно.

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

g> _>Берём, например, теорему Ферма и ищем решения x^n+y^n=z^n перебором
g> _>если решение есть выходим иначе ищем до посинения. Как анализатор может понять есть там хоть одно решение или нет?
g> Ничто не мешает анализатору быть суперинтеллектом, аналитически доказывающим теорему Ферма.
Сабж мешает же.

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

g>> Ничто не мешает анализатору быть суперинтеллектом, аналитически доказывающим теорему Ферма.
·>Сабж мешает же.

Сабж то как раз и требуется доказать или опровергнуть.

Здравствуйте, graniar, Вы писали:
G>Ну так это же и есть суть проблемы. Определить, есть такой способ или нет.
Ставлю $100 на NP-completeness. Это переместит проблему в область "математически разрешимо, но коммерчески невыгодно".

G>Если анализатор окажется NP-полной проблемой, или даже S << T = O(2^exp(S)) << M, это тоже будет очень шикарно.
В этой формуле нет размера программы. Вы включаете саму программу в S? Это, в принципе, логично, т.к. код у нас всё равно эквивалентен данным. Можно записать 42 в "область параметров" и сделать ldarg.0; а можно просто сделать ldc 42 безо всяких параметров.
В общем, NP-complete решение не интересно совсем.
Если оно окажется NP-complete, то нас всё ещё будут интересовать приближённые решения с лучшей асимптотикой.

Здравствуйте, Pzz, Вы писали:
Pzz>И я читал где-то, что чтобы просто последовательно перебрать все состояния N-битного счетчика, не хватит всей энергии вселенной. Причем N какое-то совсем небольшое, в районе то ли 128, то ли 256 бит.
Даже 64 — уже очень много. См. байку про шахматы.
Pzz>А у меня в программе обычно больше 4-х переменных типа int
На практике нетривиальные циклы встречаются не так уж и часто; поэтому если нас интересует прикладная надёжность, то решение с двумя бегунами и общим таймаутом вполне адекватно.
Таймаут у нас предоставляет страховочную сетку для нетривиальных случаев; а благодаря наличию детектора зацикливания эту сетку можно переместить достаточно далеко от старта.
Тогда у нас есть 100% гарантия того, что неудачный код не съест безлимитный ресурс, плюс некоторая уверенность в том, что простые косяки не станут бесполезно прогревать воздух в течение миллиардов операций.

Здравствуйте, ·, Вы писали:
·>"Если пространство состояний машины конечно" — это допущение эквивалентное тому, что программа останавливается.
Нет. Даже при конечности пространства состояний программа может никогда не останавливаться.
Вот вам минимальный пример:

while(true);

·>Впадаемость в цикл — это не критерий для сабж.
Для конечного пространства состояний — критерий. Для бесконечного — увы.

·>И? Как она себя поведёт на 3Мб памяти? Т.е. проверить зависнет ли программа — запустить, подождать определённое кол-во времени. Эти манипуляции с шагом-двумя ничего нового не сообщат.
Сообщат. "Определённое количество времени" как раз ничего не говорит — может быть, надо было просто подождать ещё секундочку, и программа бы успешно остановилась. А может быть — наоборот, она за это время уже миллион раз прошла через то же состояние, и детектор циклов бы давно её поймал.

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

·>Пример. Можно легко написать простой алгоритм, который перебирает числа и если a^n+b^n==c^n , то завершает. Ты запустил эту прогу на компьютере x86 с терабайтом памяти. Она не вышла, твой обнаружитель циклов ничего не обнаружил.
Этого не может быть. Либо она впадает в цикл, либо выходит. Каким образом вы себе представляете "неостановку" программы на машине конечного размера?

·>Какой из этого можно сделать вывод?
Можно сделать вывод о том, что я плохо объяснил вам принцип работы детектора циклов.

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

G>Есть такая классическая проблема о том, возможно ли в принципе проанализировать любую программу и предсказать, зависнет она или нет.

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

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

Здравствуйте, kov_serg, Вы писали:
G>>Ну то есть, вот допустим я написал такую программу-анализатор, которая принимает на вход начальное состояние виртуальной машины и выдает ответ, остановится она или нет.
_>Берём, например, теорему Ферма и ищем решения x^n+y^n=z^n перебором
_>если решение есть выходим иначе ищем до посинения. Как анализатор может понять есть там хоть одно решение или нет?
Для начала невредно вспомнить, что Ферма имел в виду целые числа.
А в компьютере никаких "целых чисел" нет.
Обычная арифметика работает не с Z, а кольцом вычетов по модулю 2^N.
Арифметика с "бесконечными целыми" всё ещё работает с целыми вполне себе ограниченного размера.
Поэтому никакая реальная программа не сможет перебрать "все целые числа".
Построение анализатора, который бы проверял воображаемую программу для воображаемой машины, невозможно.
А вот построение анализатора, который бы проверял реальную программу на реальной машине — теоретически возможно.
И если мы реализовали перебор корректно, то программа успешно переберёт все доступные ей целые числа и остановится.
А если мы допустили в программе косяк, то она впадёт в цикл и её поймает детектор циклов.

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

Здравствуйте, anonymouse2, Вы писали:
A>Если же машина Тьюринга конечна (с конечной лентой), то у нее конечное число состояний, которые можно просто перечислить. Значит и программа (содержимое ленты) может быть только конечной. Соответственно, можно простым запуском за конечное время понять, куда мы попадаем из текущего состояния: в состояние "СТОП" или в одно из конечного числа ранее пройденных и сохраненных в некоем списке состояний (что означает бесконечный цикл). Т.е. на каждой итерации работы машины берем ее полное состояние, ищем в списке, и если оно там есть — мы зациклились, если нет — сохраняем новое состояние в списке и идем дальше.
Даже список не нужен — просто запускаем вторую машину вдвое быстрее.

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

Pzz>>А у меня в программе обычно больше 4-х переменных типа int
S>На практике нетривиальные циклы встречаются не так уж и часто; поэтому если нас интересует прикладная надёжность, то решение с двумя бегунами и общим таймаутом вполне адекватно.

На практике есть много полезных частных случаев, поддающихся автоматизированному анализу. Поэтому статические анализаторы кода — полезный инструмент. Но не всемогущий.

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

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

Pzz>>На практике есть много полезных частных случаев, поддающихся автоматизированному анализу. Поэтому статические анализаторы кода — полезный инструмент. Но не всемогущий.
S>Ну... Да. В целом, мир уныл и безнадёжен. Одно из частных проявлений этого всеобщего принципа — это как раз ограничение вычислимости.

Наоборот, по-моему. Именно ограниченность мира делает возможным применение инженерной выдумки. Если бы у нас была золотая рыбка, которая исполняет любые наши желания, вот тогда, действительно, мир был бы уныл и безнадежен. Зачем к чему-то стремиться, если и так всё есть?

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

Такой язык уже сделали, Agda незывается

S>А, значит, будут существовать какие-то программы, которые можно написать для МТ, но нельзя — для нашей машины.

Да. И в этом нет ничего плохого.

S>Ну, и, естественно, окажется, что как раз самые интересные задачи — именно такие Неразрешимые на нашем "доказуемом языке".

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

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

S> ·>"Если пространство состояний машины конечно" — это допущение эквивалентное тому, что программа останавливается.
S> Нет. Даже при конечности пространства состояний программа может никогда не останавливаться.
Сабж не для минимальных известных примеров, а для общего случая. На вход подаётся произвольный код и для него надо определить сабж.

S> ·>Впадаемость в цикл — это не критерий для сабж.
S> Для конечного пространства состояний — критерий. Для бесконечного — увы.
Это просто другая задача. С тем же результатом.
Есть множество задач, которые алгоритмически эквивалентны проблеме остановки. Так вот, твоя задача "укладывается ли код в конечное число состояний" — эквивалентна сабжу.

S> ·>И? Как она себя поведёт на 3Мб памяти? Т.е. проверить зависнет ли программа — запустить, подождать определённое кол-во времени. Эти манипуляции с шагом-двумя ничего нового не сообщат.
S> Сообщат. "Определённое количество времени" как раз ничего не говорит — может быть, надо было просто подождать ещё секундочку
Бинго! Ровно то же с твоим ограничением по памяти. Надо было просто дать ещё один байтик, и программа бы успешно остановилась.

S> ·>Зато она себя может начать вести себя по-другому на двух таких машинах соединённых сетью.
S> Две машины соединённых сетью эквивалентны одной машине с пространством состояний 265.
Именно! Ты ошибся утверждая, что "достаточно проверить её на "машине" с памятью размером 2⁶⁴". Нет. Не достаточно даже для x86.

S> ·>Пример. Можно легко написать простой алгоритм, который перебирает числа и если a^n+b^n==c^n , то завершает. Ты запустил эту прогу на компьютере x86 с терабайтом памяти. Она не вышла, твой обнаружитель циклов ничего не обнаружил.
S> Этого не может быть. Либо она впадает в цикл, либо выходит. Каким образом вы себе представляете "неостановку" программы на машине конечного размера?
Ты игнорируешь третью альтернативу "не влезло в твоё произвольное ограничение по памяти".
Ты исподтишка подменяешь исходную задачу и вместо решения для данной задачи "a^n+b^n==c^n" ты выдаёшь решение для "a^n+b^n==c^n, n<2^64". Но это не даёт ничего для решения данной задачи.

S> ·>Какой из этого можно сделать вывод?
S> Можно сделать вывод о том, что я плохо объяснил вам принцип работы детектора циклов.
Да я знаю это, алгоритм черепахи и зайца называется или вроде того.

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

g> g>> Ничто не мешает анализатору быть суперинтеллектом, аналитически доказывающим теорему Ферма.
g> ·>Сабж мешает же.
g> Сабж то как раз и требуется доказать или опровергнуть.
Так он доказан, лет сто назад уж. Доказан как строгая математическая теорема.

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

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

·>Бинго! Ровно то же с твоим ограничением по памяти. Надо было просто дать ещё один байтик, и программа бы успешно остановилась.
Невозможно "дать ещё один байтик" программе, в которой адресация памяти сделана при помощи 32х-разрядных указателей.

·>Именно! Ты ошибся утверждая, что "достаточно проверить её на "машине" с памятью размером 2⁶⁴". Нет. Не достаточно даже для x86.
Достаточно, если программа не собирается общаться по сети.

·>Ты игнорируешь третью альтернативу "не влезло в твоё произвольное ограничение по памяти".
Что значит "не влезло"? Как вы себе это представляете?
·>Ты исподтишка подменяешь исходную задачу и вместо решения для данной задачи "a^n+b^n==c^n" ты выдаёшь решение для "a^n+b^n==c^n, n<2^64". Но это не даёт ничего для решения данной задачи.
Не исподтишка, а вполне открыто. Мне кажется, что от вашего внимания ускользает важный факт — на реальной машине эту задачу перебором решить невозможно. В принципе.
А решаемость этой задачи на воображаемой машине сама по себе не очень интересна — потому, что решение-то тоже воображаемое.

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

Здравствуйте, Pzz, Вы писали:
Pzz>Можно компактно собрать неразрешимые в кучку, и там их компактно разрешить, человеческим разумом, без автоматического доказатора.
А вот это уже опирается на предположение о том, что человеческий разум вычислительно мощнее автоматического доказатора.
То есть на трансцендентную природу человеческого сознания

Лично я в это не верю — я верю в тезис Чёрча. Так что всё, что мы можем компактно сделать — это совершить акт веры. Типа "мы принимаем P < NP без строгого доказательства".

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

Pzz>>Можно компактно собрать неразрешимые в кучку, и там их компактно разрешить, человеческим разумом, без автоматического доказатора.
S>А вот это уже опирается на предположение о том, что человеческий разум вычислительно мощнее автоматического доказатора.
S>То есть на трансцендентную природу человеческого сознания

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

S>Лично я в это не верю — я верю в тезис Чёрча. Так что всё, что мы можем компактно сделать — это совершить акт веры. Типа "мы принимаем P < NP без строгого доказательства".

Мы еще можем изобретать новые сущности.

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

G>Реальных архитектур, имеешь в виду с ограничением по используемой памяти? В стиле, как Sinclair выше привел, или нечто более практичное?

Возможно, неправильно выразился. На практике, если нужно доказать алгоритм, то берут конкретную архитектуру и конкретный алгоритм. Если нужно, то модифицируют его. Постановку задачу останова часто неправильно понимают из-за запутанной формулировки. Кажется, что теорема гласит "терминируемость программы невозможно доказать", а в реальности — невозможно доказать терминируемость в общем случае, поэтому и доказательство вида "вот есть программа, для которой невозможно доказать, что она остановится". Но, скажем, int main() { return 0; } вполне себе доказуема в плане останова. Таким образом ценность теоремы в том, что она говорит учёным "не пытайтесь найти универсальный способ анализа алгоритма на предмет останова, корректности и т.д. — в общем случае это невозможно".

И в этом плане сабж перекликается с печально известной гипотезой P = NP. В интернетах любят пугать квантовыми компьютерами и тем роковым днём, когда P = NP будет доказано, и сотни банков падут по всему миру, вода поднимается на 33 метра, а живые позавидуют мёртвым. А на деле, если доказать, что P = NP, то никоим образом полиномиальный алгоритм факторизации простых чисел не возникнет сам собой, его ещё нужно будет придумать.

Здравствуйте, Pzz, Вы писали:
Pzz>Нет. Просто человек может придумать новый способ доказательства на ходу, а доказатор будет пользоваться теми, которые в него предыдущие человеки заложили.
Или придумает новый способ доказательства на ходу. Почему нет?

Pzz>Мы еще можем изобретать новые сущности.
Ничуть не больше, чем МТ.