алгоритмическая (не)разрешимость эквивалентности формул

[маткиб]

Интересует алгоритмическая разрешимость/неразрешимость следующих задач:

1) Даны 2 формулы от переменной x, построенные на основе операции суперпозиции из рациональных констант и некоторого базового (стандартного) набора функций, например, x+y, x*y, x/y, exp(x), ln(x), sin(x), cos(x), arctg(x), arcsin(x), arccos(x) (если что-нибудь стандартное забыл, можно добавить; если есть интересные результаты для хороших подмножеств, тоже интересуют). Требуется определить, совпадают ли соответствующие формулам функции действительного аргумента. Никаких целых/дробных частей и вообще того, что позволяет сводить целочисленные задачи, нет.

2) То же самое, только формулы без переменных (т.е. фактически нужно сравнить значения двух арифметических выражений).

Добавлено спустя 2 минуты 58 секунд:

поправка: тригонометрических функций нет (с ними легко сводить целочисленные задачи)

Добавлено спустя 1 минуту 29 секунд:

либо они есть, но рассматриваются только всюду определенные функции (на невсюду определенных разрешающий алгоритм может работать как попало)

[mserg]

Если для формул удастся придумать "нормальную форму", тогда, преобразуя обе формулы к нормальному виду, можно сделать заключение о совпадении.

Можно еще рассмотреть вероятностный алгоритм. Для этого случайным образом генерируются значения x и сравниваются значения lдвух функций. Так как при вычислении имеют место быть погрешности, то метод применим только при использовании интервальной арифметики (с процессорной точностью). Ответов может быть 2: формулы различны; формулы совпадают с высокой вероятностью.

[маткиб]

Поставим вопрос (в котором корень зла) иначе: какие существуют нижние оценки модуля не равного нулю числа, заданного формулой длины n бит? Достаточно ли чего-нибудь вроде
$\frac{1}{\underbrace{\exp(\exp(\ldots\exp(n)))}_{n \text{ раз}}}$?

Добавлено спустя 9 минут 13 секунд:

mserg писал(а):

Если для формул удастся придумать "нормальную форму", тогда, преобразуя обе формулы к нормальному виду, можно сделать заключение о совпадении.

В принципе, если допустить, что функции всюду определенные, то в качестве нормальной формы можно взять несколько первых членов разложения в ряд тейлора в окрестности нуля (эта нормальная форма будет работать только для сравнения формул длины не более некоторого заданного числа). Тогда вопрос упирается в оценку нужного числа членов и точности их вычисления.