Decidable real arithmetic

Question

I believe that what I'm about to describe has a name—I'm almost certain that I've seen this in model theory and term-rewriting systems, possibly having something to do with ‘signature’ or ‘carrier’?—so please feel free to tell me if I'm using terms in bad, or non-standard, ways.

Consider a set $C$ of real constants. (There's no reason that we couldn't consider constants from an arbitrary field, or ring, or … whatever; but let's say ‘real’ for definiteness.) Fix also, for each $n$, a (possibly empty) set $S_n$ of (partially defined) $n$-place, real-valued functions on $\mathbb R$.

Write $\Sigma = (C, (S_n)_n)$, and define the set of $\Sigma$-terms in the following (obvious) way. The collection of $\Sigma$-terms is the smallest subset $\mathcal T$ of the set of strings over the alphabet consisting of $C \sqcup \bigsqcup_n S_n$, together with 3 distinguished symbols (, ), and ,, satisfying:

1. Each element of $C$ is in $\mathcal T$.
2. If $\sigma \in S_n$, and $w_1, \ldots, w_n$ are $\Sigma$-terms, then $\sigma(w_1, \ldots, w_n) \in \mathcal T$.

Notice that there is an obvious (partially defined) map from $\Sigma$-terms to $\mathbb R$. Notice also that I am avoiding all questions of representability of elements of $C$; if this is worrisome, we can assume that $C$ is countable, fix an enumeration, and replace all elements of $C$ by their labels.

Now call $\Sigma$ decidable if the problem of whether a given $\Sigma$-term represents $0$ is decidable. (To avoid trivialities like $C = \mathbb R_{\ge0}$, with all operations preserving positivity, let's assume that subtraction lies in $S_2$.) Are there any results about what ensembles $\Sigma$ are decidable?

For example, it's obvious that, if $C = \mathbb Q$ and the operations allowed are the field operations, then $\Sigma$ is decidable; but what if we enlarge our operations to allow extraction of positive square roots, or enlarge $C$ to the algebraic closure of $\mathbb Q$?

Answer 1

There are at least two approaches to what you describe. In symbolic computation people ask questions of the sort you are asking, except that more generally one wants to know how to compute normal or canonical forms of terms, not just decide equality.

Another line of attack comes from computability theory. There is computability and computational complexity over an arbitrary structure (a set with operations and relations). This goes under the names "recursive model theory" and "effective model theory". They study not only decidability of equality, but other general questions about computability and computational complexity of model-theoretic concepts.

I am not really an expert on this so I am hoping someone else can provide the best references, but a good place to start might be the Handbook of Recursive Mathematics (volume 1, Recursive model theory). I do not know what to suggest for symbolic computation.

Also have a look at the Blum-Shub-Smale model of real number computation, see Complexity and real computation. It is not what you are asking about, because they assume equality as a decidable operation, but it is similar to what you are suggesting in other respects. It is a popular model of real number computation in some circles (computational geometry), and harshly criticized in others (computable analysis).