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 have a finite, well-defined beta normal form.
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?