Здравствуйте, Куть, Вы писали:
К>А может, не нужно перебирать все строки, а можно как-нибудь сгруппировать их? А что, если Анализатор сам этим займётся на основе текста программы парсера, которую подали ему на вход?
Вооот...
Это другой полюс исследований в этой области.
Делается это через "док-ва". В практическом плане на прямо сегодня — через дедукцию и парные ей альфа/бета-редукции. Есть некий набор примитивов, про которые известны их характеристики. Любая программа — комбинация таких примитивов с учетом их ограничений. Св-ва подавляющего большинства однопоточных алгоритмов можно вывести через св-ва их примитивов и способа их комбинации.
Это т.н. "символьные вычисления" — противоположность твоему подходу.
К>Но люди как-то поняли, что она останавливается.
Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1).
К>Я писал про запуск парсера на одной строке, грубо говоря. Это свойство большинства алгоритмов: они не перебирают все возможные состояния, как твоя программа, которая запускает парсер на всех возможных строках. К>Так какие фундаментальные ограничения у алгоритма?
"Алгоритм" не в состоянии сделать вывод о корректности программы за разумное время. "Алгоритм" может только выдать "да/нет" для конкретного набора входных данных. Чем это лучше запуска целевой программы на этих же данных — я ХЗ, если честно. От того, что мы проэмулировали императивный вычислитель, мы не поменяли низлежащую вычислительную модель; мы лишь, считай, добавили немного отладочной информации. ))
Здравствуйте, vdimas, Вы писали:
V>Это т.н. "символьные вычисления" — противоположность твоему подходу.
Этот "подход" был использован лишь как способ доказать на примере, что анализатор для программ с конечной памятью существует.
Напомню, что в оригинальной проблеме остановки Анализатора не существует.
V>Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1).
Наверное, спутал с индукцией? =)
V> Чем это лучше запуска целевой программы на этих же данных — я ХЗ, если честно.
Целевая программа может никогда не завершится, а Анализатор всегда завершается.
Здравствуйте, Куть, Вы писали:
V>>Это т.н. "символьные вычисления" — противоположность твоему подходу. К>Этот "подход" был использован лишь как способ доказать на примере, что анализатор для программ с конечной памятью существует.
Похоже, ты уже споришь сам с собой. Я же не с этим спорил, а с тем, что в практическом плане это нам ничего не даёт.
К>Напомню, что в оригинальной проблеме остановки Анализатора не существует.
Я и не обсуждал эту проблему. Я демонстрировал, что твой Анализатор не работает лучше, чем сценарий непосредственного запуска самой программы. Именно поэтому предложил покопаться в альтернативном направлении.
V>>Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1). К>Наверное, спутал с индукцией? =)
Почему спутал? Индукцией является умозрительный вывод (человеком) характеристик алгоритма от i = 0, 1.. до произвольного N, в процессе же работы символьного анализатора происходит обратное — именно дедукция.
V>> Чем это лучше запуска целевой программы на этих же данных — я ХЗ, если честно. К>Целевая программа может никогда не завершится, а Анализатор всегда завершается.
Я давал оценки времени этого "всегда завершается" для небольшой разрядности и небольшого (по современным меркам) пространства состояний — Вселенная успеет миллиарды миллиардов раз по кругу схлопнуться в ЧД и снова взорваться.
Т.е., в смысле здравого материализма — нет ровно никакой разницы.
Здравствуйте, Evgeny.Panasyuk, Вы писали:
EP>Но из этого отнюдь не следует того, что для какого-то конкретного алгоритма МТ у нас не может быть алгоритма МТ доказательства его не останова.
С этим никто и не спорит, просто напоминают, что такой алгоритм может быть выражен более простой моделью — КА, например. И прямо из св-в КА следует конечность мн-ва его состояний.
Здравствуйте, vdimas, Вы писали:
EP>>Но из этого отнюдь не следует того, что для какого-то конкретного алгоритма МТ у нас не может быть алгоритма МТ доказательства его не останова. V>С этим никто и не спорит, просто напоминают, что такой алгоритм может быть выражен более простой моделью — КА, например. И прямо из св-в КА следует конечность мн-ва его состояний.
Конкретный обсуждаемый алгоритм не может быть выражен в КА, при этом у нас есть доказательство его не останова.
Здравствуйте, vdimas, Вы писали:
V>Похоже, ты уже споришь сам с собой. Я же не с этим спорил, а с тем, что в практическом плане это нам ничего не даёт.
Ничего не даёт использование Анализатора вообще или конкретного описанного в доказательстве алгоритма (назовем его "наивным")?
Если наивного, то кто ещё спорит сам с собой =)
Если вообще, то есть практическое применение: http://rsdn.ru/forum/philosophy/6186702.1
V>Я и не обсуждал эту проблему. Я демонстрировал, что твой Анализатор не работает лучше, чем сценарий непосредственного запуска самой программы. Именно поэтому предложил покопаться в альтернативном направлении.
А я могу продемонстрировать, что это принципиально разные вещи.
Возьмём программу на питоне:
while True:
pass
print("Done")
Даже наивный Анализатор завершается мгновенно, а программа не завершается.
К>Она тоже будет работать дольше, чем время жизни вселенной. Но люди как-то поняли, что она останавливается. V>Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1). К>Наверное, спутал с индукцией? =) V>Почему спутал? Индукцией является умозрительный вывод (человеком) характеристик алгоритма от i = 0, 1.. до произвольного N, в процессе же работы символьного анализатора происходит обратное — именно дедукция.
Ты потерял контекст, мы и говорили о человеке. Аккерман опубликовал свою функцию в начале 20-го века.
V>Я давал оценки времени этого "всегда завершается" для небольшой разрядности и небольшого (по современным меркам) пространства состояний — Вселенная успеет миллиарды миллиардов раз по кругу схлопнуться в ЧД и снова взорваться. V>Т.е., в смысле здравого материализма — нет ровно никакой разницы.
Для программы выше ты не успеешь подумать о вселенной, а Анализатор уже завершится.
Здравствуйте, Куть, Вы писали:
V>>Я и не обсуждал эту проблему. Я демонстрировал, что твой Анализатор не работает лучше, чем сценарий непосредственного запуска самой программы. Именно поэтому предложил покопаться в альтернативном направлении. К>А я могу продемонстрировать, что это принципиально разные вещи. К>Возьмём программу на питоне: К>Даже наивный Анализатор завершается мгновенно, а программа не завершается.
Тем не менее, я продемонстрировал ситуацию, когда применение анализатора ничем не лучше.
А в подобных приведенному сниппету современные компиляторы разобраться могут сами — выдают предупреждение о бесконечной рекурсии и т.д.
К>Ты потерял контекст, мы и говорили о человеке. Аккерман опубликовал свою функцию в начале 20-го века.
Словоблудие уже пошло, сорри. Во времена Аккермана не было чему "работать дольше, чем время жизни вселенной", компьютеров еще не было. А если мы говорим о времени работы программы, то компьютер индукцию не умеет, он умеет обратное по заданным формулам.
V>>Т.е., в смысле здравого материализма — нет ровно никакой разницы. К>Для программы выше ты не успеешь подумать о вселенной, а Анализатор уже завершится.
Я по работе, бывает, сталкиваюсь с дедлоками или зацикливаниями системы из нескольких ммм, назовём их "агентами", то бишь относительно независимыми процессами в рамках одной программы (такое зацикливание тоже выглядит как дедлок для конкретного многопоточного алгоритма). Причем, описанные эффекты бывают наведены такими причудливыми сценариями, что без пол-литры и не разберешься))
Даже в MS не сумели полностью избавиться от дедлоков в их SQL-сервере по объективным причинам.
Так вот, мой посыл в том, что современная многопоточная программа — это автомат с охренительным пространством состояний. И именно для обычной современной программы подобный анализатор фактически бесполезен из-за указанных мною ограничений. Простое зацикливание обнаруживается простой отладкой и это такой ничтожный %% всех сценариев, что овчинка выделки не стоит. А вот найти потенциальный сценарий дедлока или зацикливания алгоритма (алгоритмов) из мн/ва общающихся процессов, прогнав всевозможные взаимные относительные состояния всех потоков исполнения — вот это, действительно, будет востребованная весчь. И всё моё участие здесь сводится к тому, чтобы на пальцах объяснить, что избранный тобой путь поставленную задачу принципиально не решает из-за фундаментальных ограничений этого подхода (например, из двух процессов по 100 состояний в каждом, после прогона их всевозможных взаимных состояний, получим 10тыщ различных состояний эквивалентного одного автомата, и я давал прикидки именно на такой порядок кол-ва состояний).
В общем, нужен другой подход. Нужен символьный анализ, нужен "алфавит" известных "кубиков", нужен анализ и декомпозиция алгоритмов до этих кубиков с известными св-вами и затем аналитический вывод св-в программы из знаний о св-вах известных композиций из известных кубиков и далее по иерархии таких композиций. Это навскидку. А как оно будет, если заняться этим всерьез — я ХЗ.
