Здравствуйте, Кодёнок, Вы писали:
Кё>Предположим, сортировку используют для ЗАДЕРЖКИ, вместо пустого цикла. В этом случае они вдруг становятся неэквивалентны. Улавливаешь? эквивалентность/неэквивалентность алгоритмов зависит не только от них самих.
Кё>Другой пример. Эвивалентны ли алгоритмы BitBlt и AlphaBlend? Вообще — нет. Но если они используются для вывода полностью непрозрачной картинки с неважно какой скоростью — да.
Кё>Взаимозаменяемы ли миникувалда и топор? Если забивать гвозди — да, если рубить деревья — нет. И так далее.
Ты манипулируешь понятием алгоритма, как-будто у него нет определения (эквивалентность зависит от цели применения и т.д.). На самом деле в теории алгоритмов есть строгое понятие алгоритма в терминах машины Тьюринга (http://en.wikipedia.org/wiki/Church-Turing_thesis). И в такой постановке задача эквивалентности алгоритмов алгоритмически неразрешима.
chukichuki wrote:
> Как вы думаете, решение такой задачи возможно ?
Невозможно теоретически. Данная проблема легко сводится к "проблеме
останова" для машины Тьюринга, которая доказано неразрешима:
1. Предположим, что первый алгоритм вызывает останов МТ.
2. Тогда второй алгоритм для эквивалентности, как минимум, тоже должен
вызывать останов МТ.
3. Определить вызывает ли данный алгоритм останов МТ в общем случае —
невозможно.
Здравствуйте, Кодёнок, Вы писали: Кё>А я и не говорю о теоретической возможности построить для машины Тьюринга алгоритм определения эквивалентности алгоритмов (тоже наверное для машины Тьюринга которой не существует). Я о возможной реализации.
Кстати, очень точное замечание. Многие образованные разработчики не берутся за некоторые задачи, зная их теоретическую неразрешимость. В частности, за проблему останова.
Тем не менее, нельзя забывать о том, что машина Тьюринга — суть математическая абстракция. Она не может существовать в природе. Мы работаем с ограниченными машинами. И для них можно решить многие неразрешимые задачи. В частности, проблема останова легко разрешима для машины с конечным состоянием: достаточно исполнять программу на второй машине вдвое быстрее и на каждом такте сравнивать состояния. Если состояния совпали — значит программа вошла в бесконечный цикл (в силу детерминированности автомата). Для такой системы мы получим либо останов, либо цикл. На практике держать под рукой еще один синхронный пентиум 4 никто не будет, да и состояние машины (с учетом размера винта) позволяет писать циклы с неприлично большой длиной. Но для маленьких машин (например, для вычислений в рамках одного листа Excel) задача останова решается на раз-два.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, chukichuki, Вы писали:
C>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Технология доказательств эквивалентности или других свойств алгоритмов уже давно существует. Это одно из основных приложений декларативнрого программирования. Например, доказательство корректности qsort я видел своими глазами Разумеется, это происходит не полностью автоматически (кроме совсем простых случаев) — надо все-таки формально описать алгоритм доказательства. См., например, http://coq.inria.fr/
Здравствуйте, Privalov, Вы писали:
P>Почему? Они выполняют одну и ту же работу. Если в программе поменять сортировку пузырьком на быструю, это скажется только на производительности, но не на функциональности. Так что они очень даже эквивалентны. Другое дело, что эти алгоритмы не идентичны.
Предположим, сортировку используют для ЗАДЕРЖКИ, вместо пустого цикла. В этом случае они вдруг становятся неэквивалентны. Улавливаешь? эквивалентность/неэквивалентность алгоритмов зависит не только от них самих.
Другой пример. Эвивалентны ли алгоритмы BitBlt и AlphaBlend? Вообще — нет. Но если они используются для вывода полностью непрозрачной картинки с неважно какой скоростью — да.
Взаимозаменяемы ли миникувалда и топор? Если забивать гвозди — да, если рубить деревья — нет. И так далее.
Здравствуйте, Glоbus, Вы писали:
G>Думается мне, это нереально, потому что машина не знает — что такое сортировки, да и вообдще что такое алгоритмы. Длятого, чтобы понять, что делает алгоритм, нужно обладать дополнительными знаниями — например значть что такое сортировка.
Inductive lelistA (a:A) : list A -> Prop :=
| nil_leA : lelistA a nil
| cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l).
Hint Constructors lelistA.
В соседних модулях есть определение перестановки списка, сортировки кучей и того, что heapsortом из любого списка можно получить его перестановку, являющаяся отсортированным списком.
Здравствуйте, Gaperton, Вы писали:
G>Доказательство совершенно некорректно. Из того, что в обоих случаях невозможно определить останов само по себе не следует, что невозможно доказать эквивалентность алгоритмов, работающих за конечное время. Чтобы убедиться в некорректности твоего "доказательства", достаточно ограничить множество алгоритмов, эквивалентность которых предполагается доказывать, таким образом, чтобы они завершались за конечное время (что, кстати, вполне разумно ). И сопоставить с твоими выкладками, начав со слова "предположим".
В постановке задачи не было слова "конечное" время. То есть алгоритм _может_ зациклиться.
Чтобы показать, что алгоритмы эквивалентны нужно доказать, что цикл в алгоритме "B" когда-нибудь закончится. А этого сделать нельзя в общем случае.
Даже дополнительное условие конечности времени выполнения не поможет. Строим пример: алгоритмы принимают на вход массивы чисел, на выходе — тоже массивы.
1. Алгоритм "А" — сортивка пузырьком.
2. Алгоритм "Б":
Для доказательства эквивалентности вам придется доказать теорему Ферма Вместо теоремы Ферма можно поставить любое другое утверждение, неразрешимое в данной аксиоматике (а они точно будут).
Здравствуйте, Cyberax, Вы писали:
C>С теоремой Ферма — доказательства недоказуемости пока нет. Можно взять C>другое утверждение, уже с доказаной недоказуемостью.
Да, такие утверждения бывают. Более того, у меня в лекциях где-то есть конструктивное доказательство теоремы Гёделя о неполноте. Пользуясь им можно таких утверждений пачку составить.
Но и человек такое утверждения не сможет доказать (важное замчание: оставаясь в пределах тех же аксиом, т.е в пределах той же теории!). Если я правильно понимаю, можно брать подобное утверждение и добавлять его как новую аксиому (а можно брать отрицание этого утверждения) и получать более богатую, непротиворечивую теорию.
(собственно, претензия к Пенроузу именно насчет этого и была — он использовал "внешние" аксиомы, т.е по сути брал более богатую теорию и доказывал в ней, а затем переносил утверждение обратно в "меньшую" теорию).
Так что пока что я не понял твоего доказательства, что не существует универсального решателя (эквивалентного "математику").
Эквивалетность определим как совпадение множеств доказанных утверждений математика М(Т) и решателя Р(Т) для любой теории Т (набор аксиом).
Здравствуйте, chukichuki, Вы писали:
C>Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Эта задача относится к категории halting-problem (проблема остановки) машин Тьюринга.
wikipedia.ru:
При обсуждении машины Тьюринга выделяют такое понятие, как проблема остановки машины Тьюринга. Проблема формулируется следующим образом: имея таблицу состояний машины Тьюринга, мы не можем с уверенностью сказать — остановит ли данная машина свою работу, или нет. Тьюринг доказал, что эта задача является неразрешимой. Чёткий ответ на этот вопрос возможен только в двух вырожденных случаях — когда в машине не объявлено ни одного конечного состояния, либо, когда все состояния машины Тьюринга являются конечными.
См. в частности теорему Rice-Myhill-Shapiro (не знаю как правильно товарищей обозвать, кроме последнего конечно).
Одно из следствий таково:
Не существует такой машины (т.е. алгоритма) которая всегда правильно может определить что входной язык данной конкретной машины Тьюринга (твоя функция например) имеет какое-то определнное нетривиальное свойство — например выполняет одинаковую задачу (имеется ввиду что мы знаем что это означает).
Я конечно могу ошибаться в проекции абстракции на конкретное описание задачи но это по-моему оно.
Здравствуйте, Cyberax, Вы писали:
C>chukichuki wrote:
>> Как вы думаете, решение такой задачи возможно ?
C>Невозможно теоретически. Данная проблема легко сводится к "проблеме C>останова" для машины Тьюринга, которая доказано неразрешима: C>1. Предположим, что первый алгоритм вызывает останов МТ. C>2. Тогда второй алгоритм для эквивалентности, как минимум, тоже должен C>вызывать останов МТ. C>3. Определить вызывает ли данный алгоритм останов МТ в общем случае — C>невозможно.
Доказательство совершенно некорректно. Из того, что в обоих случаях невозможно определить останов само по себе не следует, что невозможно доказать эквивалентность алгоритмов, работающих за конечное время. Чтобы убедиться в некорректности твоего "доказательства", достаточно ограничить множество алгоритмов, эквивалентность которых предполагается доказывать, таким образом, чтобы они завершались за конечное время (что, кстати, вполне разумно ). И сопоставить с твоими выкладками, начав со слова "предположим".
Здравствуйте, Cyberax, Вы писали:
C>Теорема Ферма требует достаточно широкой аксиоматики, которой скорее C>всего не будет в "доказывателе" алгоритмов.
"Скорее всего" — это к физикам. Существует же конструктивистское (или даже интуиционистское) направление в математике, где работают только с объектами, которые можно получить за конечное число шагов, и ничего.
C>Ну и уж если вам так хочется, то можно взять какую-нибудь другую C>проблему из теории чисел, например, гипотезу Гольдбаха: C>http://en.wikipedia.org/wiki/Goldbach%27s_conjecture
Опять же, нет никаких оснований полагать, что решатель не сможет доказать эту гипотезу.
Здравствуйте, Cyberax, Вы писали:
C>Quintanar wrote:
>> C>Ну и уж если вам так хочется, то можно взять какую-нибудь другую >> C>проблему из теории чисел, например, гипотезу Гольдбаха: >> C>http://en.wikipedia.org/wiki/Goldbach%27s_conjecture >> Опять же, нет никаких оснований полагать, что решатель не сможет >> доказать эту гипотезу.
C>А вдруг не сможет?
А вдруг дедушка — это бабушка. Приведите доказательство, что не сможет.
Здравствуйте, Кодёнок, Вы писали:
P>>Почему? Они выполняют одну и ту же работу. Если в программе поменять сортировку пузырьком на быструю, это скажется только на производительности, но не на функциональности. Так что они очень даже эквивалентны. Другое дело, что эти алгоритмы не идентичны.
Кё>Предположим, сортировку используют для ЗАДЕРЖКИ, вместо пустого цикла. В этом случае они вдруг становятся неэквивалентны. Улавливаешь? эквивалентность/неэквивалентность алгоритмов зависит не только от них самих.
Кё>Другой пример. Эвивалентны ли алгоритмы BitBlt и AlphaBlend? Вообще — нет. Но если они используются для вывода полностью непрозрачной картинки с неважно какой скоростью — да.
Кё>Взаимозаменяемы ли миникувалда и топор? Если забивать гвозди — да, если рубить деревья — нет. И так далее.
Что означает, что решение такого важного вопроса нужно начать с определения понятия "эквивалентность".
Здравствуйте, WFrag, Вы писали:
P>>Отсутствие результата — тоже результат.
WF>Фишка в том, что ты можешь определить, когда две произвольные программы — неэквивалентны, но не можешь (вернее, можешь, но не всегда ) определить когда они эквивалентны.
Некий слепоглухонемой папуас, который даже не может отличить, работает компьютер или нет, какие алгоритмы не выполняй, будет получать одинаковые результаты. Все алгоритмы эквивалентны
Кё>Некий слепоглухонемой папуас, который даже не может отличить, работает компьютер или нет, какие алгоритмы не выполняй, будет получать одинаковые результаты. Все алгоритмы эквивалентны
Этот самый папуас не знает ничего ни о компьютерах, ни об алгоритмах. Алгоритмы не существуют.
Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Здравствуйте, Cyberax, Вы писали:
C>chukichuki wrote:
>> Как вы думаете, решение такой задачи возможно ?
C>Невозможно теоретически. Данная проблема легко сводится к "проблеме C>останова" для машины Тьюринга
Логично. А если упростить задачу. Определять эквивалентность алгоритмов не по выполняемой в конечном итоге операции,
а по соотношению вход/выход. т.е. по некоторому обощенному выражению, которое показало бы как выходные данные
зависят от входных, игнорируя особенности самих алгоритмов. Тут вроде фундаментальных заковырок нет.
Определение такой эквивалентности возможно ? И если возможно, то хотелось бы услышать ваши предложения по поводу
решения такой задачи.
Здравствуйте, mihoshi, Вы писали:
M>Технология доказательств эквивалентности или других свойств алгоритмов уже давно существует. Это одно из основных приложений декларативнрого программирования. Например, доказательство корректности qsort я видел своими глазами Разумеется, это происходит не полностью автоматически (кроме совсем простых случаев) — надо все-таки формально описать алгоритм доказательства. См., например, http://coq.inria.fr/
Да, я знаю о таких разработках. В приницпе, сам читал в какой-то книжке доказательство корректности программы вычисляющей факториал средствами исчисления программ Хоара и Флойда (аксиоматическая семантика). Однако ход рассуждений там, на сколько я представляю, не алгоритмтизирован. Т.е. процесс доказательства во многом творческий (что, кстати, видимо лишний раз подтверждает идеи Тьюринга).
Здравствуйте, mihoshi, Вы писали:
M>Технология доказательств эквивалентности или других свойств алгоритмов уже давно существует. Это одно из основных приложений декларативнрого программирования. Например, доказательство корректности qsort я видел своими глазами Разумеется, это происходит не полностью автоматически (кроме совсем простых случаев) — надо все-таки формально описать алгоритм доказательства. См., например, http://coq.inria.fr/
Преобразование алгоритма в эквивалентный — есть такое дело. Но сравнить 2 данных алгоритма на эквивалентность — задача неразрешимая (как и написал Cyberax). Сейчас не располагаю доказательством, но как новичок в функциональном программировании, привык некоторым источникам верить на слово. Пример:
Another problem is that equality is a meaningless idea for some data types. For example, comparing functions for equality is a computationally intractable problem.
Здравствуйте, Cyberax, Вы писали:
C>Даже дополнительное условие конечности времени выполнения не поможет. Строим пример: алгоритмы принимают на вход массивы чисел, на выходе — тоже массивы. C>1. Алгоритм "А" — сортивка пузырьком. C>2. Алгоритм "Б": C>
C>Для доказательства эквивалентности вам придется доказать теорему Ферма Вместо теоремы Ферма можно поставить любое другое утверждение, неразрешимое в данной аксиоматике (а они точно будут).
Справедливости ради, ты все-таки не доказал этим ничего. Поскольку теорема Ферма разрешима, то нет никаких оснований считать, что не существует алгоритма, который мог бы ее доказать. Есть теоремы, которые невозможно ни доказать, ни опровергнуть, но их еще надо бы свести к какому-нибудь алгоритму на числах (как в случае т. Ферма).
Согласен с мнением большинства — задача в общем случае не разрешима.
Возможно, для некоторых типов алгоритмов, эти алг. можно сводить к какому-то языку (автоматически), который имеет меньше конструкций, чем обычные языки. Скажем, не имеет циклов, а их реализация основывается на рекурсии или ещё что-нибудь.
Возможно, тогда будет легче построить и автомат. определение эквивал. на этом языке
Quintanar wrote:
> Справедливости ради, ты все-таки не доказал этим ничего. Поскольку > теорема Ферма разрешима, то нет никаких оснований считать, что не > существует алгоритма, который мог бы ее доказать. Есть теоремы, > которые невозможно ни доказать, ни опровергнуть, но их еще надо бы > свести к какому-нибудь алгоритму на числах (как в случае т. Ферма).
Теорема Ферма требует достаточно широкой аксиоматики, которой скорее
всего не будет в "доказывателе" алгоритмов.
chukichuki wrote:
> C>Невозможно теоретически. Данная проблема легко сводится к "проблеме > C>останова" для машины Тьюринга > Логично. А если упростить задачу. Определять эквивалентность > алгоритмов не по выполняемой в конечном итоге операции, > а по соотношению вход/выход. т.е. по некоторому обощенному выражению, > которое показало бы как выходные данные > зависят от входных, игнорируя особенности самих алгоритмов.Тут вроде > фундаментальных заковырок нет.
Есть одна — необходимо поставить дополнительное условие, что существуют
и известны такие наборы входных данных, что алгоритмы проходят через все
возможные комбинации ветвлений. Тогда задача установки эквивалентности
будет разрешима (хотя надо подумать), но такое условие слишком сильно.
Здравствуйте, Cyberax, Вы писали:
C>Есть одна — необходимо поставить дополнительное условие, что существуют C>и известны такие наборы входных данных, что алгоритмы проходят через все C>возможные комбинации ветвлений. Тогда задача установки эквивалентности C>будет разрешима (хотя надо подумать), но такое условие слишком сильно.
Вряд ли. Разве что, если есть ограничение сверху на кол-во состояний. Тогда можно их просто тупо перебрать.
Quintanar wrote:
> C>Ну и уж если вам так хочется, то можно взять какую-нибудь другую > C>проблему из теории чисел, например, гипотезу Гольдбаха: > C>http://en.wikipedia.org/wiki/Goldbach%27s_conjecture > Опять же, нет никаких оснований полагать, что решатель не сможет > доказать эту гипотезу.
Здравствуйте, chukichuki, Вы писали:
C>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов.
Пузырек и qsort не эквивалентны Это два разных алгоритма, которые выполняют разное количество разных операций. Например, они будут работать разное время, а это может быть критично (например, кто-то использует сортировку для задержки).
C> Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Сформулируй получше, потому что в такой формулировке, как тебе показали, это невозможно. Вернее, есть только одно решение — сравнить машинные коды на полную идентичность (не считая адресов).
Здравствуйте, chukichuki, Вы писали:
C>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Правильно ли я понял — машина должна сам разрулить, что делают алгоритмы и сказать, что да, они делают одно и тоже (если это так)?
Здравствуйте, Кодёнок, Вы писали:
Кё>Пузырек и qsort не эквивалентны Это два разных алгоритма, которые выполняют разное количество разных операций. Например, они будут работать разное время, а это может быть критично (например, кто-то использует сортировку для задержки).
Почему? Они выполняют одну и ту же работу. Если в программе поменять сортировку пузырьком на быструю, это скажется только на производительности, но не на функциональности. Так что они очень даже эквивалентны. Другое дело, что эти алгоритмы не идентичны.
Quintanar wrote:
>>> C>Ну и уж если вам так хочется, то можно взять какую-нибудь другую >>> C>проблему из теории чисел, например, гипотезу Гольдбаха: >>> C>http://en.wikipedia.org/wiki/Goldbach%27s_conjecture >>> Опять же, нет никаких оснований полагать, что решатель не сможет >>> доказать эту гипотезу. > C>А вдруг не сможет? > А вдруг дедушка — это бабушка. Приведите доказательство, что не сможет.
В достаточно сложной теории существуют утверждения, такие, что не может
быть доказана за конечное число шагов их верность или ложность.
То есть если наш решатель работает в рамках арифметики Пеано, в которой
можно сформулировать теорему Ферма, то он вряд ли найдет ее
доказательство — это требует привлечения дополнительных аксиоматик.
Здравствуйте, Glоbus, Вы писали:
G>Здравствуйте, chukichuki, Вы писали:
C>>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
G>Правильно ли я понял — машина должна сам разрулить, что делают алгоритмы и сказать, что да, они делают одно и тоже (если это так)?
Ну в идеале (недостижимом за конечное время — да !
Здравствуйте, Cyberax, Вы писали:
C>В достаточно сложной теории существуют утверждения, такие, что не может C>быть доказана за конечное число шагов их верность или ложность.
C>То есть если наш решатель работает в рамках арифметики Пеано, в которой C>можно сформулировать теорему Ферма, то он вряд ли найдет ее C>доказательство — это требует привлечения дополнительных аксиоматик.
А можно ссылочку на источник подобных утверждений?
Получается, что теорема Ферма в арифметике Пеано недоказуема?
Здравствуйте, Кодёнок, Вы писали:
Кё>Предположим, сортировку используют для ЗАДЕРЖКИ, вместо пустого цикла. В этом случае они вдруг становятся неэквивалентны. Улавливаешь? эквивалентность/неэквивалентность алгоритмов зависит не только от них самих.
Почему? Разве эквивалентность алгоритмов зависит от того, где и как их используют? Если, как ты предлагаешь, использовать сортировку для задержки, она от этого в генератор случайных чисел не превратится.
Кё>Другой пример. Эвивалентны ли алгоритмы BitBlt и AlphaBlend? Вообще — нет. Но если они используются для вывода полностью непрозрачной картинки с неважно какой скоростью — да.
В обоих приведенных тобой примерах речь идет не об алгоритмах как таковых, а об их использовании.
Кё>Взаимозаменяемы ли миникувалда и топор? Если забивать гвозди — да, если рубить деревья — нет. И так далее.
И здесь речь идет о применении инструментов. Кстати, в этом случае ответ зависит еще и от параметров самих инструментов (размеры, масса и т. д.)
Здравствуйте, Gleb Alexeev, Вы писали:
GA>Ты манипулируешь понятием алгоритма, как-будто у него нет определения (эквивалентность зависит от цели применения и т.д.). На самом деле в теории алгоритмов есть строгое понятие алгоритма в терминах машины Тьюринга (http://en.wikipedia.org/wiki/Church-Turing_thesis). И в такой постановке задача эквивалентности алгоритмов алгоритмически неразрешима.
А я и не говорю о теоретической возможности построить для машины Тьюринга алгоритм определения эквивалентности алгоритмов (тоже наверное для машины Тьюринга которой не существует). Я о возможной реализации.
У нас же всегда работает реальная программа на реальной ЭВМ, в некотором окружении. Окружение, в том числе операционная система, может влиять на выполнение программы. Два разных алгоритма очевидно будут вызывать множество разных эффектов. Какие-то эффекты будут вызываться обоими алгоритмами, какие-то только одним из них. Какие из эффектов будут важны — зависит от _нашей_ цели! Можно ли два немного отличающихся эффекта счесть одним и тем же — опять же зависит от нас.
WFrag wrote:
> C>В достаточно сложной теории существуют утверждения, такие, что не может > C>быть доказана за конечное число шагов их верность или ложность. > > C>То есть если наш решатель работает в рамках арифметики Пеано, в которой > C>можно сформулировать теорему Ферма, то он вряд ли найдет ее > C>доказательство — это требует привлечения дополнительных аксиоматик. > А можно ссылочку на источник подобных утверждений?
Первое утверждение — теорема Геделя о неполноте, смотрится в учебнике
мат. логики.
> Получается, что теорема Ферма в арифметике Пеано недоказуема?
Да, _исключительно_ в рамках арифметики Пеано она, скорее всего, не
доказуема — известное доказательство требует привлечения кучи других
аксиоматик.
Здравствуйте, Privalov, Вы писали:
P>Можно ли считать 2 алгоритма эквивалентными, если, получая на входе одинаковые данные, они возвращают одинаковые результаты?
Почему нет? Однако можно определить "эквивалентность" и так:
Две программы Тьюринга (не "алгоритмы", дабы избежать тонкости связанной с определением понятия "алгоритм") считаются эквивалентными, если для любого входного кортежа обе программы завершаются за одинаковое время (или обе зацикливаются) и выдают одинаковый результат.
В таком случае задача "неэквивалентности" — разрешима. Можно написать программу (для МТ), которая получая на вход код двух программ и остановится если они неэквивалентны и зациклится — если эквивалентны.
Однако обратная задача ("эквивалентности") же — неразрешима, хотя с ходу доказательство я, наверное, и не придумаю. Видимо, надо как-то свести задачу к известной задаче разрешимости (например, к задача об остановке).
Privalov wrote:
> WF>Что означает, что решение такого важного вопроса нужно начать с > определения понятия "эквивалентность". > Можно ли считать 2 алгоритма эквивалентными, если, получая на входе > одинаковые данные, они возвращают одинаковые результаты?
Да. Хотя они еще могут и ничего не возвращать (т.е. зациклиться).
Здравствуйте, Privalov, Вы писали:
WF>>Что означает, что решение такого важного вопроса нужно начать с определения понятия "эквивалентность".
P>Можно ли считать 2 алгоритма эквивалентными, если, получая на входе одинаковые данные, они возвращают одинаковые результаты?
А что такое результаты? Тепловыделение и потеря времени — тоже результаты. Для разных алгоритмов разные. Даже для одного алгоритма, выполненного два раза, могут быть разными. Можно ли раз и навсегда выработать правило, какие полученные эффекты включать в "результаты", а какие — нет?
Здравствуйте, WFrag, Вы писали:
Кё>>Взаимозаменяемы ли миникувалда и топор? Если забивать гвозди — да, если рубить деревья — нет. И так далее.
WF>Что означает, что решение такого важного вопроса нужно начать с определения понятия "эквивалентность".
Не нужно, достаточно интуитивного понимания. Дело в другом. См. ответ Глебу. Каждое реальное выполнение программы (на реальной ЭВМ) вызывает бесконечное множество эффектов, от очень заметных до совсем незаметных (выделение тепла, потеря тобой 1 минуты жизни на ожидание и т.д.). Человек может каким угодно образом решить, были два набора эффектов для него одним и тем же результатом, или разными результатами. Два разных человека решат по разному.
Здравствуйте, Кодёнок, Вы писали:
Кё>>>Взаимозаменяемы ли миникувалда и топор? Если забивать гвозди — да, если рубить деревья — нет. И так далее.
WF>>Что означает, что решение такого важного вопроса нужно начать с определения понятия "эквивалентность".
Кё>Не нужно, достаточно интуитивного понимания. Дело в другом. См. ответ Глебу. Каждое реальное выполнение программы (на реальной ЭВМ) вызывает бесконечное множество эффектов, от очень заметных до совсем незаметных (выделение тепла, потеря тобой 1 минуты жизни на ожидание и т.д.). Человек может каким угодно образом решить, были два набора эффектов для него одним и тем же результатом, или разными результатами. Два разных человека решат по разному.
Собственно, ты сам себе и противоречишь. Второе предложение собственно и обосновывает, почему нужно строго определять. У каждого — свое интуитивное понимание, не формализовав его говорить о задаче — бессмысленно. Потому что разные поределения будут давать разные задачи. Например, меня бы устроила эквивалентность данная мной в соседней ветке (по результату + времени), с условием, что МТ заменить на что-нибудь более близкое к реалиям (хоть бы даже и на JVM ).
Здравствуйте, WFrag, Вы писали:
WF>Две программы Тьюринга (не "алгоритмы", дабы избежать тонкости связанной с определением понятия "алгоритм") считаются эквивалентными, если для любого входного кортежа обе программы завершаются за одинаковое время (или обе зацикливаются) и выдают одинаковый результат.
Я думаю одинаковое время выполнения для эквивалентности не столь критично. Его можно опустить.
WF>В таком случае задача "неэквивалентности" — разрешима. Можно написать программу (для МТ), которая получая на вход код двух программ и остановится если они неэквивалентны и зациклится — если эквивалентны.
WF>Однако обратная задача ("эквивалентности") же — неразрешима, хотя с ходу доказательство я, наверное, и не придумаю. Видимо, надо как-то свести задачу к известной задаче разрешимости (например, к задача об остановке).
Я совсем ничего не понял. Разве не (не эквиваленты) != эквиваленты ? В чем разница между задачами "неэквивалентости" и "эквивалентности" ?
Здравствуйте, WFrag, Вы писали:
WF>Однако обратная задача ("эквивалентности") же — неразрешима, хотя с ходу доказательство я, наверное, и не придумаю. Видимо, надо как-то свести задачу к известной задаче разрешимости (например, к задача об остановке).
О! Придумал доказательство!
Пусть у нас есть МТ, которая на вход получает две программы МТ (способ кодирования их несущественнен) и выдает 0 если они неэквивалентны, 1 — если да (назовем ее Э). Посмотрим, как можно свести задачу к задаче остановки (которая, как известно, неразрешима).
Пусть дана программа П и входные данные Д. Построим программу ПД, которая вычисляет П(Д) (т.е это просто композиция двух программ — одна забивает ленту входными данными Д, вторая — просто вычисляет П). Очевидно, что ПД не зависит от входных данных. Т.е она либо останавливается и выдает в точности П(Д), либо зацикливается.
Вычислим Э(ПД, Б), где Б — бесконечный цикл. Если они неэквивалентны, то сущ. входные данные на которых ПД останавливается (так как Б не останавливается при любых входных данных), а значит ПД останавливается везде (так как не зависит от входных данных), а значит П(Д) — останавливается. Если же Э(ПД, Б) выдает 1, то ПД — не останавливается, а значит не останавливается и П(Д)!
Мы решили задачу об остановке -> противоречие. Такого алгорится Э не существует.
Здравствуйте, WFrag, Вы писали:
WF>Две программы Тьюринга (не "алгоритмы", дабы избежать тонкости связанной с определением понятия "алгоритм") считаются эквивалентными, если для любого входного кортежа обе программы завершаются за одинаковое время (или обе зацикливаются) и выдают одинаковый результат.
А зачем добавлять в определение время выполнения? Опять же, в случае сортировки можно подобрать данные так, что и быстрый метод, и пузырек управятся с ними за одинаковое время. При этом оба метода завершаются и выдают одинаковый результат. Ясно, что в общем случае это не так, однако алгоритмы, imho, остаются эквивалентными для внешнего наблюдателя. Кому из программистов не доводилось менять тот же пузырек в пробной версии на быструю сортировку в рабочей? Производительность меняется, функциональность — нет. Т. е. внешний наблюдатель увидит уменьшение (или увеличение) времени выполнения программы, однако не заметит никаких различий в результатах.
Здравствуйте, chukichuki, Вы писали:
C>Я думаю одинаковое время выполнения для эквивалентности не столь критично. Его можно опустить.
Можно.
WF>>В таком случае задача "неэквивалентности" — разрешима. Можно написать программу (для МТ), которая получая на вход код двух программ и остановится если они неэквивалентны и зациклится — если эквивалентны.
WF>>Однако обратная задача ("эквивалентности") же — неразрешима, хотя с ходу доказательство я, наверное, и не придумаю. Видимо, надо как-то свести задачу к известной задаче разрешимости (например, к задача об остановке).
C>Я совсем ничего не понял. Разве не (не эквиваленты) != эквиваленты ? В чем разница между задачами "неэквивалентости" и "эквивалентности" ?
Задача эквивалентности выдает 0 (останавливается), если программы П1 и П2 — эквивалентны (в моем определении, но время, в общем-то, можно опустить — оно не существенно). Иначе она зацикливается. Т.е это программа позволяет определить эквивалентность двух программ.
Задача неэквивалентности выдает 0 (останавливается), если программы П1 и П2 — неэквивалентны. Иначе она зацикливается. Т.е это программа позволяет определить неэквивалентность двух программ.
Это мое определение. На самом деле я немного попутал — в разных топиках у меня разные определения, но в том, на который ты отвечал определения именно такие.
Здравствуйте, Privalov, Вы писали:
P>А зачем добавлять в определение время выполнения? Опять же, в случае сортировки можно подобрать данные так, что и быстрый метод, и пузырек управятся с ними за одинаковое время. При этом оба метода завершаются и выдают одинаковый результат. Ясно, что в общем случае это не так, однако алгоритмы, imho, остаются эквивалентными для внешнего наблюдателя. Кому из программистов не доводилось менять тот же пузырек в пробной версии на быструю сортировку в рабочей? Производительность меняется, функциональность — нет. Т. е. внешний наблюдатель увидит уменьшение (или увеличение) времени выполнения программы, однако не заметит никаких различий в результатах.
Мне так захотелось. Можно и опустить — по сути это ничего не меняет. Просто разные определения понятия "эквивалентность".
Здравствуйте, WFrag, Вы писали:
P>>Можно ли считать 2 алгоритма эквивалентными, если, получая на входе одинаковые данные, они возвращают одинаковые результаты?
WF>Почему нет? Однако можно определить "эквивалентность" и так:
WF>Две программы Тьюринга (не "алгоритмы", дабы избежать тонкости связанной с определением понятия "алгоритм") считаются эквивалентными, если для любого входного кортежа обе программы завершаются за одинаковое время (или обе зацикливаются) и выдают одинаковый результат.
А если они по-разному зацикливаются? Одна постоянно что-нибудь пишет, другая не делает ничего.
Здравствуйте, Privalov, Вы писали:
P>Отсутствие результата — тоже результат.
Фишка в том, что ты можешь определить, когда две произвольные программы — неэквивалентны, но не можешь (вернее, можешь, но не всегда ) определить когда они эквивалентны.
Здравствуйте, Кодёнок, Вы писали:
Кё>А если они по-разному зацикливаются? Одна постоянно что-нибудь пишет, другая не делает ничего.
Да, это интересный вопрос. В моем определении разные "зацикленности" не разделяются, хотя в реальной жизни они могут иметь смысл (вспомним хотя бы Unix-овый yes ). Упущение.
Здравствуйте, WFrag, Вы писали:
Кё>>А если они по-разному зацикливаются? Одна постоянно что-нибудь пишет, другая не делает ничего.
WF>Да, это интересный вопрос. В моем определении разные "зацикленности" не разделяются, хотя в реальной жизни они могут иметь смысл (вспомним хотя бы Unix-овый yes ). Упущение.
Хотя я не прав. Для МТ вообще бессмысленно понятие "постоянно что-то писать" (нет понятия ввода/вывода), поэтому для МТ такое разделение бессмысленно.
Но такое понятие можно ввести — например, разделять "выхлопы" программы специальным символом, т.е считаем, что программа не возвращается и не модифицирует старые данные (котррые до последнего выведенного разделителя). В таком случае возникает еще одно определение "эквивалентности".
Здравствуйте, WFrag, Вы писали:
WF>Собственно, ты сам себе и противоречишь. Второе предложение собственно и обосновывает, почему нужно строго определять. У каждого — свое интуитивное понимание, не формализовав его говорить о задаче — бессмысленно. Потому что разные поределения будут давать разные задачи. Например, меня бы устроила эквивалентность данная мной в соседней ветке (по результату + времени), с условием, что МТ заменить на что-нибудь более близкое к реалиям (хоть бы даже и на JVM ).
Для каждой ситуации будет своё "строгое" определение. Зачем оно нужно тогда? Какое бы строгое определение ты ни дал, мы всегда будем решать какой-то частный случай задачи об эквивалентности. И всегда найдется человек, который вспомнит их практики случай, когда твоё определение эквивалентности не подойдет и придется решать уже другую задачу об эквивалентности.
Так что определяться тут надо с тем, что вы хотите Например, выделить типичные задачи и решить каждую:
1. Эквивалентность = две функции возвращают одно и то же значение от одних и тех же входных данных. Побочные эффекты и время не волнуют.
2. То же, что и п. 1, но оговоренные побочные эффекты должны совпадать. Например, можно принимать во внимание только вызовы функций из DLL. Время не волнует.
3. п.1 + разница по времени выполнения не более N%, либо всегда (при каждом выполнении), либо статистически (в среднем на 1000 выполнений на разных данных, случайных или подобранных).
4. п.2 + время из п.3
Первый пункт наверное самый простой.
Естественно, речь не идет о машине Тьюринга. Она бесполезна. Наши программы либо что-то считают (возвращают результат), либо что-то делают (побочные эффекты). Вот для них и следует решать задачу эквивалентности.
Здравствуйте, Кодёнок, Вы писали:
Кё>Для каждой ситуации будет своё "строгое" определение. Зачем оно нужно тогда? Какое бы строгое определение ты ни дал, мы всегда будем решать какой-то частный случай задачи об эквивалентности. И всегда найдется человек, который вспомнит их практики случай, когда твоё определение эквивалентности не подойдет и придется решать уже другую задачу об эквивалентности.
Кё>Так что определяться тут надо с тем, что вы хотите Например, выделить типичные задачи и решить каждую:
О чем и речь. Потому что я могу ввести такое определение эквивалентности:
П1 и П2 эквивалентны, если за число шагов N (как правило, нас интересует конечное время ) для любого входного кортежа из конечного множества входных данных D (как правило, память у нас ограничена ) они обе остановятся и выдадут одинаковый результат. Эта задача — разрешима.
Значит, для любого N и D эта задача разрешима. Можно бежать писать программу для N=100лет и |D|=1Тб
То есть некой "общей задачи эквивалентности", без строго определения просто не существует! Это разнве задачи и разные же решения. В одном случае задача — разрешима, в другом — нет. Хотя вроде бы "задача" одна и та же — "эквивалентность".
Кё>1. Эквивалентность = две функции возвращают одно и то же значение от одних и тех же входных данных. Побочные эффекты и время не волнуют.
Кё>2. То же, что и п. 1, но оговоренные побочные эффекты должны совпадать. Например, можно принимать во внимание только вызовы функций из DLL. Время не волнует.
Кё>3. п.1 + разница по времени выполнения не более N%, либо всегда (при каждом выполнении), либо статистически (в среднем на 1000 выполнений на разных данных, случайных или подобранных).
Кё>4. п.2 + время из п.3
Кё>Первый пункт наверное самый простой.
Кё>Естественно, речь не идет о машине Тьюринга. Она бесполезна. Наши программы либо что-то считают (возвращают результат), либо что-то делают (побочные эффекты). Вот для них и следует решать задачу эквивалентности.
Почему? Проще свести задачу к МТ и строго ее решить. Как это делается для вывода (простейший побочный эффект) — я показал (как это сделать для ввода — пока не придумал ). Просто для МТ проще некоторые построения производить, не нужно отвлекаться на мелкие несущественные детали (типа тех же вызовов DLL).
Это, конечно, если интересует некий строгий теоретический результат, а не практическое решение (например, как база со всеми существующими программами). В начальной постановке вопрос был именно теоретический.
Здравствуйте, Кодёнок, Вы писали:
WF>>Фишка в том, что ты можешь определить, когда две произвольные программы — неэквивалентны, но не можешь (вернее, можешь, но не всегда ) определить когда они эквивалентны.
Кё>Некий слепоглухонемой папуас, который даже не может отличить, работает компьютер или нет, какие алгоритмы не выполняй, будет получать одинаковые результаты. Все алгоритмы эквивалентны
Правильно. Это я на протяжении многих топиков и говорю. В топике, на который ты отвечал, эквивалентность — введенная мной (хотя опять же, ограничение по времени можно убрать).
Именно для такой задачи получается именно такой результат — озвученный выше.
Здравствуйте, WFrag, Вы писали:
WF>Почему? Проще свести задачу к МТ и строго ее решить. Как это делается для вывода (простейший побочный эффект) — я показал (как это сделать для ввода — пока не придумал ). Просто для МТ проще некоторые построения производить, не нужно отвлекаться на мелкие несущественные детали (типа тех же вызовов DLL).
Единственное, что свести настоящий недетерминизм к МТ у нас не получится. Если начинаем говорить о недетерминированном выполнении программы на, скажем, x86 можно тут же опуститься до уровня квантовой механики, бога, инопланетянах и на этом закончить рассуждения о программировании вообще.
С другой стороны, можно ограничиться псевдо-недетерминизмом — просто очень сложной функцией выбора от большого кортежа входных параметров (например, программа была запущена в такой-то момент, в это время состояние памяти такое-то, состояние процессора такое-то, температура такая-то, и.т.д).
Здравствуйте, Cyberax, Вы писали:
>> Получается, что теорема Ферма в арифметике Пеано недоказуема?
C>Да, _исключительно_ в рамках арифметики Пеано она, скорее всего, не C>доказуема — известное доказательство требует привлечения кучи других C>аксиоматик.
Опять двадцать пять. СКОРЕЕ ВСЕГО — это не аргумент. Приведите полное доказательство этого факта.
Quintanar wrote:
> C>Да, _исключительно_ в рамках арифметики Пеано она, скорее всего, не > C>доказуема — известное доказательство требует привлечения кучи других > C>аксиоматик. > Опять двадцать пять. СКОРЕЕ ВСЕГО — это не аргумент. Приведите полное > доказательство этого факта.
Видел на arxive'е статью, где это человек пытается доказать. Сейчас ищу ее.
Здравствуйте, chukichuki, Вы писали:
C>Здравствуйте, Glоbus, Вы писали:
G>>Здравствуйте, chukichuki, Вы писали:
C>>>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
G>>Правильно ли я понял — машина должна сам разрулить, что делают алгоритмы и сказать, что да, они делают одно и тоже (если это так)?
C>Ну в идеале (недостижимом за конечное время — да !
Думается мне, это нереально, потому что машина не знает — что такое сортировки, да и вообдще что такое алгоритмы. Длятого, чтобы понять, что делает алгоритм, нужно обладать дополнительными знаниями — например значть что такое сортировка.
Здравствуйте, Cyberax, Вы писали:
C>Первое утверждение — теорема Геделя о неполноте, смотрится в учебнике C>мат. логики.
Это я знаю.
C>Да, _исключительно_ в рамках арифметики Пеано она, скорее всего, не C>доказуема — известное доказательство требует привлечения кучи других C>аксиоматик.
Ну и что, что требует? Совершенно необязательно, что они необходимы. Жду доказательства.
WFrag wrote:
> C>Да, _исключительно_ в рамках арифметики Пеано она, скорее всего, не > C>доказуема — известное доказательство требует привлечения кучи других > C>аксиоматик. > Ну и что, что требует? Совершенно необязательно, что они необходимы. > Жду доказательства.
С теоремой Ферма — доказательства недоказуемости пока нет. Можно взять
другое утверждение, уже с доказаной недоказуемостью. Например в теории
графов есть одно такое (вернут мне учебник Непейводы по мат. логике —
скажу).
Здравствуйте, Cyberax, Вы писали:
>> C>С теоремой Ферма — доказательства недоказуемости пока нет. >> Я, вероятно, выпал из контекста, но теорема Ферма доказана.
C>Мы говорим про ее недоказуемость в рамках исключительно аксиоматики C>арифметики Пеано.
Прошу прощения
Возможно — по крайней мере двух этих алгоритмов — но без их трассировки — никак
Опишиите действия человека в данной ситуации — да , он должен знать назначение этих алгоритмов — аналогично и с машиной — она тоже должна знать назначение.
Соответственно если не знать назначение алгоритма — доказать эквивалентость сложнее — и человек не всегда это сможет сделать.
Здравствуйте, Cyberax, Вы писали:
C>Для автоматического доказательства теорем. Используется, например, при C>доказательстве правильности алгоритмов.
C>Естественно, доказывать он умеет далеко не все
Здравствуйте, Sinclair, Вы писали:
S>Но для маленьких машин (например, для вычислений в рамках одного листа Excel) задача останова решается на раз-два.
По моим подсчетам число состояний для одного листа Excel значительно превосходит количество колебаний, совершенных всеми атомами Вселенной за время её существования.
Здравствуйте, Трурль, Вы писали: Т>По моим подсчетам число состояний для одного листа Excel значительно превосходит количество колебаний, совершенных всеми атомами Вселенной за время её существования.
Да. На практике можно даже для листа ексель построить несложный алгоритм, который имеет длину цикла, близкую к полному числу состояний. Естественно, решение проблемы останова в данном случае не будет иметь практического смысла
К счастью, природа этого алгоритма такова, что его построение невозможно выполнить случайно. Подавляющее большинство безостановочных алгоритмов, которые возникают в процессе разработки, имеют намного более короткие циклы.
... << RSDN@Home 1.1.4 stable rev. 510>>
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
которой не существует). Я о возможной реализации.
). И сопоставить с твоими выкладками, начав со слова "предположим".
— да !
