Decidibilidad de la igualdad y la solidez de las expresiones que involucran aritméticos y exponenciales elementales.

Question

Tendremos expresiones que estén compuestas de elementos de $ \ mathbb n $ y un conjunto limitado de operaciones binarias { $ +, \ Times, -, / $ } y funciones { $ \ exp, \ ln $ }. Las expresiones están siempre bien formadas y forman árboles finitos, con números como nodos de hoja y operadores como nodos internos, operaciones binarias que tienen dos subpresiones infantiles y las funciones. Se interpreta un valor de tal expresión que significa algún número en $ \ mathbb r $ .

Hay dos limitaciones en la estructura de las expresiones: el divisor (la subexpresión a la derecha) de $ / $ no puede ser 0 y el El argumento de $ \ ln $ debe ser positivo.

Tengo dos preguntas sobre este tipo de expresiones:

• ¿Es posible asegurar la "solidez" de tal expresión, en el sentido de que las dos limitaciones se pueden verificar en el tiempo finito?

• es una verificación de igualdad entre dos expresiones de este tipo decidible?

Estas preguntas parecen estar conectadas en el sentido de que si puedes verificar la igualdad de la subexpresión relevante a cero, puede decidir si una expresión de padres de división es un sonido, y no parece difícil verificar Si una subexpresión de $ \ ln $ es positivo o negativo si se sabe que no es cero.

Sé que la igualdad en $ \ mathbb r $ generalmente no es decidible, mientras que la igualdad en los números algebraicos es. Sin embargo, me pregunto cómo la inclusión de { $ \ exp, \ ln $ } cambia el resultado. Sospecho que si existe "casos patológicos" donde dos expresiones con una estructura dramáticamente diferente resultan en el mismo número real, verificar la igualdad entre ellos podría ser indecidible, como el $ \ exp $ < / span> y $ \ ln $ podría obstaculizar la normalización de dichas expresiones.

(una nota lateral: Publiqué una versión anterior de una pregunta con intención similar aquí , pero resultó haber pensado muy poco detrás de él, y tuvo complicaciones innecesarias (= no relacionadas con la carne de la pregunta) con logaritmos complejos).

Answer 1

No lo sé, pero sospecho que es una pregunta abierta.

Si el teoría de los reales con función exponencial es decidible, entonces su problema Es decidible, también. Se sabe que si la conjetura de Shanuel sostiene, entonces el primero es decidible, por lo que su problema es también.

Si entiendo correctamente, el siguiente papel aborda su problema:

El problema de identidad para las funciones y constantes elementales . Dan Richardson, John Fitch. Issac '94.

Parece que muestran un procedimiento que siempre termina si la conjetura de Shanuel sostiene; Y si no termina para una expresión particular, entonces podemos extraer de esa expresión un contraejemplo a la conjetura de Shanuel. Luego, argumentan que parece poco probable que encontraremos un contraejemplo en cualquier momento, por lo que parece poco probable que encontraremos insumos en los que este procedimiento no termine en cualquier momento pronto.

Consulte también https://matherverflow.net/q/118972/37212 y https://matoverflow.net/q/129563/37212 y https://matoverflow.net/q/145299/37212 .