9
$\begingroup$

Is there an efficient algorithm to determine if two terms are beta-equivalent? Specifically, I am 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 (BNF) 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$
4
  • $\begingroup$ Note: it was suggested that I cross-post this from Math StackExchange: math.stackexchange.com/questions/3748030 $\endgroup$ 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
  • $\begingroup$ Agda supports lossy unification which might be efficient, but as suggested by the name, it's lossy $\endgroup$
    – ice1000
    Nov 2 '21 at 18:30
11
$\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$
6
  • 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$ 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$ 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$ 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$ Jul 24 '20 at 10:49
6
$\begingroup$

I'd like to point out that if:

  1. the terms $M$ and $N$ are strongly normalizing (as the question allows), and

  2. one considers the complexity as depending also on the number $k_M$ and $k_N$ of beta-steps to normalize $M$ and $N$ (according to strong call-by-value evaluation),

then conversion can be tested very efficiently, namely bi-linearly, that is, linearly in the sizes $|M|$ and $|N|$ of the starting terms and linearly in the number of beta steps $k_M$ and $k_N$.

Note that taking into account the number of beta steps (that is, adding hypothesis 2 above), does not make the problem trivial, because, not only normal forms can be exponential in the size of the starting term (as pointed out in the question), but they can also be exponential in the number of beta steps to reach the normal form (a degeneracy known as size explosion and affecting also the simply typed lambda calculus).

The bilinear algorithm is very sophisticated. It is obtained by combining two algorithms by Accattoli, Condoluci, and Sacerdoti Coen, solving separately the two steps for testing conversion mentioned in the question.

The first algorithm evaluates terms in bi-linear time using sharing. The second algorithm compares the normal forms with sharing for equality of their unfolding in linear time.

The key point is that one has to use sharing to avoid the size explosion, and that doing it in linear time requires an extremely careful managing of sharing.

As far as I know, this is the only existing positive complexity result about conversion.

$\endgroup$
3
  • $\begingroup$ Hi @Beniamino, you say that the algorithm is "very sophisticated". The algorithm I have in mind is the following: compute the leftmost-outermost-useful normal forms of M and N in the linear substitution calculus, then compare them using the method you give in your paper with Ugo. However, if I do things naively, this algorithm is "only" polytime (both for the reduction part and the comparison part), whereas the sophistication is needed to achieve linearity, right? $\endgroup$ Nov 2 '21 at 11:54
  • $\begingroup$ Ah, sorry, I just realized you mentioned "strong call-by-value evaluation", so the algorithm I have in mind is probably not the right one (I mean, it cannot be improved to linear time)... $\endgroup$ Nov 2 '21 at 12:02
  • 1
    $\begingroup$ Hi Damiano, yes, my work with Ugo (relative to strong call-by-name) does provide a polytime algorithm but not a linear one (both comparison and evaluation are quadratic), probably I should have said it. For comparison (which is independent from the strategy), the linear and the quadratic algorithms are radically different. For evaluation, small adjustments might turn the quadratic algorithm for strong call-by-name into a linear one, but this has never been spelled out. For strong call-by-value, instead, there is a published linear algorithm, that at times has even logarithmic (!) overhead. $\endgroup$ Nov 3 '21 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.