An efficient Beta-Equivalence algorithm?

The answer is no. An old theorem of Statman states that $beta$-equivalence in the simply-typed $lambda$-calculus is not elementary recursive, that is, no algorithm whose running time is bounded by $2^{vdots^{2^{|S|+|T|}}}$ for a tower of exponentials of fixed height may decide whether two simply-typed terms $S$ and $T$ are $beta$-equivalent.

The original statement is from

Richard Statman. The typed $lambda$-calculus is not elementary recursive. Theoret. Comput. Sci. 9:73-81, 1979.

A simpler proof may be found in this paper by Harry Mairson.

Edit: as observed by Martin Berger, Mairson proves that $betaeta$-equivalence is not elementary recursive, whereas Statman's result (and the OP's question) concerns $beta$-equivalence, without $eta$. However, as pointed out by xavierm02, Mairson's result implies Statman's. Let me fill in the details for those who are not familiar with $eta$-long forms.

The $eta$-long form $eta(x^A)$ of a variable $x^A$ is defined by induction on $A$: observe that $A=A_1tocdotsto A_ntoalpha$ for some $ninmathbb N$, some types $A_1,ldots,A_n$ (smaller than $A$) and some atom $alpha$, and let

$$eta(x^A) := lambda y_1^{A_1}ldotslambda y_n^{A_n}.xeta(y_1^{A_1})cdotseta(y_n^{A_n}),$$

where the $eta(y_i^{A_i})$ are given inductively.

The $eta$-long form $eta(M)$ of a simply-typed $lambda$-term $M$ is defined by replacing every occurrence of variable $x^A$ of $M$ (free or bound) with $eta(x^A)$. (NB: through Curry-Howard, this corresponds to taking a sequent calculus proof and expanding it so that it has only atomic axioms).

Observe that:

1. $eta$-long forms are stable under substitution, and therefore under $beta$-reduction;
2. two $eta$-long $beta$-normal forms are $betaeta$-equivalent iff they are equal (up to $alpha$-renaming, of course);
3. computing the $eta$-long form of a simply-typed $lambda$-term is elementary recursive (if you don't keep the size of type annotations, the $eta$-long form of a term may be exponentially bigger, but that is not a problem).

That Mairson's result implies Statman's is a consequence of the following:

Claim. Let $M,N$ be two simply-typed $lambda$-terms. Then, $Msimeq_{betaeta}N$ iff $eta(M)simeq_betaeta(N)$.

In fact, via point (3) above, an elementary recursive algorithm for deciding $beta$-equivalence immediately gives an elementary recursive algorithm for deciding $betaeta$-equivalence (the one pointed out by xavierm02).

Let us prove the claim. The right-to-left implication is trivial. Conversely, suppose that $Msimeq_{betaeta} N$. This obviously implies $eta(M)simeq_{betaeta}eta(N)$. Let $P$ and $Q$ be the $beta$-normal forms of $eta(M)$ and $eta(N)$, respectively. By point (1) above, both $P$ and $Q$ are $eta$-long (because $eta(M)$ and $eta(N)$ are). But of course we still have $Psimeq_{betaeta} Q$, so by point (2) $P=Q$, which proves $eta(M)simeq_betaeta(N)$ (they have the same $beta$-normal form).