Rational exponential expressions Consider the following extension of polynomials.  The rational exponential expressions (REXes) are given by:


*

*The leaves 1 and $x$ for $x$ drawn from a class of variables; and

*Closed under the binary functions of addition, multiplication, exponentiation, and division.


This is a restriction to positive constants of a class of expressions studied in Brown, 1969, "Rational Exponential Expressions and a Conjecture Concerning π and e".  Buchberger & Loos, 1982, "Algebraic Simplification", sect. 6, mention the existence of algorithms for finding canonical forms for these expressions, but say their correctness depends on number-theoretic conjectures that have not been settled.
I'm interested in a decision procedure for dominance, where for two REXes in one variable, $f$ and $g$, $f \leq g$ if $\exists N \in {\mathbb N}.\forall n \in {\mathbb N}. N \leq n \implies f(n) \leq g(n)$.  Do we have either the existence of canonical forms, or decidability for this problem?  
 A: The integers are a red herring. All of the rational exponential expressions are logarithmico-exponential functions in the sense of Hardy. Therefore, for any such $f$ and $g$, either $f(t) > g(t)$ for all sufficiently large real $t$, 
$f(t) < g(t)$ for all sufficiently large real $t$ or $f(t)=g(t)$. There is no reason to restrict to the case that $t$ is an integer. 
I highly suspect that this problem is decidable, but I don't actually know this. This is the sort of thing that people who study transseries think about.
A: Yes, there are algorithms to decide asymptotic dominance - in fact for a much wider class of elementary functions. I discovered the first such algorithm circa 1980 while an undergrad member of the MIT Mathlab group researching effective algorithms for computing limits for the Macsyma symbolic computation system. Another different algorithm was discovered independently a handful of years later by John Shackell. You should be able to find references to the literature by googling the more recent buzzword "transseries".
Many computer algebra systems have (partial) implementations of these algorithms. Here's an example of my algorithm on (my generalization of) an example Rich Schroeppel proposed to attempt to stump my algorithm (he was convinced no such algorithm existed). It shows that $\rm{\: lim_{x\to\infty}\ d40 = e^a}$

Don't dare try L'Hopital's rule on that monster!
For further discussion (and the text form of the above image) see my post on sci.math, 1996/03/20, L'Hopital's rule question:
http://groups.google.com/group/sci.math/msg/05298104ac44efd2
http://groups.google.com/groups?selm=WGD.96Mar20231913%40berne.ai.mit.edu 
A: I don't have an answer to the one-variable decision
question that you asked.
But you did introduce multi-variable
expressions, and there are some fascinating results on the
multi-variable analogue of your domination problem.
(Perhaps you know all this already...) That is, given two rational
exponential expressions f(x1,...,xk)
and
 f(x1,...,xk), the problem is to decide whether
 f(n1,...,nk) <=
 g(n1,...,nk), for all positive integers (n1,...,nk) except at most
 finitely often.
The answer is that this decision problem is undecidable,
and it is undecidable even for polynomial expressions.
There is no algorithm that will tell you when one
multi-variable (positive) polynomial expression eventually
dominates another.
The reason is that the decision problem of 
Diophantine equations
is encodable into this domination problem. That work
famously shows that the problem to decide if a given
integer polynomial p(x1,...,xk) has
a zero in the integers is undecidable. This is the famous
MRDP solution to Hilbert's 10th
problem.
It is easy to reduce the Diophantine problem to the
domination problem, as follows. First, let us restrict to
non-negative integers, for which the MRDP results still
apply. Suppose we are given a polynomial
p(x1,...,xk) expression over the
integers, and want to decide if it has a solution in the
natural numbers. This expression may involve some minus
signs, which your expressions do not allow, but we will
take care of that by moving all the minus signs to one
side. Introduce a new variable x0 and consider
the domination problem:


*

*Does 1 <=
(1+n0)p(n1,...,nk)2 for
all natural numbers except finitely often?


We can expand the right hand side, and move the negative
signs to the left, to arrive at an instance of your
domination problem, using only positive polynomials. Now,
if p(n1,...,nk) is never 0, then the
answer to the stated domination problem is Yes, since the
right hand side will always be at least 1 in this case.
Conversely, if p(n1,...,nk) = 0 has
a solution, then we arrive at infinitely many violations of
domination by using any choice of n0. Thus, if
we could decide the domination problem, then we could
decide whether p(n1,...,nk) = 0 has
solutions in the natural numbers, which we cannot do by the
MRDP theorem. QED
I think the best situation with the Diophantine equations
is that it remains undecidable with nine variables, and so
the domination problem I described above is undecidable
with ten variables. (Perhaps Bjorn Poonen will show up here
and tell us a better answer?)
Of course, this doesn't answer the one-variable question
that you asked, and probably you know all this already.
My final remark is that if one can somehow represent the
inverse pairing function, then one will get undecidability
even in the one variable case. That is, let f(n,m) =
(n+m)(n+m+1)/2 + m be one of the usual pairing functions,
which is bijective between ω2 and ω.
Let p be the function such that p(f(n,m)) = n, the
projection of the pairs onto the first coordinate. If the
expressions are enriched to allow p, then one can in effect
work with several variables by coding them all via pairing
into one variable, and in this case, the domination problem
in the one-variable case, for rational exponential
expressions also allowing the function p, will be
undecidable. It would seem speculative to suppose that p is
itself equivalent to a rational exponential expression, but
do you know this?
