Здравствуйте, chukichuki, Вы писали:

C>Представим ситуацию. Существует два алгоритма, описывающих по сути одну и ту же операцию. Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?

Технология доказательств эквивалентности или других свойств алгоритмов уже давно существует. Это одно из основных приложений декларативнрого программирования. Например, доказательство корректности qsort я видел своими глазами Разумеется, это происходит не полностью автоматически (кроме совсем простых случаев) — надо все-таки формально описать алгоритм доказательства. См., например, http://coq.inria.fr/