6
$\begingroup$

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:

  1. Compute the beta normal form for each term.
  2. 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?

$\endgroup$
  • $\begingroup$ Note: it was suggested that I cross-post this from Math StackExchange: math.stackexchange.com/questions/3748030 $\endgroup$ – user1636815 Jul 7 '20 at 23:26
  • $\begingroup$ Well you can evaluate in a way that does substitutions lazily (which more or less corresponds to thinking of terms as directed acyclic graphs instead of trees), and then the NF has a reasonable size, and you don't reduce the same thing several times. $\endgroup$ – xavierm02 Jul 9 '20 at 21:04
  • $\begingroup$ I don't think there is any way of guessing in which term to reduce and where that helps for the worst case. It might be possible for the average case, with enough tricks, but I doubt you can get anything more than a linear speedup. For example, if a variable is free in one term and not the other, then you know that a redex that has it as argument (and drops it) needs to be reduced at some point. $\endgroup$ – xavierm02 Jul 9 '20 at 21:13
8
$\begingroup$

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:

  1. $\eta$-long forms are stable under substitution, and therefore under $\beta$-reduction;
  2. two $\eta$-long $\beta$-normal forms are $\beta\eta$-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, $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).

$\endgroup$
  • 2
    $\begingroup$ Mairson's paper proves the result for $\beta\eta$, not $\beta$, unlike Statman. There is probably an obvious reason why that doesn't make a difference in the present context. $\endgroup$ – Martin Berger Jul 12 '20 at 19:56
  • 2
    $\begingroup$ @MartinBerger Probably because to decide $\beta\eta$, you can just compute $\eta$-long forms of both terms, and then decide $\beta$. $\endgroup$ – xavierm02 Jul 13 '20 at 8:36
  • $\begingroup$ @MartinBerger: thanks for your comment, I updated the answer. $\endgroup$ – Damiano Mazza Jul 14 '20 at 12:23
  • 1
    $\begingroup$ @xavierm02: that's indeed why Mairson's result implies Statman's. I updated my answer to give the details for those who are not familiar with $\eta$-long forms. Thank you. $\endgroup$ – Damiano Mazza Jul 14 '20 at 12:24
  • $\begingroup$ @DamianoMazza Given that expansion of terms to $\eta$-long NF can lead to a serious increase in size, I wonder if sharper bounds can be (or have already been) derived by a more sophisticated analysis (i.e. not just reducing to $\eta$-long and then comparing for $\beta$). $\endgroup$ – Martin Berger Jul 24 '20 at 10:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.