Is equivalence of functions built from nested exponentiations a decidable problem?

Question

Let $\mathcal{E}$ be the minimal set of symbolic expressions (without any predefined meaning) such that

• The symbol $x$ is in $\mathcal{E}$, and
• If expressions $P,Q\in\mathcal{E}$, then the superscript expression $(P)^{(Q)}\in \mathcal{E}$.

For every expression $S\in\mathcal{E}$, define the interpretation of $S$ as the function $\mathbb{R}^+\to\mathbb{R}^+$ given by $x\mapsto S$, where each occurrence of $x$ in $S$ is considered as the function parameter, and superscript expressions are considered as exponentiations. Note that we concern ourselves only with positive values of $x$.

We can make an observation that interpretations of two structurally distinct expressions can be the same function, e.g. the expressions $$\left((x)^{(x)}\right)^{\left((x)^{(x)}\right)},\ \left((x)^{\left((x)^{(x)}\right)}\right)^{(x)}$$ both have the same function $x\mapsto x^{x^{x+1}}$ as their interpretation.

---

Questions:

• Is there an algorithm that for every pair of expressions from $\mathcal{E}$ can decide whether they have the same interpretation?
• If yes, can we give an explicit example of such algorithm?

Answer 1

The problem is effectively decidable, and we will describe an algorithm. By way of preparation, we need to mention the o-minimality of the real exponential field, and Wilkie's solution to Tarski's High School Algebra problem.

The real exponential field $\mathbb{R}_{exp}$ is the field of real numbers with an additional unary function $x\mapsto e^x$. Wilkie proved that $\mathbb{R}_{exp}$ is o-minimal, meaning that that every definable set of reals is a finite union of intervals.

Note that the function $x^x$ is definable in $\mathbb{R}_{exp}$. Indeed, $y=x^x$ if and only if $$\exists u\,\,(x=e^u\wedge y=e^{ux}),$$ (using $x^x=e^{x\ln x}$). Since definable functions are closed under composition, all of the tower expressions in $\mathcal{E}$ are definable in $\mathbb{R}_{exp}$.

Now suppose two expressions $f,g\in\mathcal{E}$ define the same function on the natural numbers. Let $S$ be the set of positive real numbers $x$ for which $f(x)=g(x)$. Then $S$ is a definable subset of $R_{exp}$. Therefore $S$ is a finite union of intervals. Since $S$ contains every positive integer, it follows that $S$ contains some interval $(x_0,\infty)$.

But all of the functions defined by elements of $\mathcal{E}$ are analytic on $\mathbb{R}^+$. It follows immediately from the principle of real analytic continuation (see e.g. Corollary 1.2.5 of A Primer of Real Analytic Functions by Krantz and Parks) that $f$ and $g$ define the same function on $\mathbb{R}^+$.

So we are reduced to solving the identity problem for $\mathcal{E}$ interpreted over the positive integers. This brings us to Tarski's High School Algebra Problem and Wilkie's solution. Tarski wrote down a set of axioms for the equational theory of the structure $(\mathbb{N},\,+,\,\times,\,e,\,1)$, where $e$ is binary exponentiation. These so-called High School Axioms are the (positive) semiring axioms together with the rules of exponentiation \begin{align*} &x^1=x,\,\,1^x=x\\ &(xy)^z=x^zy^z\\ %%%%%%%%%%%%%%%%%% Following Exponent rule corrected &x^{y+z}=x^yx^z\\ &(x^y)^z=x^{yz}. \end{align*} Tarski asked if the whole equational theory can be deduced from these. The answer is no. Wilkie found 'exotic' identities not deducible from the above, and he gave a computably enumerable set of identities from which the whole equational theory is indeed deducible.

Returning to identities for $\mathcal{E}$, we now have an algorithm. Given a possible identity, use Wilkie's axioms to look for it by listing all equations between elements of $\mathcal{E}$ that hold for all natural numbers. At the same time plug in integers $1,2,\ldots$ looking for a counterexample. One of these two processes will terminate after finitely many steps.

Wilkie's paper is available from CiteSeer here.

There is a Wikipedia article on Tarski's High School problem here.

It would be interesting to know if there is a nice analytic proof (avoiding Wilkie's theorem on the o-minimality of $\mathbb{R}_{exp}$) that the functions defined on $\mathbb{R}^+$ by the expressions in $\mathcal{E}$ are determined by their values on the positive integers.

Answer 2

This is a justification of the algorithm suggested in Dan Turetsky's comment.

Every expression in $E$ reduces to an expression in $E'$ which is the minumum language such that $x\in E'$ and $x^{(p_1*\dots*p_n)}\in E'$ whenever $p_1,\dots,p_n\in E'$. Let us define a linear order on $E'$ as follows.

First, every expression in $E'$ has a level, which is the maximum number of nested exponentiations. More precisely, the level of $x$ is 0, and the level of $x^{(p_1*\dots*p_n)}$ is the maximum of the levels of $p_i$'s plus one. Let $E_n$ denote the set of expresions of level at most $n$.

We define our linear order on $E_n$ by induction. First of all, $x$ is the minimal element of our order. Let $f,g\in E_n$ and $f,g\ne x$. Then $f=x^{p_1*\dots*p_m}$ and $g=x^{q_1*\dots*q_k}$ where $p_i$'s and $q_j$'s are from $E_{n-1}$. Let us sort $p_i$'s and $q_j$'s in non-ascending order with respect to the (already defined) linear order on $E_{n-1}$. Then we say that $f>g$ iff the sequence $(p_i)$ is lexocographically bigger than $(q_j)$, i.e. $p_l>q_l$ where $l$ is the first index of mismatch (or $(q_j)$ is an initial subsegment of $(p_i)$). Clearly this definition is consistent with its previous stage, so we have a well-defined linear order on $E'$. This order is easy to compute.

I claim that, if $f>g$ in this linear order, then $f$ dominates $g$ at infinity, i.e. $f(x)>g(x)$ for all sufficiently large $x\in\mathbb R_+$. Moreover, $f$ dominates $g^a$ for any $a\in\mathbb N$. The latter claim is easy to prove by induction. Indeed, $x^x$ dominates $x^a$, and the induction step goes as follows. Let $f=x^{p_1*\dots*p_m}$ and $g=x^{q_1*\dots*q_k}$ and $f>g$. We need to prove that $f$ dominates $g^a$, or, equivalently, that the product $p_1\dots p_m$ dominates $aq_1\dots q_k$. By removing common initial terms we may assume that $p_1>q_1$ in our order. (If all $q_j$'s cancel out completely, it remains to prove that $p_1$ dominates the constant $a$ and this is trivial.) Now by induction hypothesis, $p_1$ dominates $q_1^{k+1}$, which dominates $q_1^2q_2\dots q_k$, which dominates $aq_1\dots q_k$, q.e.d.