powered by simpleCommunicator - 2.0.49     © 2025 Programmizd 02
Форумы / Программирование [игнор отключен] [закрыт для гостей] / Верификация сложности алгоритма
18 сообщений из 118, страница 5 из 5
Верификация сложности алгоритма
    #39828919
Interloper
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Ares_ekb,

Интересно, изучу ваши выкладки на досуге, спасибо.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39828921
Фотография Aklin
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
InterloperСложность должна быть не точной величиной, а указанием на один из классов сложности.

Interloperтак как не существует универсального алгоритма для определения факта остановки любого алгоритма
Не существует алгоритма для оценки неработающего алгоритма в виде черного ящика.

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


InterloperСложность должна быть не точной величиной, а указанием на один из классов сложности.Это сугубо теоретический вопрос тогда, а не вопрос программирования.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39828941
exp98
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
А ещё я тугодум и так и не понял
автор...алгоритма для проверки сложности, иначе этот алгоритм может быть преобразован в алгоритм определения факта остановки Для нас доказали теорему о неразрешимости массовой проблемы останова.
Проверка сложности является частным случаем алгоритма проверки останова. Для этого ч-го случая мне лично не приходилось видеть признанных доказательств неразр-ти.
Кроме того,не приходилось видеть и док-в того, что если неразрешима массовая проблема, то неразр-ма и частная проблема.

Тем не менее нам здесь пытались втюхать, что она верна по причине того, что является ч-м случ-м алгоритма проверки останова и потому верна. Т.о., налицо неправомерное применение "доказательства от противного", т.е. весьма противное доказательство. И прежде всего я протестовал против этого, поскольку все другие рассуждения были достаточно очевидны.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39828947
Interloper
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
AklinНе существует алгоритма для оценки неработающего алгоритма в виде черного ящика.

Слова "неработающего" и "в виде черного ящика" уберите, а так все верно. С чего вы выдумали, что речь идет о неработающих алгоритмах - ума не приложу.
Что касается вида, то он может быть любой, хоть исходный код. Не исходный код какого-то одного конкретного алгоритма: алгоритм оценки должен принимать на вход исходный код любого алгоритма. Для частного случая в виде подмножества алгоритмов, решение, безусловно существует.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39828948
Interloper
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
AklinЭто сугубо теоретический вопрос тогда, а не вопрос программирования.
Это вопрос теории алгоритмов, естественно, а не того программирования, которым вы занимаетесь в офисе.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39828949
Interloper
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
exp98Для этого ч-го случая мне лично не приходилось видеть признанных доказательств неразр-ти.
.
Доказательство приведено в этой теме на 2й странице. Оно достаточно простое, чтобы в нем мог разобраться любой, кто знает основные понятия математической логики.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39828961
Ares_ekb
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
kealon(Ruslan)попробуй ради интереса доказать так O(N) для алгоритма составления бинарной кучи
Чтобы доказать формально нужно время. Интересная идея, я попробую, если будет возможность. Но на это уйдет наверное неделя-две, потому что я никогда таким не занимался.

А с помощью эвристик это можно сделать так:

Алгоритм выглядит следующим образом (по ссылке ещё есть ссылка на прикольную книгу, где всё описано более подробно "Кормен, Т., Лейзерсон, Ч., Ривест, Р., Штайн, К. Глава 6. Пирамидальная сортировка // Алгоритмы: построение и анализ"):
Код: sql
1.
2.
3.
4.
Build_Heap(A)
  A.heap_size = A.length
  for i = floor(A.length/2) downto 1
    do Heapify(A, i)

где A - это входной массив, который нужно превратить в кучу
A.length - его длина (которая равна длине кучи A.heap_size и для простоты мы эту длину будем иногда обозначать просто N)
Heapify - это функция, которая упорядочивает элементы в поддереве кучи:
Код: sql
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
Heapify(A, i)
  left = 2i
  right = 2i+1
  largest = i
  if left <= A.heap_size и A[left] > A[largest]
    then largest = left
  if right <= A.heap_size и A[right] > A[largest]
    then largest = right
  if largest != i
    then Обменять A[i] и A[largest]
         Heapify(A, largest)



Допустим этот алгоритм написан на каком-то реальном ЯП, а не псевдоязыке. Мы распарсили его и получили абстрактное синтаксическое дерево (AST), которое будем анализировать.

Сначала оценим сложность функции Heapify:

Видим в AST этой функции рекурсивный вызов себя. Других рекурсивных вызовов или циклов нет, значит сложность определяется этим единственным вызовом. При рекурсивном вызове передаются 2 аргумента: A и largest. Аргумент A в теле функции никак не изменяется и передаётся как есть. Для largest возможны 3 варианта:

1) largest = i, в этом случае рекурсия прекращается
2) largest = 2i
3) largest = 2i+1

Короче анализатор AST должен сделать такие выводы:
1) С каждым рекурсивным вызовом i как минимум удваивается.
2) Рекурсия прекращается в худшем случае когда i достигает A.heap_size (для простоты будем называть её N)

В wiki и в книге из этого делается неправильный вывод, что сложность этой функции равна O(log N). Наш же анализатор должен сделать вывод, что сложность равна O(log N) - O(log i) или просто O(log N/i). Где log - логарифм по основанию 2. Попробую пояснить почему так.

Например есть цикл:
Код: sql
1.
for (int x = i; x < N; x += step) { ... }

Для него сложность будет O((N-i)/step). Если i=0 и step = 1, то это вырождается просто в O(N).

Для такого цикла:
Код: sql
1.
for (int x = i; x < N; x *= step) { ... }

Сложность будет O(log_step(N/i)), где log_step - логарифм по основанию step.

Функция Heapify эквивалентна как-раз такому циклу со step = 2.


Теперь оцениваем сложность Build_Heap. Видим в ней цикл от floor(N/2) до 1 с шагом 1. Сложность цикла равна
O(sum_i (сложность тела цикла)) =
O(sum_i (log N/i)) =
O(sum_i (log N) - sum_i (log i)) =
(раскрываем сумму по i от 1 до N/2)
O(N/2 * log N - log (N/2)!) =
(тут мы используем тот факт , что O(log N!) = O(N log N))
O(N/2 * log N - N/2 * log (N/2)) =
O(N/2 * log (N / N/2)) =
O(N/2 * log 2) =
(отбрасываем константы)
O(N)

Готово!


Чтобы все эти вычисления автоматизировать нужно:
1) Заложить все эти эвристики по анализу for, if, рекурсивных вызовов и т.п. в абстрактных синтаксических деревьях
2) Нужна какая-то система, которая упрощает O-выражения - это выглядит вполне реальным. Возможно подойдут готовые системы для символьных вычислений или можно самому что-то написать.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39828967
Ares_ekb
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Идея всего этого такая... В книге приводится какое-то очень не тривиальное доказательство сложности O(N). Там делается утверждение
Поскольку число вершин высоты h в куче из n элементов не превышает ceil(n / 2^(h+1)), а высота всей кучи не превышает floor(lg n), то время работы не превышаети дальше приводится какая-то безумная формула.

Автоматизировать такие рассуждения невозможно. А ту последовательность действий, которую я привёл выше, вполне можно автоматизировать.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829011
Ares_ekb
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Насчет формальных доказательств. Нашёл очень клёвую реализацию некоторого абстрактного императивного языка IMP2 для Isabelle HOL. В нём есть переменные, циклы, условия и т.п. Ещё можно задавать разные инварианты для императивных программ, которые можно доказывать. И ещё для этого языка буквально неделю назад запилили реализацию двоичной кучи как-раз по книге Кормена Т. и др. "Алгоритмы: построение и анализ". Там доказывается корректность этой реализации.

Причём реализация двоичной кучи занимает по идее 1 страницу, а доказательств там больше чем на 20 страниц. И это даже без доказательства сложности алгоритма. Это показывает на сколько всё сложно с формальными методами. На практике для произвольных алгоритмов реально использовать только какие-то эвристики, которые описывал выше.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829032
kealon(Ruslan)
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Ares_ekb,

да, в математическом доказательстве используется сходящаяся геометрическая прогрессия - тынц
И это очень простой пример, без подкавык.
По многим алгоритмам используется оптимистичная оценка, например: хэш-таблица, декартово дерево

Судя по всему, даже со специализированным языком "с подсказками" и частично работающее, в общем виде реально тянет на RocketScience
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829033
kealon(Ruslan)
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Ares_ekbНасчет формальных доказательств. Нашёл очень клёвую реализацию некоторого абстрактного императивного языка IMP2 для Isabelle HOL. В нём есть переменные, циклы, условия и т.п. Ещё можно задавать разные инварианты для императивных программ, которые можно доказывать. И ещё для этого языка буквально неделю назад запилили реализацию двоичной кучи как-раз по книге Кормена Т. и др. "Алгоритмы: построение и анализ". Там доказывается корректность этой реализации.

Причём реализация двоичной кучи занимает по идее 1 страницу, а доказательств там больше чем на 20 страниц. И это даже без доказательства сложности алгоритма. Это показывает на сколько всё сложно с формальными методами. На практике для произвольных алгоритмов реально использовать только какие-то эвристики, которые описывал выше.я так подозреваю, что если ты не НАСА, то платить программистам за такую разработку явно перебор :-)
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829138
Фотография Aklin
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
InterloperAklin
Слова "неработающего" и "в виде черного ящика" уберите, а так все верно. С чего вы выдумали, что речь идет о неработающих алгоритмах - ума не приложу.
Что касается вида, то он может быть любой, хоть исходный код. Не исходный код какого-то одного конкретного алгоритма: алгоритм оценки должен принимать на вход исходный код любого алгоритма. Для частного случая в виде подмножества алгоритмов, решение, безусловно существует.С того, что его разработчик не может гарантировать конечность времени исполнения этого алгоритма на допустимых входных данных.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829139
Фотография Aklin
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
InterloperAklinЭто сугубо теоретический вопрос тогда, а не вопрос программирования.
Это вопрос теории алгоритмов, естественно, а не того программирования, которым вы занимаетесь в офисе.Тогда речь не может идти о том, что на компьютере не хватит памяти, или вообще о количестве запусков.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829193
Dimitry Sibiryakov
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
InterloperСложность должна быть не точной величиной, а указанием на один из классов сложности.
Тогда вспоминай матан (если, конечно, для тебя это слово не матерное). Степенная функция отличается от линейной и логарифмической. Причём для их различения достаточно трёх точек.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829197
Фотография Aklin
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Dimitry SibiryakovПричём для их различения достаточно трёх точек.В указанных ТС пределах делать замеры нельзя, ибо функция может потенциально зависнуть.

А если она "может" то зависнет.
А если зависнет, то встает вопрос об алгоритмически невозможном определении конечности этого алгоритма, а это известная доказанная проблема, поэтому даже пытаться не стоит =)

А доказывать математически он не хочет.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829261
Ares_ekb
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
kealon(Ruslan)да, в математическом доказательстве используется сходящаяся геометрическая прогрессия - тынц

И это очень простой пример, без подкавык.Проблема таких доказательств как по ссылке в том, что их невозможно автоматизировать. Там очень много рассуждений, каких-то посылок, которые берутся просто из головы автора и никак не следуют из структуры алгоритма. Например, откуда взялась эта лемма "Пусть для какого-то элемента массива при вызове siftdown было сделано i вызовов оператора swap. Тогда его индекс не превосходил floor(n/2^i)"? Ни один инструмент точно не сможет сформулировать и доказать такую лемму из ниоткуда.

Чтобы можно было оценивать сложность автоматически, нужно свести эту процедуру к каким-то очень простым шагам. Пусть этих шагов будет очень много, пусть там будет много тупого перебора, но зато это можно автоматизировать.

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

kealon(Ruslan)Судя по всему, даже со специализированным языком "с подсказками" и частично работающее, в общем виде реально тянет на RocketScienceЕсли полностью формальное доказательство, то да. А если какие-то полуформализованные эвристики по анализу кода, как я описывал, то вполне реально сделать. Хотя даже это вполне потянуло бы на диссертацию :)
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39829526
vas0
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Если взять просто быструю сортировку Хоара (QuickSort). Сложность в худшем n^2. Сложность в среднем n*log, да и то сложность в среднем оценивается лишь вероятностно.

Доказательство сложности в среднем даже зная алгоритм непростая задача. А для черного ящика видимо и вообще мрак. Если "опорный элемент" для хоара будет случайно выбираться, уже с оценкой будешь иметь проблему: иногда n*log, а иногда n^2.

Оценка по сложности это скорее подсказка, чтобы не попасть с проклятием размерности, а не точная величина.
...
Рейтинг: 0 / 0
Верификация сложности алгоритма
    #39836576
Фотография SashaMercury
Скрыть профиль Поместить в игнор-лист Сообщения автора в теме
Участник
Interlopermaytonпропущено...

Твои уточняющие вопросы напоминают легкий троллинг отвечающих.
Тебе уже в первом ответе дали методику.

Ты ее применил? Ты нарисовал график в Excel?

Давай дружище сделай как советуют опытные. А потом подойдешь к теории снова.

График меня не интересует. Я уже понял, что проблема алгоритмически неразрешима.
Вопрос я задал фундаментальный, решение тупо взять нарисовать график, очевидно, не решает поставленную задачу.
InterloperПредположим, у нас есть программно реализованный алгоритм, решающий некую задачу. Предполагается, что этот алгоритм имеет определенную сложность, выраженную нотацией "О большое", например, O(n*logn). Мы можем вызывать алгоритм на разных входных данных и замерять время его выполнения.
Как программно проверить, верно ли предположение о сложности?

Программно проверить? Напишите программу, если хотите программно проверить. Одним из параметров будет функция подозрительная на асимптотику, проведите ряд экспериментов по n, постройте отношение затраченного времени черного ящика и ф. подозрительной на асимптотику, если функция та самая, то в пределе получите константу. Что там как вы говорите алгоритмически неразрешимого? Вам по-моему о чем-то подобном говорили
...
Рейтинг: 0 / 0
18 сообщений из 118, страница 5 из 5
Форумы / Программирование [игнор отключен] [закрыт для гостей] / Верификация сложности алгоритма
Целевая тема:
Создать новую тему:
Автор:
Закрыть
Цитировать
Найденые пользователи ...
Разблокировать пользователей ...
Читали форум (0):
Пользователи онлайн (0):
x
x
Закрыть


Просмотр
0 / 0
Close
Debug Console [Select Text]