Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
chukichuki wrote:
> Как вы думаете, решение такой задачи возможно ?
Невозможно теоретически. Данная проблема легко сводится к "проблеме
останова" для машины Тьюринга, которая доказано неразрешима:
1. Предположим, что первый алгоритм вызывает останов МТ.
2. Тогда второй алгоритм для эквивалентности, как минимум, тоже должен
вызывать останов МТ.
3. Определить вызывает ли данный алгоритм останов МТ в общем случае —
невозможно.
Здравствуйте, Cyberax, Вы писали:
C>chukichuki wrote:
>> Как вы думаете, решение такой задачи возможно ?
C>Невозможно теоретически. Данная проблема легко сводится к "проблеме C>останова" для машины Тьюринга, которая доказано неразрешима: C>1. Предположим, что первый алгоритм вызывает останов МТ. C>2. Тогда второй алгоритм для эквивалентности, как минимум, тоже должен C>вызывать останов МТ. C>3. Определить вызывает ли данный алгоритм останов МТ в общем случае — C>невозможно.
Доказательство совершенно некорректно. Из того, что в обоих случаях невозможно определить останов само по себе не следует, что невозможно доказать эквивалентность алгоритмов, работающих за конечное время. Чтобы убедиться в некорректности твоего "доказательства", достаточно ограничить множество алгоритмов, эквивалентность которых предполагается доказывать, таким образом, чтобы они завершались за конечное время (что, кстати, вполне разумно ). И сопоставить с твоими выкладками, начав со слова "предположим".
Здравствуйте, Gaperton, Вы писали:
G>Доказательство совершенно некорректно. Из того, что в обоих случаях невозможно определить останов само по себе не следует, что невозможно доказать эквивалентность алгоритмов, работающих за конечное время. Чтобы убедиться в некорректности твоего "доказательства", достаточно ограничить множество алгоритмов, эквивалентность которых предполагается доказывать, таким образом, чтобы они завершались за конечное время (что, кстати, вполне разумно ). И сопоставить с твоими выкладками, начав со слова "предположим".
В постановке задачи не было слова "конечное" время. То есть алгоритм _может_ зациклиться.
Чтобы показать, что алгоритмы эквивалентны нужно доказать, что цикл в алгоритме "B" когда-нибудь закончится. А этого сделать нельзя в общем случае.
Даже дополнительное условие конечности времени выполнения не поможет. Строим пример: алгоритмы принимают на вход массивы чисел, на выходе — тоже массивы.
1. Алгоритм "А" — сортивка пузырьком.
2. Алгоритм "Б":
Для доказательства эквивалентности вам придется доказать теорему Ферма Вместо теоремы Ферма можно поставить любое другое утверждение, неразрешимое в данной аксиоматике (а они точно будут).
Здравствуйте, Cyberax, Вы писали:
C>chukichuki wrote:
>> Как вы думаете, решение такой задачи возможно ?
C>Невозможно теоретически. Данная проблема легко сводится к "проблеме C>останова" для машины Тьюринга
Логично. А если упростить задачу. Определять эквивалентность алгоритмов не по выполняемой в конечном итоге операции,
а по соотношению вход/выход. т.е. по некоторому обощенному выражению, которое показало бы как выходные данные
зависят от входных, игнорируя особенности самих алгоритмов. Тут вроде фундаментальных заковырок нет.
Определение такой эквивалентности возможно ? И если возможно, то хотелось бы услышать ваши предложения по поводу
решения такой задачи.
Здравствуйте, chukichuki, Вы писали:
C>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Технология доказательств эквивалентности или других свойств алгоритмов уже давно существует. Это одно из основных приложений декларативнрого программирования. Например, доказательство корректности qsort я видел своими глазами Разумеется, это происходит не полностью автоматически (кроме совсем простых случаев) — надо все-таки формально описать алгоритм доказательства. См., например, http://coq.inria.fr/
Здравствуйте, 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:
> Справедливости ради, ты все-таки не доказал этим ничего. Поскольку > теорема Ферма разрешима, то нет никаких оснований считать, что не > существует алгоритма, который мог бы ее доказать. Есть теоремы, > которые невозможно ни доказать, ни опровергнуть, но их еще надо бы > свести к какому-нибудь алгоритму на числах (как в случае т. Ферма).
Теорема Ферма требует достаточно широкой аксиоматики, которой скорее
всего не будет в "доказывателе" алгоритмов.
Здравствуйте, Cyberax, Вы писали:
C>Теорема Ферма требует достаточно широкой аксиоматики, которой скорее C>всего не будет в "доказывателе" алгоритмов.
"Скорее всего" — это к физикам. Существует же конструктивистское (или даже интуиционистское) направление в математике, где работают только с объектами, которые можно получить за конечное число шагов, и ничего.
C>Ну и уж если вам так хочется, то можно взять какую-нибудь другую C>проблему из теории чисел, например, гипотезу Гольдбаха: C>http://en.wikipedia.org/wiki/Goldbach%27s_conjecture
Опять же, нет никаких оснований полагать, что решатель не сможет доказать эту гипотезу.
chukichuki wrote:
> C>Невозможно теоретически. Данная проблема легко сводится к "проблеме > C>останова" для машины Тьюринга > Логично. А если упростить задачу. Определять эквивалентность > алгоритмов не по выполняемой в конечном итоге операции, > а по соотношению вход/выход. т.е. по некоторому обощенному выражению, > которое показало бы как выходные данные > зависят от входных, игнорируя особенности самих алгоритмов.Тут вроде > фундаментальных заковырок нет.
Есть одна — необходимо поставить дополнительное условие, что существуют
и известны такие наборы входных данных, что алгоритмы проходят через все
возможные комбинации ветвлений. Тогда задача установки эквивалентности
будет разрешима (хотя надо подумать), но такое условие слишком сильно.
Здравствуйте, Cyberax, Вы писали:
C>Есть одна — необходимо поставить дополнительное условие, что существуют C>и известны такие наборы входных данных, что алгоритмы проходят через все C>возможные комбинации ветвлений. Тогда задача установки эквивалентности C>будет разрешима (хотя надо подумать), но такое условие слишком сильно.
Вряд ли. Разве что, если есть ограничение сверху на кол-во состояний. Тогда можно их просто тупо перебрать.
Quintanar wrote:
> 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>А вдруг не сможет?
А вдруг дедушка — это бабушка. Приведите доказательство, что не сможет.
Здравствуйте, chukichuki, Вы писали:
C>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов.
Пузырек и qsort не эквивалентны Это два разных алгоритма, которые выполняют разное количество разных операций. Например, они будут работать разное время, а это может быть критично (например, кто-то использует сортировку для задержки).
C> Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Сформулируй получше, потому что в такой формулировке, как тебе показали, это невозможно. Вернее, есть только одно решение — сравнить машинные коды на полную идентичность (не считая адресов).
Здравствуйте, chukichuki, Вы писали:
C>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Например, cортировку некоторого массива. Первый алгоритм выполняет сортировку методом "пузырька", второй — быстрой сортировкой (qsort). Алгоритмы записаны на некотором (любом) императивном языке программирования и оформленны в виде подпрограмм, которым на вход поступает массив из n элементов, а на выходе получается массив из n отсоритированных в соотвествии с заданным критерием элементов. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Правильно ли я понял — машина должна сам разрулить, что делают алгоритмы и сказать, что да, они делают одно и тоже (если это так)?
). И сопоставить с твоими выкладками, начав со слова "предположим".
Вместо теоремы Ферма можно поставить любое другое утверждение, неразрешимое в данной аксиоматике (а они точно будут).
