Добро пожаловать в форум, Guest  >>   Войти | Регистрация | Поиск | Правила | В избранное | Подписаться
Все форумы / Программирование Новый топик    Ответить
Топик располагается на нескольких страницах: Ctrl  назад   1 2 3 4 [5]      все
 Re: Верификация сложности алгоритма  [new]
Interloper
Member

Откуда: Москва
Сообщений: 488
Ares_ekb,

Интересно, изучу ваши выкладки на досуге, спасибо.
20 июн 19, 18:33    [21912443]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Aklin
Member

Откуда: Прямо сейчас меня здесь нет
Сообщений: 58146
Interloper
Сложность должна быть не точной величиной, а указанием на один из классов сложности.


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

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

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


Interloper
Сложность должна быть не точной величиной, а указанием на один из классов сложности.
Это сугубо теоретический вопрос тогда, а не вопрос программирования.
20 июн 19, 18:39    [21912446]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
exp98
Member

Откуда:
Сообщений: 1674
А ещё я тугодум и так и не понял
автор
...алгоритма для проверки сложности, иначе этот алгоритм может быть преобразован в алгоритм определения факта остановки
Для нас доказали теорему о неразрешимости массовой проблемы останова.
Проверка сложности является частным случаем алгоритма проверки останова. Для этого ч-го случая мне лично не приходилось видеть признанных доказательств неразр-ти.
Кроме того,не приходилось видеть и док-в того, что если неразрешима массовая проблема, то неразр-ма и частная проблема.

Тем не менее нам здесь пытались втюхать, что она верна по причине того, что является ч-м случ-м алгоритма проверки останова и потому верна. Т.о., налицо неправомерное применение "доказательства от противного", т.е. весьма противное доказательство. И прежде всего я протестовал против этого, поскольку все другие рассуждения были достаточно очевидны.
20 июн 19, 20:09    [21912483]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Interloper
Member

Откуда: Москва
Сообщений: 488
Aklin
Не существует алгоритма для оценки неработающего алгоритма в виде черного ящика.

Слова "неработающего" и "в виде черного ящика" уберите, а так все верно. С чего вы выдумали, что речь идет о неработающих алгоритмах - ума не приложу.
Что касается вида, то он может быть любой, хоть исходный код. Не исходный код какого-то одного конкретного алгоритма: алгоритм оценки должен принимать на вход исходный код любого алгоритма. Для частного случая в виде подмножества алгоритмов, решение, безусловно существует.
20 июн 19, 21:04    [21912495]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Interloper
Member

Откуда: Москва
Сообщений: 488
Aklin
Это сугубо теоретический вопрос тогда, а не вопрос программирования.

Это вопрос теории алгоритмов, естественно, а не того программирования, которым вы занимаетесь в офисе.
20 июн 19, 21:05    [21912496]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Interloper
Member

Откуда: Москва
Сообщений: 488
exp98
Для этого ч-го случая мне лично не приходилось видеть признанных доказательств неразр-ти.
.

Доказательство приведено в этой теме на 2й странице. Оно достаточно простое, чтобы в нем мог разобраться любой, кто знает основные понятия математической логики.
20 июн 19, 21:06    [21912497]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Ares_ekb
Member

Откуда: Екатеринбург
Сообщений: 1300
kealon(Ruslan)
попробуй ради интереса доказать так O(N) для алгоритма составления бинарной кучи

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

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

Алгоритм выглядит следующим образом (по ссылке ещё есть ссылка на прикольную книгу, где всё описано более подробно "Кормен, Т., Лейзерсон, Ч., Ривест, Р., Штайн, К. Глава 6. Пирамидальная сортировка // Алгоритмы: построение и анализ"):
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 - это функция, которая упорядочивает элементы в поддереве кучи:
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. Попробую пояснить почему так.

Например есть цикл:
for (int x = i; x < N; x += step) { ... }
Для него сложность будет O((N-i)/step). Если i=0 и step = 1, то это вырождается просто в O(N).

Для такого цикла:
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-выражения - это выглядит вполне реальным. Возможно подойдут готовые системы для символьных вычислений или можно самому что-то написать.
20 июн 19, 22:57    [21912528]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Ares_ekb
Member

Откуда: Екатеринбург
Сообщений: 1300
Идея всего этого такая... В книге приводится какое-то очень не тривиальное доказательство сложности O(N). Там делается утверждение
Поскольку число вершин высоты h в куче из n элементов не превышает ceil(n / 2^(h+1)), а высота всей кучи не превышает floor(lg n), то время работы не превышает
и дальше приводится какая-то безумная формула.

Автоматизировать такие рассуждения невозможно. А ту последовательность действий, которую я привёл выше, вполне можно автоматизировать.
20 июн 19, 23:10    [21912534]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Ares_ekb
Member

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

Причём реализация двоичной кучи занимает по идее 1 страницу, а доказательств там больше чем на 20 страниц. И это даже без доказательства сложности алгоритма. Это показывает на сколько всё сложно с формальными методами. На практике для произвольных алгоритмов реально использовать только какие-то эвристики, которые описывал выше.
21 июн 19, 08:38    [21912604]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
kealon(Ruslan)
Member

Откуда: Нижневартовск
Сообщений: 5107
Ares_ekb,

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

Судя по всему, даже со специализированным языком "с подсказками" и частично работающее, в общем виде реально тянет на RocketScience
21 июн 19, 09:38    [21912658]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
kealon(Ruslan)
Member

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

Причём реализация двоичной кучи занимает по идее 1 страницу, а доказательств там больше чем на 20 страниц. И это даже без доказательства сложности алгоритма. Это показывает на сколько всё сложно с формальными методами. На практике для произвольных алгоритмов реально использовать только какие-то эвристики, которые описывал выше.
я так подозреваю, что если ты не НАСА, то платить программистам за такую разработку явно перебор :-)
21 июн 19, 09:42    [21912660]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Aklin
Member

Откуда: Прямо сейчас меня здесь нет
Сообщений: 58146
Interloper
Aklin

Слова "неработающего" и "в виде черного ящика" уберите, а так все верно. С чего вы выдумали, что речь идет о неработающих алгоритмах - ума не приложу.
Что касается вида, то он может быть любой, хоть исходный код. Не исходный код какого-то одного конкретного алгоритма: алгоритм оценки должен принимать на вход исходный код любого алгоритма. Для частного случая в виде подмножества алгоритмов, решение, безусловно существует.
С того, что его разработчик не может гарантировать конечность времени исполнения этого алгоритма на допустимых входных данных.
21 июн 19, 12:02    [21912822]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Aklin
Member

Откуда: Прямо сейчас меня здесь нет
Сообщений: 58146
Interloper
Aklin
Это сугубо теоретический вопрос тогда, а не вопрос программирования.

Это вопрос теории алгоритмов, естественно, а не того программирования, которым вы занимаетесь в офисе.
Тогда речь не может идти о том, что на компьютере не хватит памяти, или вообще о количестве запусков.
21 июн 19, 12:03    [21912823]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Dimitry Sibiryakov
Member

Откуда:
Сообщений: 48132
Interloper
Сложность должна быть не точной величиной, а указанием на один из классов сложности.

Тогда вспоминай матан (если, конечно, для тебя это слово не матерное). Степенная функция отличается от линейной и логарифмической. Причём для их различения достаточно трёх точек.
21 июн 19, 13:36    [21912926]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Aklin
Member

Откуда: Прямо сейчас меня здесь нет
Сообщений: 58146
Dimitry Sibiryakov
Причём для их различения достаточно трёх точек.
В указанных ТС пределах делать замеры нельзя, ибо функция может потенциально зависнуть.

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

А доказывать математически он не хочет.
21 июн 19, 13:46    [21912932]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
Ares_ekb
Member

Откуда: Екатеринбург
Сообщений: 1300
kealon(Ruslan)
да, в математическом доказательстве используется сходящаяся геометрическая прогрессия - тынц

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

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

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

kealon(Ruslan)
Судя по всему, даже со специализированным языком "с подсказками" и частично работающее, в общем виде реально тянет на RocketScience
Если полностью формальное доказательство, то да. А если какие-то полуформализованные эвристики по анализу кода, как я описывал, то вполне реально сделать. Хотя даже это вполне потянуло бы на диссертацию :)
21 июн 19, 15:16    [21913055]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
vas0
Member

Откуда: Таможенный союз (Россия, Казахстан)
Сообщений: 1228
Если взять просто быструю сортировку Хоара (QuickSort). Сложность в худшем n^2. Сложность в среднем n*log, да и то сложность в среднем оценивается лишь вероятностно.

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

Оценка по сложности это скорее подсказка, чтобы не попасть с проклятием размерности, а не точная величина.
23 июн 19, 04:19    [21913491]     Ответить | Цитировать Сообщить модератору
 Re: Верификация сложности алгоритма  [new]
SashaMercury
Member

Откуда: Москва
Сообщений: 2653
Interloper
mayton
пропущено...

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

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

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


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

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


Программно проверить? Напишите программу, если хотите программно проверить. Одним из параметров будет функция подозрительная на асимптотику, проведите ряд экспериментов по n, постройте отношение затраченного времени черного ящика и ф. подозрительной на асимптотику, если функция та самая, то в пределе получите константу. Что там как вы говорите алгоритмически неразрешимого? Вам по-моему о чем-то подобном говорили
11 июл 19, 21:27    [21925259]     Ответить | Цитировать Сообщить модератору
Топик располагается на нескольких страницах: Ctrl  назад   1 2 3 4 [5]      все
Все форумы / Программирование Ответить