Deterministic polynomial-time PIT for straight-line program equivalence

During compiler optimization, proving that an optimized basic block of code is semantically equivalent to its unoptimized original form is a core objective. For loop-free programs with basic arithmetic, this verification reduces to checking the equivalence of straight-line programs (SLPs).

Let \(\mathbb{F}\) be a field and \(X=\{x_1,\ldots,x_n\}\) be a set of input variables. An SLP \(\mathcal{P}\) of size \(s\) over \(\mathbb{F}[X]\) is a sequence of assignments

\[ v_i = A_i \circ B_i, \qquad \text{for } i \in \{1,\dots,s\}, \]

where the operation \(\circ \in \{+,-,\times\}\), and the operands \(A_i,B_i\) are either constants from \(\mathbb{F}\), an input variable from \(X\), or previously computed intermediate values \(v_j\) with \(j < i\). The output of the SLP is \(v_s\), which represents a formal multivariate polynomial \(P(X)\in\mathbb{F}[X]\).

Given two SLPs \(\mathcal{P}_1\) and \(\mathcal{P}_2\) computing polynomials \(P_1(X)\) and \(P_2(X)\), the equivalence checking problem asks whether

\[ P_1(X)-P_2(X)\equiv 0 \]

identically.

A direct expansion of the two polynomials is not feasible in general. An SLP of size \(s\) can compute a polynomial of degree as large as \(2^s\), with exponentially many monomials. Thus, expanding the output into a sum-of-monomials representation may require exponential time and space in the worst case, making naive compiler verification impractical.

This problem is an instance of Polynomial Identity Testing, or PIT. By the Schwartz-Zippel lemma, PIT has a randomized polynomial-time algorithm. By evaluating the SLP at randomly chosen points from a sufficiently large finite subset \(S\subset\mathbb{F}\) and checking whether the result is zero, one can detect if \(P_1-P_2\) is not the zero polynomial with high probability.

Open Problem. Does general arithmetic-circuit PIT admit a deterministic polynomial-time algorithm? Deterministic polynomial-time algorithms are known for several restricted circuit classes. However, no unconditional deterministic polynomial-time algorithm is known for PIT in the general case.

During compiler optimization, proving that an optimized basic block of code is semantically equivalent to its unoptimized original form is a core objective. For loop-free programs with basic arithmetic, this verification reduces to checking the equivalence of straight-line programs (SLPs).

Let \(\mathbb{F}\) be a field and \(X = \{x_1, \ldots, x_n\}\) be a set of input variables. An SLP, \(\mathcal{P}\) of size \(s\) over \(\mathbb{F}[X]\) is a sequence of assignments:

\[
v_i = A_i \circ B_i, \quad \text{for } i \in \{1, \dots, s\}
\]

where the operation \(\circ \in \{+, -, \times\}\), and the operands \(A_i, B_i\) are either constants from \(\mathbb{F}\), an input variable from \(X\), or previously computed intermediate values \(v_j\) with \(j < i\). The output of the SLP is \(v_s\), which represents a formal multivariate polynomial \(P(X) \in \mathbb{F}[X]\).

Given two SLPs \(\mathcal{P}_1\) and \(\mathcal{P}_2\) computing polynomials \(P_1(X)\) and \(P_2(X)\), the equivalence checking problem asks whether \(P_1(X) - P_2(X) \equiv 0\) identically.

A direct expansion of the two polynomials is not feasible in general. An SLP of size \(s\) can compute a polynomial of degree as large as \(2^s\), with exponentially many monomials. Thus, expanding the output into a sum-of-monomials representation may require exponential time and space in the worst-case, making naive compiler verification impractical.

This problem is an instance of Polynomial Identity Testing, or PIT. By the Schwartz-Zippel lemma, PIT has a randomized polynomial-time algorithm. By evaluating SLP at randomly chosen points from a sufficiently large finite subset of the field \(S \subset \mathbb{F}\) and checking whether the result is zero, we can detect if \(P_1 - P_2\) is not the zero polynomial with high probability.

\textbf{Open Problem:} Does general arithmetic-circuit PIT admit a deterministic polynomial-time algorithm? Deterministic polynomial-time algorithms are known for several restricted circuit classes. However, no unconditional deterministic polynomial-time algorithm is known for PIT in the general case.