Suppose we are given an expression composed of integers,$ +, *, -, /,$ elementary functions $(exp, sin, cos, tan)$ and their inverses (and for simplicity, assume each argument to these functions is in the range where it is defined and real valued, ie $[-1,1]$ for $arcsin$). Examples:
$\exp(\log(9)/2)-3$
$\exp(-\exp(\exp(1000))$
$\arcsin(3/5)+\arctan(4/3)-3*\arcsin(1/2)$
Our task is to determine whether the expression exactly equals zero. Is this task computable? (I want to know whether it's possible to write a C program to do this; I guess that's equivalent to whether the task is Turing computable).
Here's my thinking so far: I suspect that an algorithm could find a rational approximation within $\frac1n$ of the expression for any $n$. Successively doing this for each $n$ and halting if the approximation is outside $[-\frac1n,\frac1n]$, we could halt iff the expression is nonzero (but with unbounded memory usage). This could be interleaved with attempts to prove that the expression is zero. However, I don't know whether every expression that equals zero is provably so (if not, I guess I need to think about how I would define "equals zero"). It also would be nice if the running time and memory of the algorithm were bounded by some function of the expression length...