Theoretical Computer Science

Motivation

Shor's 1997 paper (SIAM J. Comput. 26(5), arXiv:quant-ph/9508027) gives a polynomial-time quantum algorithm for factoring integers. The quantum computer does not factor directly: it finds the multiplicative order of an element modulo $n$. The step from order finding to factoring is classical and randomized, and goes back to Miller's 1976 work on primality testing (G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13 (1976)). Every account of Shor's algorithm, and every resource estimate for breaking RSA with a quantum computer, depends on this reduction succeeding with a constant probability per trial. This mission formalizes that probability bound as Shor states it on p. 1498 of the published paper.

Setting

Let $n > 1$ be an odd integer with prime factorization

$$n = \prod_{i=1}^{k} p_i^{\alpha_i},$$

so $k$ is the number of distinct prime factors of $n$, all odd. The unit group $(\mathbb{Z}/n\mathbb{Z})^\times$ consists of the residues coprime to $n$; it has $\varphi(n)$ elements, where $\varphi$ is Euler's totient function.

For a unit $x$ the order $r = \operatorname{ord}_n(x)$ is the least positive integer with $x^r \equiv 1 \pmod n$. For each $i$ the local order $r_i$ is the order of $x \bmod p_i^{\alpha_i}$, taken modulo the full prime power, not modulo $p_i$. For a positive integer $m$, $\nu_2(m)$ denotes the exponent of the largest power of $2$ dividing $m$.

The reduction is: choose $x$ uniformly at random from $(\mathbb{Z}/n\mathbb{Z})^\times$, obtain its order $r$ (from the quantum subroutine), and compute

$$g(x) = \gcd\bigl(x^{r/2} - 1,\ n\bigr).$$

The procedure yields a nontrivial factor at $x$ when $r$ is even and $1 < g(x) < n$. In Lean this event is ShorAlgorithms.Reduction.successEvent n u for u : (ZMod n)ˣ, and $r_i$ is localOrder n u p for p ∈ n.primeFactors.

Formalization targets

Goal: the success probability

$$\Pr_{x \in (\mathbb{Z}/n)^\times}\bigl[r \text{ even and } 1 < \gcd(x^{r/2}-1, n) < n\bigr] \;\ge\; 1 - \frac{1}{2^{k-1}}.$$

It is stated for every odd $n > 1$. For a prime power ($k = 1$) the bound is $0$, so the statement says nothing there; it is informative exactly when $n$ is not a prime power, as the paper remarks. The constant is sharp: for $n = 21$ exactly $6$ of the $12$ units succeed, so $1 - 1/2^{k}$ in place of $1 - 1/2^{k-1}$ would be false.

Milestones, in the order the page uses them

1. Success criterion. If $r$ is even and $x^{r/2} \not\equiv -1 \pmod n$, then $1 < \gcd(x^{r/2}-1, n) < n$.
2. Order is the lcm. $r = \operatorname{lcm}(r_1, \dots, r_k)$.
3. Failure forces agreement. For odd $n$, if the procedure fails at $x$, then $\nu_2(r_1) = \cdots = \nu_2(r_k)$.
4. At most half per odd prime power. For an odd prime $p$ and $\alpha \ge 1$, at most $\varphi(p^\alpha)/2$ units modulo $p^\alpha$ have order with a prescribed 2-adic valuation.
5. All agree rarely. The units for which $\nu_2(r_1) = \cdots = \nu_2(r_k)$ number at most $\varphi(n)/2^{k-1}$.

Significance

The result. The bound turns an order-finding oracle into a factoring algorithm: when $n$ is odd and not a prime power, each trial succeeds with probability at least $1/2$, so $t$ independent trials all fail with probability at most $2^{-t}$. Even numbers and prime powers are split classically, as the paper notes, so the bound completes the reduction from factoring to order finding. The same criterion — a square root of $1$ other than $\pm 1$ splits $n$ — underlies the Miller–Rabin test and several classical factoring methods.

Formalizing it. The mathematics is classical and proved; the paper gives a sketch of one paragraph. This mission writes out the sketch as machine-checked statements over Mathlib's ZMod, including the probabilistic step, which in the paper is an informal appeal to the Chinese remainder theorem and "50% probability of agreeing with the previous ones". Mathlib already has the needed ingredients (cyclicity of $(\mathbb{Z}/p^\alpha)^\times$ for odd $p$, ZMod.chineseRemainder, ZMod.card_units_eq_totient), but not the reduction or its probability bound.

Difficulty

The success criterion (milestone 1) is elementary. The substance is the counting. The obvious route — treating the $\nu_2(r_i)$ as independent and each "equal to the previous one with probability $1/2$" — needs both a precise product decomposition of the unit group modulo $n$ into the unit groups modulo $p_i^{\alpha_i}$, compatible with the local orders, and the count in a cyclic group of even order of the elements whose order has a given 2-adic valuation. The informal phrase "at most a 50% probability of agreeing with the previous ones" hides a conditioning argument over $k - 1$ coordinates that has to be done by an explicit cardinality bound. A second pitfall is milestone 3: its converse direction and its forward direction use oddness of $n$ in different places, and modulo a power of $2$ the argument breaks because $-1 \equiv 1 \pmod 2$.

Formalization scope

• Sample space. Uniform on (ZMod n)ˣ; probabilities are stated in cleared-denominator form, $(1 - 2^{-(k-1)})\,\varphi(n) \le \#\{\text{successes}\}$ in $\mathbb{R}$, with the count as Nat.card of a subtype. Non-units have no multiplicative order and are not sampled.
• The gcd. $x^{r/2}$ is represented by its least nonnegative residue .val, which is at least $1$ for a unit when $n > 1$, so the natural-number subtraction in val - 1 never truncates. $r/2$ is natural-number division, used only under Even r.
• $k$. n.primeFactors.card, at least $1$ for $n > 1$, so k - 1 does not truncate. Since $n$ is odd this equals the page's "number of distinct odd prime factors".
• Local orders. The order of the image of $x$ in ZMod (p ^ n.factorization p) under the reduction homomorphism.
• Hypotheses. The goal assumes exactly $n$ odd and $n > 1$. It does not assume "not a prime power": that clause in the paper describes when the bound is useful. Milestones 1 and 2 do not assume $n$ odd, because they do not need it; milestones 3 and 5 do.
• No trivialization. Counting over all of ZMod n instead of the units would put non-units (with junk order $0$) into the denominator; the goal counts over (ZMod n)ˣ and divides by $\varphi(n)$. The goal's constant is the paper's $1 - 1/2^{k-1}$, which is attained, so it cannot be weakened into a triviality without changing the theorem.
• Welcome contributions. A reusable counting lemma for elements of prescribed 2-adic order in a finite cyclic group; the transfer of ZMod.chineseRemainder to unit groups and to local orders; and proofs of the milestones in any order.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172 (preprint arXiv:quant-ph/9508027, https://arxiv.org/abs/quant-ph/9508027)
• G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
• D. E. Knuth, The Art of Computer Programming, Vol. 2: Seminumerical Algorithms, 2nd ed., Addison-Wesley, 1981.
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford University Press, 1979 (Theorem 121, Chinese remainder theorem).

Motivation

Shor's factoring and discrete logarithm algorithms (Shor 1997) reduce both problems to sampling from the output of a quantum Fourier transform: a register holding a superposition with a hidden period is transformed, then measured, and the measured value carries information about the period. The whole speed-up rests on one engineering fact: for $q = 2^l$ the $q \times q$ Fourier matrix, which has $q^2 = 4^l$ entries, can be applied by a quantum circuit of only $O(l^2)$ elementary gates, each acting on one or two bits.

That circuit was found independently by Coppersmith (IBM RC 19642, 1994) and Deutsch, and Shor's §4 presents it following Ekert and Jozsa (Rev. Mod. Phys. 68, 1996). It is the quantum analogue of the radix-2 fast Fourier transform, and it reappears in phase estimation, in the hidden subgroup algorithms for abelian groups, and in every textbook account of quantum computation. This mission formalizes Shor's statement that the circuit computes the Fourier matrix, up to a reversal of the output bits, together with the two displayed steps of its verification.

Setting

A register of $l$ bits has one basis state $|a\rangle = |a_{l-1} a_{l-2} \dots a_0\rangle$ for every bit string, with $a_0$ the least significant bit; the string encodes the integer

$$a = \sum_{j=0}^{l-1} 2^j a_j, \qquad 0 \le a < q = 2^l .$$

A state is a vector of complex amplitudes, one per basis state. A gate is a matrix whose rows are indexed by input basis vectors and whose columns are indexed by output basis vectors (§2, p. 1489). A gate on some of the bits acts on those bits through its matrix and leaves the others alone (§2, p. 1490): the output amplitude at a string $b$ is the sum, over the possible input values $u$ of the acted-on bits, of the input amplitude at $b$ with those bits replaced by $u$, times the matrix entry from $u$ to the corresponding bits of $b$.

The Fourier matrix $A_q$ (eq. (4.1)) is the $q \times q$ matrix with $(a, c)$ entry $q^{-1/2}\exp(2\pi i\,ac/q)$; it takes $|a\rangle$ to $q^{-1/2}\sum_{c=0}^{q-1}\exp(2\pi i\,ac/q)\,|c\rangle$.

The circuit uses two gates (eqs. (4.2), (4.3)):

• $R_j$ acts on bit $j$ with matrix $\frac{1}{\sqrt 2}\begin{pmatrix} 1 & 1 \\ 1 & -1\end{pmatrix}$;
• $S_{j,k}$, for $j < k$, acts on bits $j$ and $k$ with matrix $\mathrm{diag}(1, 1, 1, e^{i\theta_{k-j}})$, where $\theta_{k-j} = \pi / 2^{k-j}$; it multiplies the amplitude of a basis state by $e^{i\theta_{k-j}}$ when bits $j$ and $k$ are both $1$.

The circuit is the gate sequence (4.4), applied from left to right:

$$R_{l-1}\, S_{l-2,l-1}\, R_{l-2}\, S_{l-3,l-1}\, S_{l-3,l-2}\, R_{l-3} \cdots R_1\, S_{0,l-1}\, S_{0,l-2} \cdots S_{0,2}\, S_{0,1}\, R_0 ,$$

that is, for $j = l-1, \dots, 0$ it applies $S_{j,l-1}, \dots, S_{j,j+1}$ and then $R_j$. On three bits it is $R_2 S_{1,2} R_1 S_{0,2} S_{0,1} R_0$.

The bit reversal of a string $b$ is the string $c$ with $c_k = b_{l-1-k}$.

Formalization targets

Goal: the circuit computes $A_q$ up to bit reversal (§4, p. 1496)

For every $l \ge 0$ and every basis state $|a\rangle$, with $q = 2^l$,

$$\text{circuit}\,|a\rangle = \frac{1}{q^{1/2}}\sum_{b}\exp(2\pi i\,ac/q)\,|b\rangle, \qquad c = \text{bit reversal of } b .$$

The sum runs over all $l$-bit strings $b$. Reading the output register in reverse order therefore yields $A_q|a\rangle$.

Milestone 1: the amplitude along the circuit (§4, eq. (4.5), p. 1496)

The amplitude of $|b\rangle$ in $\text{circuit}\,|a\rangle$ is

$$2^{-l/2}\exp\Big(i\Big(\sum_{0\le j<l}\pi a_jb_j + \sum_{0\le j<k<l}\frac{\pi}{2^{k-j}}a_jb_k\Big)\Big).$$

Milestone 2: the phase identity (§4, eqs. (4.6)–(4.10), pp. 1496–1497)

For bit strings $a, b$, with $c$ the bit reversal of $b$ and $a, c$ their values,

$$\exp\Big(i\Big(\sum_{0\le j<l}\pi a_jb_j + \sum_{0\le j<k<l}\frac{\pi}{2^{k-j}}a_jb_k\Big)\Big) = \exp(2\pi i\,ac/q).$$

Significance

The result. The goal says that $A_q$, a dense unitary on $2^l$ amplitudes, is realized by $l$ one-bit gates and $l(l-1)/2$ two-bit gates, followed by a relabelling of the output. This is what makes the Fourier sampling step of the factoring algorithm (§5) and of the discrete logarithm algorithm (§6) polynomial in the number of bits. Without it, the analyses of those sections describe measurements of states that no efficient circuit is known to prepare. The bit reversal is a real part of the statement: the circuit does not compute $A_q$ itself for $l \ge 2$, and an implementation must either permute the output bits or read them in reverse order.

Formalizing it. The identity is classical and its proof is short on paper; its content lies in bookkeeping that is easy to get wrong: which bit a gate touches, which of the input or output value a bit holds when a phase gate acts, and the order in which the gates are applied. A machine-checked version fixes all of these conventions explicitly and yields a reusable model of gate-level circuits on bit strings. To the drafter's knowledge there is no Lean formalization of this circuit on Prove2Me; the platform's FastFourierTransform rows state the classical Cooley–Tukey recursion for the unnormalized transform with the opposite sign, which is a different object.

Difficulty

Multiplying out the gate matrices is not an argument beyond tiny $l$: the difficulty is to control the whole product of $l(l+1)/2$ gates symbolically. The paper's argument (§4, p. 1496) is informal at exactly the points a formal proof must make precise: that only one sequence of intermediate basis states from $|a\rangle$ to $|b\rangle$ carries nonzero amplitude, and that at the moment $S_{j,k}$ acts, bit $k$ already holds its output value $b_k$ while bit $j$ still holds its input value $a_j$. Both facts depend on the order (4.4); applying the same gates in the reverse order gives a different unitary, whose phase pairs $b_j$ with $a_k$. The phase identity then holds only modulo $2\pi$, not as an equality of real numbers, so it cannot be closed by rearranging sums alone.

Formalization scope

• States. A bit string on $l$ bits is Fin l → Fin 2, with bit j equal to $a_j$ and value $\sum_j 2^j a_j$ (least significant bit first). A state is a function from bit strings to ℂ. The case $l = 0$ ($q = 1$, empty circuit) is included.
• Gate application follows the row = input convention: a one-bit gate $M$ on bit $j$ sends $\psi$ to $b \mapsto \sum_u \psi(b[j\mapsto u])\,M_{u, b_j}$, and a two-bit gate acts analogously on the pair (bit $j$, bit $k$).
• The circuit is the gate list (4.4) — an explicit list of constructors R j and S j k — run by a left fold, so the leftmost gate acts first. It is not defined as the matrix $A_q$ or by its entries; a definition of that kind would make the goal true by unfolding and is ruled out.
• Angles. $\theta_{k-j} = \pi/2^{k-j}$ uses natural-number subtraction, which is exact because the list only contains $S_{j,k}$ with $j < k$.
• Normalization. The prefactor $q^{-1/2}$ is written $(\sqrt{2^l})^{-1}$.
• Basis form. The goal is stated on basis states, as on the page; by linearity it determines the circuit on every state.
• Not stated. The gate count: the paper's sentence "we thus need to use $l(l-1)/2$ quantum gates" (p. 1496) counts only the gates $S_{j,k}$; the sequence (4.4) also contains the $l$ gates $R_j$, $l(l+1)/2$ gates in all. The approximate transform of Coppersmith and the one-bit construction of Griffiths and Niu (p. 1497) are out of scope, as is the polynomial-time claim.

Welcome contributions: proofs of the two milestones and the goal; general lemmas about one- and two-bit gate actions on Fin l → Fin 2 states (commutation of gates on disjoint bits, linearity, action on basis states), which are reusable for any gate-level circuit; and a proof that the circuit is unitary.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
• D. Coppersmith, An approximate Fourier transform useful in quantum factoring, IBM Research Report RC 19642, 1994. https://arxiv.org/abs/quant-ph/0201067
• A. Ekert and R. Jozsa, Quantum computation and Shor's factoring algorithm, Rev. Mod. Phys. 68:733–753, 1996. https://doi.org/10.1103/RevModPhys.68.733
• R. B. Griffiths and C.-S. Niu, Semiclassical Fourier transform for quantum computation, Phys. Rev. Lett. 76:3228–3231, 1996. https://doi.org/10.1103/PhysRevLett.76.3228

Motivation

A process on a shared-memory multiprocessor that finds a lock held must decide what to do while it waits. It can spin, repeatedly testing the lock and occupying its processor, or it can block, giving the processor to another process and paying a fixed context-switch cost $C$ to be descheduled and later restored. Spinning is cheap when the lock is released soon; blocking is cheap when the wait is long. The waiting time is not known in advance, so the choice has to be made on-line. This is the spin-block problem, studied by Karlin, Manasse, McGeoch and Owicki in Competitive Randomized Algorithms for Nonuniform Problems (Algorithmica 11, 1994, doi:10.1007/BF01189993), §4. Mathematically it is the continuous form of the ski-rental problem, and the same rent-or-buy structure recurs in power-down policies and in TCP acknowledgement (Karlin, Kenyon, Randall, STOC 2001).

Timeline:

• Karlin, Manasse, Rudolph and Sleator (1988, doi:10.1007/BF01762111) introduced competitive analysis of snoopy caching and showed that $2$ is the optimal deterministic factor there. The spin-block analogue is recorded in the 1994 paper (pp. 558–559): spinning for time $C$ and then blocking is $2$-competitive, and no deterministic algorithm does better.
• Karlin, Manasse, McGeoch and Owicki (SODA 1990; Algorithmica 1994) found the optimal randomized factors for snoopy caching and spin-block. For spin-block, Theorem 10 (p. 559) gives $e/(e-1)\approx1.582$ against an oblivious adversary. Theorem 9 (p. 559) shows that against an adaptive on-line adversary randomization does not help: the factor stays $2$.

Setting

Fix a context-switch cost $C>0$. A lock wait is described by its release time $\tau\ge0$. An algorithm handling the wait chooses a blocking time $b\in[0,\infty]$: it spins until time $b$ and then blocks ($b=\infty$: never block). The cost of the wait is

$$\mathrm{waitCost}_C(b,\tau)=\begin{cases}\tau,&\tau\le b,\\ b+C,&b<\tau,\end{cases}$$

so a lock released exactly at the blocking time costs $\tau$. The optimal off-line algorithm, which knows $\tau$, pays $\min(\tau,C)$.

An input is a finite sequence $\sigma=(\tau_0,\dots,\tau_{n-1})$ of lock waits. A deterministic on-line algorithm chooses the blocking time of wait $j$ as a function of $\tau_0,\dots,\tau_{j-1}$, the release times it has already observed. Its cost $C_A(\sigma)$ is the sum of the wait costs, and the off-line cost is $C_{opt}(\sigma)=\sum_j\min(\tau_j,C)$.

A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms: a probability space $(I,\mu)$ and a deterministic algorithm $A_i$ for each $i\in I$, with $i\mapsto C_{A_i}(\sigma)$ measurable for every $\sigma$. Its expected cost is $\mathbf{E}C_A(\sigma)=\int C_{A_i}(\sigma)\,d\mu(i)$. Following §1 of the paper, $A$ is $c$-competitive against an oblivious adversary if there is a constant $a$ with

$$\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(\sigma)+a\qquad\text{for every input }\sigma .$$

The adversary is oblivious: it fixes $\sigma$ before the algorithm's random choices are made.

The paper's algorithm blocks at a random time with cumulative distribution

$$\pi(t)=\begin{cases}\dfrac{e^{t/C}-1}{e-1},&0\le t\le C,\\[1ex] 1,&t>C,\end{cases}$$

where $\pi(t)$ is the probability of blocking before time $t$.

Formalization targets

Goal: Theorem 10 (p. 559)

For every $C>0$:

$$\Big(\forall A\ \forall c,\ A\ \text{is } c\text{-competitive}\ \Rightarrow\ c\ge\tfrac{e}{e-1}\Big)\quad\text{and}\quad\exists A,\ A\ \text{is } \tfrac{e}{e-1}\text{-competitive}.$$

Milestones

1. Expected cost of one wait (§4.1, p. 560). For a blocking time with law $\nu$ and release time $\tau$,

$$\mathbf{E}\,\mathrm{waitCost}_C(b,\tau)=\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt,\qquad \pi(t)=\nu\{b<t\}.$$

2. The ratio of the paper's distribution (§4.1, p. 560). With the $\pi$ above, for all $\tau\ge0$,

$$\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt\le\tfrac{e}{e-1}\min(\tau,C).$$

3. Theorem 10, first claim: the lower bound $c\ge e/(e-1)$ for every $c$-competitive randomized algorithm.
4. Theorem 10, second claim: existence of an $e/(e-1)$-competitive randomized algorithm.

Significance

Theorem 10 settles the randomized competitive ratio of the continuous ski-rental problem: $e/(e-1)$ is achievable and cannot be improved by any on-line algorithm, randomized or not, against an oblivious adversary. The same constant is the limit of the paper's snoopy-caching ratios $e_p/(e_p-1)$ as the block size grows, and it recurs in randomized rent-or-buy problems and in on-line primal-dual analyses.

The result is proved in the literature, and the mission's work is to formalize it. The platform has related material but not this statement: Primal-Dual Online Algorithms I: Fractional Ski Rental proves a deterministic, fractional, discrete-day bound (PrimalDualOnline.SkiRental.fractional_competitive), which is a different model and contains no lower bound. A complete formalization produces a reusable model of randomized on-line algorithms with history-dependent decisions and an exact lower bound for them.

Difficulty

The upper bound per lock wait is an explicit computation. The difficulty lies elsewhere. First, the on-line algorithm is allowed to adapt to the release times of all previous waits, so a bound for a single wait does not by itself bound a sequence: the randomized algorithm must be assembled so that each wait is handled with the right blocking law, whatever happened before. Second, the lower bound is a statement about every randomized algorithm and must survive the additive constant $a$: a single hard lock wait proves nothing, because $a$ absorbs any bounded loss. It has to be shown that on long sequences of waits every algorithm loses a factor $e/(e-1)$ on average. The natural first idea, to exhibit one bad release time for each algorithm, fails for randomized algorithms facing an oblivious adversary.

Formalization scope

All objects live in the namespace NonuniformCompetitive.SpinBlock. Release times are ℝ≥0, blocking times ℝ≥0∞, wait costs ℝ≥0∞, and the off-line cost is real. Committed conventions:

• $C>0$ is a hypothesis of every theorem (the paper's "some large cost $C$"); at $C=0$ blocking at once is free and the lower bound fails.
• A tie $b=\tau$ costs $\tau$; this matches "$\pi(t)$ is the probability that the algorithm blocks sometime before time $t$".
• Inputs are finite sequences of lock waits and competitiveness carries the additive constant $a$ of §1 (p. 543). A formalization with a single wait and no additive constant would be a different, easier lower bound and is ruled out.
• The on-line algorithm sees the release times of earlier waits (the information used by the paper's adaptive algorithms, p. 561). This enlarges the class of algorithms: it strengthens the lower bound and does not affect the upper bound.
• A randomized algorithm is a mixed strategy whose cost on each fixed input is measurable in the random outcome; the expected cost is a lower Lebesgue integral. Without measurability the lower integral would not be the expectation and the upper bound would become easier than the paper's.
• Milestone 1 is stated for every blocking law, not only for the paper's $\pi$. Milestone 2 keeps the paper's inequality, although equality holds.

Infrastructure a complete development needs: Lebesgue integrals of functions of a random variable (the layer-cake formula), interval integrals of the exponential, the construction of a probability measure on $[0,\infty]$ with a prescribed continuous distribution function, and a Yao-type averaging argument over finitely supported input distributions for the lower bound. The model of randomized on-line algorithms with history-dependent decisions is reusable for other rent-or-buy problems. Contributions welcome: proofs of the milestones, and intermediate lemmas such as the discretised lower bound for a fixed step $C/p$.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. doi:10.1007/BF01189993
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. doi:10.1007/BF01762111
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.
• A. R. Karlin, C. Kenyon, D. Randall, Dynamic TCP Acknowledgement and Other Stories about e/(e−1), STOC 2001, 502–509. doi:10.1145/380752.380845
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3 (2009). doi:10.1561/0400000024

Motivation

Scheduling jobs with release dates on one machine to minimize the total weighted completion time, written $1|r_j|\sum w_jC_j$, is strongly NP-hard even with unit weights (Lenstra, Rinnooy Kan & Brucker, 1977). It is a basic model of scheduling theory and a standard testbed for approximation algorithms built on linear programming relaxations. Several LP relaxations give lower bounds for it (Dyer & Wolsey, 1990; Queyranne, 1993), and the question how far these bounds can be from the optimum is also a question about the quality of branch-and-bound methods that use them.

Timeline, as surveyed in Table 1 of Goemans, Queyranne, Schulz, Skutella & Wang (2002):

• Phillips, Stein & Wein (Math. Programming, 1998) introduce converting a preemptive schedule into a nonpreemptive one by list scheduling, and the notion of $\alpha$-points; for the weighted problem their bound is $16+\epsilon$.
• Hall, Shmoys & Wein (SODA 1996) obtain 4; Schulz (IPCO 1996) and Hall, Schulz, Shmoys & Wein (Math. Oper. Res., 1997) obtain 3; Chakrabarti et al. obtain $2.8854+\epsilon$, and a combination of methods gives $2.4427+\epsilon$.
• Goemans (SODA 1997) orders jobs by $\alpha$-points of the LP schedule: $\alpha=1/\sqrt2$ gives $1+\sqrt2\approx2.4143$, a uniformly random $\alpha$ gives 2.
• Chekuri, Motwani, Natarajan & Stein (SIAM J. Comput., 2001) use random $\alpha$-points of an arbitrary preemptive schedule and obtain $e/(e-1)$ for unit weights, relative to the preemptive optimum rather than an LP value.
• Goemans, Queyranne, Schulz, Skutella & Wang (2002) prove $1.7451$ for the best common $\alpha$ and $1.6853$ for job-dependent random $\alpha_j$, both relative to the LP value $Z_R$. Afrati et al. (FOCS 1999) later give a polynomial-time approximation scheme, which does not bound the LP relaxations.

This mission formalizes the $1.6853$ result, the paper's main theorem.

Setting

There are $n$ jobs $N=\{0,\dots,n-1\}$. Job $j$ has an integral processing time $p_j>0$, an integral release date $r_j\ge0$ and a weight $w_j>0$. The jobs are indexed so that $w_0/p_0\ge w_1/p_1\ge\dots\ge w_{n-1}/p_{n-1}$.

The LP schedule is the preemptive schedule that at every moment processes the available (released, unfinished) job of smallest index. Since the data are integral, it is determined slot by slot: in $[\tau,\tau+1)$ it runs the smallest-index job $j$ with $r_j\le\tau$ and work left, or idles. Let $A^{LP}_j\subseteq\mathbb R$ be the set of times at which it processes $j$. The mean busy time of $j$ is

$$M^{LP}_j=\frac1{p_j}\int_{A^{LP}_j}t\,dt .$$

The mean busy time relaxation (R) has a variable $M_j$ per job:

$$Z_R=\min\Bigl\{\sum_j w_j\bigl(M_j+\tfrac12p_j\bigr)\ :\ \sum_{j\in S}p_jM_j\ge p(S)\bigl(r_{\min}(S)+\tfrac12p(S)\bigr)\ \text{for all nonempty }S\subseteq N\Bigr\},$$

with $p(S)=\sum_{j\in S}p_j$ and $r_{\min}(S)=\min_{j\in S}r_j$. $Z_R$ is a lower bound on the optimum of $1|r_j|\sum w_jC_j$.

For $0<\alpha\le1$ the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has been processed for $\alpha p_j$ units in the LP schedule; $t_j(0^+)$ is the start time of $j$. For a vector $\boldsymbol\alpha\in(0,1]^n$, the $(\alpha_j)$-schedule processes the jobs nonpreemptively, as early as possible, in nondecreasing order of $t_j(\alpha_j)$; $C^{\boldsymbol\alpha}_j$ is the completion time of $j$ in it.

Let $\gamma\approx0.4835$ be the solution in $(0,1)$ of $\gamma+\ln(2-\gamma)=e^{-\gamma}\bigl((2-\gamma)e^{\gamma}-1\bigr)$, and set

$$\delta=\gamma+\ln(2-\gamma)\approx0.8999,\qquad c=1+\frac{e^{-\gamma}}{\delta},\qquad g(\alpha)=\begin{cases}(c-1)e^\alpha&0<\alpha\le\delta,\\0&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.9 (p. 185)

$c<1.6853$, and if $\alpha_1,\dots,\alpha_n$ each have density $g$ and are pairwise independent, then $\sum_j w_jC^{\boldsymbol\alpha}_j$ is integrable and

$$\mathbb E\Bigl[\sum_j w_jC^{\boldsymbol\alpha}_j\Bigr]\le c\cdot Z_R .$$

The bound is against the constant $c$ defined by the formula; the decimal $1.6853$ appears only in the separate inequality $c<1.6853$.

Milestones

1. Theorem 2.5 (p. 173): $M^{LP}$ is an optimal solution of (R), so $Z_R=\sum_jw_j(M^{LP}_j+\tfrac12p_j)$.
2. Eq. (3.1) (p. 176): $M^{LP}_j=\int_0^1t_j(\alpha)\,d\alpha$.
3. Corollary 3.2 (p. 179): $C^{\boldsymbol\alpha}_j\le t_j(\alpha_j)+\sum_{k:\alpha_k\le\eta_k(\alpha_j)}(1+\alpha_k-\eta_k(\alpha_j))p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$.
4. Eq. (3.10) (p. 182): $M^{LP}_j=t_j(0^+)+\sum_{k\in N_2}(1-\mu_k)p_k+\tfrac12p_j$, where $N_2$ is the set of jobs processed between the start and completion of $j$ and $\mu_k$ is the fraction of $j$ processed before $k$ starts.
5. Eq. (3.11) (p. 183): the bound of Corollary 3.2 split over $N_1=N\setminus(N_2\cup\{j\})$ and $N_2$.
6. Lemma 3.11 (p. 185): $g$ is a probability density on $(0,1]$, and (i) $\int_0^\eta g(\alpha)(1+\alpha-\eta)\,d\alpha\le(c-1)\eta$, (ii) $(1+E_g[\alpha])\int_\mu^1g(\alpha)\,d\alpha\le c(1-\mu)$ for $\eta,\mu\in[0,1]$.

Significance

Theorem 3.9 gives a randomized algorithm for $1|r_j|\sum w_jC_j$ whose expected cost is at most $1.6853$ times the optimum, and a variant of it runs on-line (Theorem 3.14). Since $Z_R$ is a lower bound, it also shows that the relaxation (R), and the preemptive time-indexed relaxation (D), which has the same value, is within a factor $1.6853$ of the optimum (Corollary 3.10). The paper's Section 3.6 shows the gap of these relaxations can approach $e/(e-1)\approx1.5819$, so the bound is not far from what this relaxation can give.

The result is proved on paper; no machine-checked proof exists, and no part of this theory (LP schedule, $\alpha$-points, list scheduling from a preemptive schedule) is on the platform. The mission produces, besides the goal, a reusable formal account of $\alpha$-point scheduling: the LP schedule as a concrete object, the identity between mean busy times and average $\alpha$-points, and the deterministic completion-time bound of Corollary 3.2, which underlies many later $\alpha$-point analyses.

Difficulty

The obvious argument, bounding $C^{\boldsymbol\alpha}_j$ by Corollary 3.2 and integrating each $\alpha_k$ independently against $g$, does not work directly: the set of jobs $k$ with $\alpha_k\le\eta_k(\alpha_j)$ depends on $\alpha_j$, and the two effects of the random $\alpha_k$ pull in opposite directions (a small $\alpha_k$ shrinks the terms $1+\alpha_k-\eta_k$, a large one removes terms from the sum). The analysis needs the structure of the LP schedule around job $j$ (equations (3.9)–(3.11)) to separate the jobs whose $\eta_k$ is constant in $\alpha_j$ from those for which it jumps from $0$ to $1$, and then a density tuned to both at once. The claim is made under pairwise independence only, so no product structure of the random vector is available. On the formal side, the LP schedule, $\alpha$-points and list scheduling are defined from scratch, and the measure-theoretic content (integrability of a piecewise-constant function of $\boldsymbol\alpha$, conditioning under pairwise independence) is real work.

Formalization scope

Jobs are Fin n (0-based), $p$ and $r$ are natural numbers and $w$ is real. The ordering by $w_j/p_j$ is a hypothesis of every statement about the LP schedule, which is defined by the smallest-index rule; under that hypothesis the two coincide. The LP schedule is defined slot by slot, which is exact for integral data. Processing is represented by sets of times, not indicator functions. $t_j(\alpha)$ is an infimum over times, $t_j(0^+)=\inf A^{LP}_j$, and the $(\alpha_j)$-schedule is the closed form $C^{\boldsymbol\alpha}_j=\max_{k\preceq j}\bigl(r_k+\sum_{k\preceq i\preceq j}p_i\bigr)$ of list scheduling in lexicographic (α-point, index) order. $Z_R$ is the real infimum of the objective over the feasible set of (R), which is nonempty and bounded below for $w\ge0$. The random vector is any probability measure on $\mathbb R^n$ whose coordinate laws all equal the law with density $g$ and whose coordinates are pairwise independent; the product measure is one example, but the theorem is for all of them. $\gamma$ is any solution in $(0,1)$ of its equation.

A trivializing formalization is ruled out: the expectation is asserted together with integrability (a non-integrable integrand would have Bochner integral $0$), $g$ is supported on $(0,\delta]$ so every $\alpha_j$ lies in $(0,1]$ almost surely, and the bound is against $Z_R$ defined from (R), not against an expression that already contains Theorem 2.5.

Running times ($O(n\log n)$, $O(n^2)$), derandomization, the counting results (Proposition 3.8, Lemma 3.12) and the on-line variant are not formalized. Lemma 3.1 on the auxiliary $(\alpha_j)$-Conversion schedule is not a milestone; Corollary 3.2 is stated directly for the $(\alpha_j)$-schedule.

Contributions welcome: proofs of the milestones in any order; general lemmas on list scheduling and $\alpha$-points of preemptive schedules, which are reusable beyond this mission; and the measure-theoretic step from pairwise independence to the conditional bound on $\mathbb E[C^{\boldsymbol\alpha}_j\mid\alpha_j]$.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single machine scheduling with release dates, SIAM J. Discrete Math. 15(2):165–192, 2002. https://doi.org/10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998.
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Math. Oper. Res. 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM–SIAM SODA, 591–598, 1997.
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31:146–166, 2001. https://doi.org/10.1137/S0097539797327180
• M. E. Dyer, L. A. Wolsey, Formulating the single machine sequencing problem with release dates as a mixed integer program, Discrete Appl. Math. 26:255–270, 1990.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Ann. Discrete Math. 1:343–362, 1977.

Motivation

Minimizing the total weighted completion time $\sum_j w_j C_j$ of jobs with release dates on a single machine, written $1\,|\,r_j\,|\,\sum w_j C_j$ in scheduling notation, is strongly NP-hard. It is one of the basic models of machine scheduling, and it has served as a test case for a general technique in approximation algorithms: solve a linear programming relaxation, read off a preemptive schedule, and convert it into a nonpreemptive one using $\alpha$-points, the times at which a given fraction of each job has been processed. Phillips, Stein and Wein (doi:10.1007/BF01585872) introduced ordering jobs by points of a preemptive schedule; Goemans (SODA 1997, reference [11] of the paper below) and Chekuri, Motwani, Natarajan and Stein (doi:10.1137/S0097539797327180) showed that choosing $\alpha$ at random improves the guarantee.

Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X) combine two LP relaxations, shown to have equal value, with carefully chosen random $\alpha$. This mission formalizes their Theorem 3.5: when a single $\alpha$ is drawn from a truncated exponential density, the resulting schedule costs in expectation at most $c < 1.7451$ times the LP lower bound.

Timeline:

• 1998: Phillips, Stein and Wein give the first constant-factor approximation (ratio $2$) for the unit-weight problem $1\,|\,r_j\,|\,\sum C_j$ by converting a preemptive schedule.
• 1997: Goemans (SODA) introduces randomly chosen $\alpha$-points for the weighted problem, the conference precursor of the paper formalized here.
• 2001: Chekuri, Motwani, Natarajan and Stein give a randomized $e/(e-1) \approx 1.58$-approximation for the unit-weight problem.
• 2002: Goemans, Queyranne, Schulz, Skutella and Wang give $1.7451$ for a single random $\alpha$ (Theorem 3.5) and $1.6853$ for job-dependent random $\alpha_j$ (Theorem 3.9), both against the same LP bound.
• 1999: Afrati et al. (doi:10.1109/SFFCS.1999.814574) give a polynomial-time approximation scheme for the problem. It is not LP-based, so the LP-relative factors of Theorems 3.5 and 3.9 remain of interest as bounds on the relaxations' integrality gaps.

Setting

There are $n$ jobs $N = \{1, \dots, n\}$. Job $j$ has an integral processing time $p_j > 0$, an integral release date $r_j \ge 0$ and a weight $w_j > 0$. The jobs are indexed so that $w_1/p_1 \ge w_2/p_2 \ge \cdots \ge w_n/p_n$.

A preemptive schedule gives each job a set $A_j \subseteq [r_j, \infty)$ of processing times of measure $p_j$, the sets pairwise disjoint. The mean busy time of $j$ is $M_j = \frac{1}{p_j}\int_{A_j} t\,dt$.

The LP schedule is the preemptive schedule that always processes the available job of smallest index, which under the indexing above is the available job of largest ratio $w_j/p_j$. Its mean busy times are $M^{LP}_j$.

The mean busy time relaxation (R) minimizes $\sum_j w_j (M_j + \tfrac12 p_j)$ subject to $\sum_{j \in S} p_j M_j \ge p(S)\big(r_{\min}(S) + \tfrac12 p(S)\big)$ for every nonempty $S \subseteq N$, where $p(S) = \sum_{j\in S} p_j$ and $r_{\min}(S) = \min_{j\in S} r_j$. Its optimal value is $Z_R$, a lower bound on the optimum of $1\,|\,r_j\,|\,\sum w_j C_j$.

For $0 < \alpha \le 1$, the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has received $\alpha p_j$ units of processing in the LP schedule, and $t_j(0^+)$ is its start time. The $\alpha$-schedule processes the jobs nonpreemptively, each as early as possible, in nondecreasing order of $t_j(\alpha)$; $C^\alpha_j$ is the completion time of $j$ in it. More generally, the $(\alpha_j)$-schedule orders the jobs by $t_j(\alpha_j)$ for a vector $\boldsymbol\alpha = (\alpha_j)$.

Let $0 < \gamma < 1$ solve $1 - \frac{\gamma^2}{1+\gamma} = \gamma + \ln(1+\gamma)$ ($\gamma \approx 0.4675$), and set

$$c = \frac{1+\gamma}{1+\gamma-e^{-\gamma}}, \qquad \delta = 1 - \frac{\gamma^2}{1+\gamma}, \qquad f(\alpha) = \begin{cases}(c-1)e^{\alpha} & 0 < \alpha \le \delta,\\ 0 & \text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.5

If $\alpha$ is drawn with density $f$, then $c < 1.7451$, the expectation below is finite, and

$$\mathbb E_f\Big[\sum_{j} w_j C^\alpha_j\Big] \le c \cdot Z_R .$$

Milestones

1. Theorem 2.5: $M^{LP}$ is an optimal solution to (R), so $Z_R = \sum_j w_j (M^{LP}_j + \tfrac12 p_j)$.
2. Eq. (3.1): $M^{LP}_j = \int_0^1 t_j(\alpha)\,d\alpha$.
3. Corollary 3.2: $C^{\boldsymbol\alpha}_j \le t_j(\alpha_j) + \sum_{k:\,\alpha_k\le\eta_k(\alpha_j)} (1+\alpha_k-\eta_k(\alpha_j))\,p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$ in the LP schedule.
4. Eq. (3.10): $M^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_j$, where $N_2$ is the set of jobs processed between the start and the completion of $j$ and $\mu_k$ the fraction of $j$ done before $k$ starts.
5. Eq. (3.11): the bound of Corollary 3.2 rewritten in terms of $N_1$, $N_2$ and $\mu_k$.
6. Lemma 3.6: $f$ is a density on $[0,1]$ with $\int_0^\eta f(\alpha)(1+\alpha-\eta)\,d\alpha \le (c-1)\eta$ and $\int_\mu^1 f(\alpha)(1+\alpha)\,d\alpha \le c(1-\mu)$ for $\eta, \mu \in [0,1]$.

Significance

Theorem 3.5 is a randomized $1.7451$-approximation for $1\,|\,r_j\,|\,\sum w_j C_j$, and simultaneously a bound on the integrality gap of (R): every instance has $\mathrm{OPT} \le 1.7451\, Z_R$. The paper also derandomizes it: there are at most $n$ distinct $\alpha$-schedules (its Proposition 3.8), and the best of them can be found in $O(n^2)$ time. The paper remarks that the truncated exponential density is optimal for its analysis and that the factor is tight for it.

On the formal side, the mission produces a reusable model of single-machine preemptive schedules, the LP schedule, $\alpha$-points and list scheduling, and the first machine-checked instance of the $\alpha$-point rounding technique that recurs across scheduling approximation. The result itself is proved in the paper; no machine-checked proof of it or of the LP-schedule identities (3.1), (3.10) is known to exist.

Difficulty

The obvious approach, bounding each $C^\alpha_j$ separately by a multiple of $t_j(\alpha)$, gives only the factor $\max\{1 + 1/\alpha, 1 + 2\alpha\}$ for fixed $\alpha$ (Theorem 3.3 of the paper), which is at least $1+\sqrt2$. The improvement needs the precise structure of the LP schedule around each job: which jobs interrupt $j$ ($N_2$) and which do not ($N_1$), and how the fraction $\eta_k(\alpha)$ of each other job depends on $\alpha$. Turning this structure into exact identities for piecewise-constant, piecewise-linear functions of $\alpha$ defined through a recursively built schedule is the bulk of the formal work. The analytic part (Lemma 3.6) is elementary but depends on the specific equation that defines $\gamma$.

Formalization scope

Jobs are Fin n (0-based) with $p, r : \texttt{Fin } n \to \mathbb N$ and real weights. The sortedness $w_j/p_j \ge w_k/p_k$ for $j \le k$, positivity $p_j > 0$ and $w_j > 0$ are hypotheses of every theorem about the LP schedule. Because the data are integral, the LP schedule is defined slot by slot on unit intervals $[\tau, \tau+1)$; a job's processing set is a finite union of such intervals. $\alpha$-points are infima over reals, and every statement restricts $\alpha$ to $(0,1]$. The $(\alpha_j)$-schedule's completion times are given by the closed form of list scheduling, $C_j = \max_{k \preceq j}(r_k + \sum_{k \preceq i \preceq j} p_i)$, with ties of $\alpha$-points broken by index (they do not occur for $\alpha \in (0,1]$). $Z_R$ is the infimum of the objective of (R) over its feasible set. The random $\alpha$ has law $f(\alpha)\,d\alpha$ on $\mathbb R$, and the expectation is a Lebesgue integral.

The goal asserts integrability of $\alpha \mapsto \sum_j w_j C^\alpha_j$ together with the bound, so the inequality cannot hold through the convention that a non-integrable function has integral $0$. The bound is against $Z_R$ defined from (R), not against $\sum_j w_j (M^{LP}_j + \tfrac12 p_j)$, which would build Theorem 2.5 into the goal; and the density's support $(0,\delta]$ is written out, so no mass is placed outside $(0,1]$. The running-time claims are not formalized, and the uniqueness of $\gamma$ is not asserted: the statements hold for every solution in $(0,1)$.

Useful infrastructure: finite unions of intervals and their measures, monotone piecewise-linear functions and their integrals, and list-scheduling identities. Contributions to any milestone, and general lemmas about the LP schedule (it is a preemptive schedule, has no idle time inside a job's span, processes interrupting jobs completely), are welcome.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2):165–192, 2002. doi:10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998. doi:10.1007/BF01585872
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 591–598, 1997 (no DOI; reference [11] of Goemans et al. 2002).
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1):146–166, 2001. doi:10.1137/S0097539797327180
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th IEEE FOCS, 32–43, 1999. doi:10.1109/SFFCS.1999.814574