An efficient Beta-Equivalence algorithm? Is there an efficient algorithm to determine if two terms are beta-equivalent? I'm specifically curious about simply-typed-lambda-calculus, so you can assume both terms are strongly normalizing.
I know a simple algorithm:

Compute the beta normal form for each term.
Confirm that the two BNFs are alpha-equivalent.

But it is possible for BNFs to be exponentially larger than the original Term. Is it possible check the equivalence of Terms S and T in O(|S| + |T|) time?
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 $\beta\eta$-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_1\to\cdots\to A_n\to\alpha$ for some $n\in\mathbb 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}\ldots\lambda y_n^{A_n}.x\eta(y_1^{A_1})\cdots\eta(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:

$\eta$-long forms are stable under substitution, and therefore under $\beta$-reduction;
two $\eta$-long $\beta$-normal forms are $\beta\eta$-equivalent iff they are equal (up to $\alpha$-renaming, of course);
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, $M\simeq_{\beta\eta}N$ iff $\eta(M)\simeq_\beta\eta(N)$.
In fact, via point (3) above, an elementary recursive algorithm for deciding $\beta$-equivalence immediately gives an elementary recursive algorithm for deciding $\beta\eta$-equivalence (the one pointed out by xavierm02).
Let us prove the claim.  The right-to-left implication is trivial.  Conversely, suppose that $M\simeq_{\beta\eta} N$. This obviously implies $\eta(M)\simeq_{\beta\eta}\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 $P\simeq_{\beta\eta} Q$, so by point (2) $P=Q$, which proves $\eta(M)\simeq_\beta\eta(N)$ (they have the same $\beta$-normal form).