<p>I'd like to point out that if:</p>
<ol>
<li><p>the terms <span class="math-container">$M$</span> and <span class="math-container">$N$</span> are strongly normalizing (as the question allows), and</p>
</li>
<li><p>one considers the complexity as depending also on the number <span class="math-container">$k_M$</span> and <span class="math-container">$k_N$</span> of beta-steps to normalize <span class="math-container">$M$</span> and <span class="math-container">$N$</span> (according to strong call-by-value evaluation),</p>
</li>
</ol>
<p>then conversion can be tested <em>very</em> efficiently, namely <em>bi-linearly</em>, that is, linearly in the sizes <span class="math-container">$|M|$</span> and <span class="math-container">$|N|$</span> of the starting terms and linearly in the number of beta steps <span class="math-container">$k_M$</span> and <span class="math-container">$k_N$</span>.</p>
<p>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 <em>they can also be exponential in the number of beta steps to reach the normal form</em> (a degeneracy known as <em>size explosion</em> and affecting also the simply typed lambda calculus).</p>
<p>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.</p>
<p>The <a href="https://ieeexplore.ieee.org/document/9470630" rel="nofollow noreferrer">first algorithm</a> evaluates terms in bi-linear time using sharing. The <a href="https://dl.acm.org/doi/10.1145/3354166.3354174" rel="nofollow noreferrer">second algorithm</a> compares the normal forms with sharing for equality of their unfolding in linear time.</p>
<p>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.</p>
<p>As far as I know, this is the only existing positive complexity result about conversion.</p>

CC BY-SA 4.0
2021-11-02T11:54:42.030Z
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?
Damiano Mazza
CC BY-SA 4.0
2021-11-02T12:02:07.690Z
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)...
Damiano Mazza
CC BY-SA 4.0
2021-11-03T10:49:29.133Z
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.
Beniamino Accattoli
CC BY-SA 4.0
2021-10-31T12:48:19.317Z
2021-11-02T08:40:37.123Z
2021-11-02T08:40:37.123Z
Beniamino Accattoli
<p>The answer is no.  An old theorem of Statman states that <span class="math-container">$\beta$</span>-equivalence in the simply-typed <span class="math-container">$\lambda$</span>-calculus is not elementary recursive, that is, no algorithm whose running time is bounded by <span class="math-container">$2^{\vdots^{2^{|S|+|T|}}}$</span> for a tower of exponentials of fixed height may decide whether two simply-typed terms <span class="math-container">$S$</span> and <span class="math-container">$T$</span> are <span class="math-container">$\beta$</span>-equivalent.</p>
<p>The original statement is from</p>
<p>Richard Statman.  <a href="https://www.sciencedirect.com/science/article/pii/0304397579900070" rel="noreferrer">The typed <span class="math-container">$\lambda$</span>-calculus is not elementary recursive</a>.  <em>Theoret. Comput. Sci.</em> 9:73-81, 1979.</p>
<p>A simpler proof may be found in <a href="https://www.sciencedirect.com/science/article/pii/030439759290020G" rel="noreferrer">this paper by Harry Mairson</a>.</p>
<p><strong>Edit:</strong> as observed by Martin Berger, Mairson proves that <span class="math-container">$\beta\eta$</span>-equivalence is not elementary recursive, whereas Statman's result (and the OP's question) concerns <span class="math-container">$\beta$</span>-equivalence, without <span class="math-container">$\eta$</span>.  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 <span class="math-container">$\eta$</span>-long forms.</p>
<p>The <em><span class="math-container">$\eta$</span>-long form</em> <span class="math-container">$\eta(x^A)$</span> of a variable <span class="math-container">$x^A$</span> is defined by induction on <span class="math-container">$A$</span>: observe that <span class="math-container">$A=A_1\to\cdots\to A_n\to\alpha$</span> for some <span class="math-container">$n\in\mathbb N$</span>, some types <span class="math-container">$A_1,\ldots,A_n$</span> (smaller than <span class="math-container">$A$</span>) and some atom <span class="math-container">$\alpha$</span>, and let</p>
<p><span class="math-container">$$\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}),$$</span></p>
<p>where the <span class="math-container">$\eta(y_i^{A_i})$</span> are given inductively.</p>
<p>The <em><span class="math-container">$\eta$</span>-long form</em> <span class="math-container">$\eta(M)$</span> of a simply-typed <span class="math-container">$\lambda$</span>-term <span class="math-container">$M$</span> is defined by replacing every occurrence of variable <span class="math-container">$x^A$</span> of <span class="math-container">$M$</span> (free or bound) with <span class="math-container">$\eta(x^A)$</span>.  (NB: through Curry-Howard, this corresponds to taking a sequent calculus proof and expanding it so that it has only atomic axioms).</p>
<p>Observe that:</p>
<ol>
<li><span class="math-container">$\eta$</span>-long forms are stable under substitution, and therefore under <span class="math-container">$\beta$</span>-reduction;</li>
<li>two <span class="math-container">$\eta$</span>-long <span class="math-container">$\beta$</span>-normal forms are <span class="math-container">$\beta\eta$</span>-equivalent iff they are equal (up to <span class="math-container">$\alpha$</span>-renaming, of course);</li>
<li>computing the <span class="math-container">$\eta$</span>-long form of a simply-typed <span class="math-container">$\lambda$</span>-term is elementary recursive (if you don't keep the size of type annotations, the <span class="math-container">$\eta$</span>-long form of a term may be exponentially bigger, but that is not a problem).</li>
</ol>
<p>That Mairson's result implies Statman's is a consequence of the following:</p>
<p><strong>Claim.</strong>  Let <span class="math-container">$M,N$</span> be two simply-typed <span class="math-container">$\lambda$</span>-terms.  Then, <span class="math-container">$M\simeq_{\beta\eta}N$</span> iff <span class="math-container">$\eta(M)\simeq_\beta\eta(N)$</span>.</p>
<p>In fact, via point (3) above, an elementary recursive algorithm for deciding <span class="math-container">$\beta$</span>-equivalence immediately gives an elementary recursive algorithm for deciding <span class="math-container">$\beta\eta$</span>-equivalence (the one pointed out by xavierm02).</p>
<p>Let us prove the claim.  The right-to-left implication is trivial.  Conversely, suppose that <span class="math-container">$M\simeq_{\beta\eta} N$</span>. This obviously implies <span class="math-container">$\eta(M)\simeq_{\beta\eta}\eta(N)$</span>. Let <span class="math-container">$P$</span> and <span class="math-container">$Q$</span> be the <span class="math-container">$\beta$</span>-normal forms of <span class="math-container">$\eta(M)$</span> and <span class="math-container">$\eta(N)$</span>, respectively. By point (1) above, both <span class="math-container">$P$</span> and <span class="math-container">$Q$</span> are <span class="math-container">$\eta$</span>-long (because <span class="math-container">$\eta(M)$</span> and <span class="math-container">$\eta(N)$</span> are). But of course we still have <span class="math-container">$P\simeq_{\beta\eta} Q$</span>, so by point (2) <span class="math-container">$P=Q$</span>, which proves <span class="math-container">$\eta(M)\simeq_\beta\eta(N)$</span> (they have the same <span class="math-container">$\beta$</span>-normal form).</p>

CC BY-SA 4.0
2020-07-12T19:56:06.253Z
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.
Martin Berger
CC BY-SA 4.0
2020-07-13T08:36:46.653Z
@MartinBerger Probably because to decide $\beta\eta$, you can just compute $\eta$-long forms of both terms, and then decide $\beta$.
xavierm02
CC BY-SA 4.0
2020-07-14T12:23:44.943Z
@MartinBerger: thanks for your comment, I updated the answer.
Damiano Mazza
CC BY-SA 4.0
2020-07-14T12:24:38.050Z
@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.
Damiano Mazza
CC BY-SA 4.0
2020-07-24T10:49:57.427Z
@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$).
Martin Berger
CC BY-SA 4.0
2020-08-04T07:36:23.087Z
@MartinBerger the increase in size is only relative to the underlying, untyped term.  If you take type annotations into account (which is natural since otherwise the notion of $\eta$-expansion does not make much sense), then there is no exponential blow-up. For instance, transforming a sequent calculus proof into a sequent calculus proof with atomic axioms is a polynomial-time procedure, a fact which I think is regularly used in proof complexity.
Damiano Mazza
CC BY-SA 4.0
2020-07-11T11:09:55.953Z
2020-07-14T12:23:09.940Z
2020-07-14T12:23:09.940Z
Damiano Mazza
<p>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.</p>
<p>I know a simple algorithm:</p>
<ol>
<li><p>Compute the <a href="https://en.wikipedia.org/wiki/Beta_normal_form" rel="nofollow noreferrer">beta normal form</a> (BNF) for each term.</p>
</li>
<li><p>Confirm that the two BNFs are alpha-equivalent.</p>
</li>
</ol>
<p>But it is possible for BNFs to be exponentially larger than the original term? Is it possible check the equivalence of terms <span class="math-container">$S$</span> and <span class="math-container">$T$</span> in <span class="math-container">$O(|S| + |T|)$</span> time?</p>

CC BY-SA 4.0
2020-07-07T23:26:14.033Z
Note: it was suggested that I cross-post this from Math StackExchange: https://math.stackexchange.com/questions/3748030
user1636815
CC BY-SA 4.0
2020-07-09T21:04:22.610Z
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.
xavierm02
CC BY-SA 4.0
2020-07-09T21:13:40.113Z
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.
xavierm02
CC BY-SA 4.0
2021-11-02T18:30:38.583Z
Agda supports lossy unification which might be efficient, but as suggested by the name, it's lossy
ice1000
<lambda-calculus><typed-lambda-calculus>
Is there an efficient beta-equivalence algorithm?
user1636815
# Is there an efficient beta-equivalence algorithm?

(Asked by: username_0 on 2020-07-07)

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](https://en.wikipedia.org/wiki/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?

**Tags:** lambda-calculus, typed-lambda-calculus
> **Comments:**
> **username_0**: Note: it was suggested that I cross-post this from Math StackExchange: https://math.stackexchange.com/questions/3748030  
> **username_1**: 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.  
> **username_1**: 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.  
> **username_2**: Agda supports lossy unification which might be efficient, but as suggested by the name, it's lossy  

---

## 2 answers

### Answer by username_4 on 2020-07-11. Score: 12 | Accepted answer

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](https://www.sciencedirect.com/science/article/pii/0304397579900070). *Theoret. Comput. Sci.* 9:73-81, 1979.

A simpler proof may be found in [this paper by Harry Mairson](https://www.sciencedirect.com/science/article/pii/030439759290020G).

**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).

> **Comments:**
> **username_5**: 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.  
> **username_1**: @MartinBerger Probably because to decide $\beta\eta$, you can just compute $\eta$-long forms of both terms, and then decide $\beta$.  
> **username_4**: @MartinBerger: thanks for your comment, I updated the answer.  
> **username_4**: @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.  
> **username_5**: @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$).  
> **username_4**: @MartinBerger the increase in size is only relative to the underlying, untyped term.  If you take type annotations into account (which is natural since otherwise the notion of $\eta$-expansion does not make much sense), then there is no exponential blow-up. For instance, transforming a sequent calculus proof into a sequent calculus proof with atomic axioms is a polynomial-time procedure, a fact which I think is regularly used in proof complexity.  

---

### Answer by username_3 on 2021-10-31. Score: 6

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](https://ieeexplore.ieee.org/document/9470630) evaluates terms in bi-linear time using sharing. The [second algorithm](https://dl.acm.org/doi/10.1145/3354166.3354174) 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.

> **Comments:**
> **username_4**: 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?  
> **username_4**: 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)...  
> **username_3**: 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.  

---

