Operations Research

Motivation

Competitive analysis compares an online algorithm, which must answer each request before seeing the next, with the optimal off-line solution of the same request sequence. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994) set up a general framework, request-answer games, in which paging, the $K$-server problem and metrical task systems are all instances, and used it to compare the power of randomized algorithms against several kinds of adversaries.

One of their results (Theorem 2.1) says that if a randomized algorithm is $\alpha$-competitive against every adaptive off-line adversary, then some deterministic algorithm is already $\alpha$-competitive. The argument is a game-theoretic existence proof: it says nothing about how to compute the deterministic algorithm. Section 4 of the paper, "A Constructive Version of Theorem 2.1", answers the natural follow-up question for a large class of games: under monotonicity, locality and a finite diameter, a deterministic algorithm that loses only a factor $1+\epsilon$ can be assembled from a finite object.

Setting

A request-answer game $F$ has a request set $R$, a finite answer set $A$, and cost functions $f_n : R^n \times A^n \to \mathbb{R}$, $n \ge 0$; $f_0$ is the cost of the empty play. The off-line optimum of a request sequence $r$ of length $n$ is $c(r) = \min_{a \in A^n} f_n(r, a)$. A deterministic online algorithm $G$ answers the $i$-th request by a function $g_i(r_1, \dots, r_i)$ of the requests so far; its cost on $r$ is $c_G(r) = f_n(r, G(r))$. It is $\alpha$-competitive if $c_G(r) \le \alpha(c(r))$ for every $r$.

The game is monotone if $f_{n+1}(rt, ab) \ge f_n(r, a)$ always, and local if for every $h > 0$ only finitely many request sequences have $c(r) \le h$. The discrepancy of two request-answer sequences is

$$\delta((r,a),(r',a')) = f(rr', aa') - f(r,a) - f(r',a'),$$

and the diameter $D(F)$ is the supremum of $|\delta|$ over all pairs.

For a real $H$, the set $R_H$ consists of the request sequences all of whose proper prefixes have off-line optimum at most $H$. Given a deterministic algorithm $A_H$, the restart algorithm simulates $A_H$ and, as soon as the request sequence leaves $R_H$, starts over as if it had received no previous requests. This cuts every request sequence into segments $r = r(1)\, r(2) \cdots r(t)$, each a longest prefix in $R_H$ of what remains.

Formalization targets

Goal: Theorem 4.1 through its construction

Let $F$ be monotone and local, with finite nonempty $R$ and $A$, $f_0 \ge 0$, and diameter at most $D$. Let $\alpha(x) = d\,x$ with $d \ge 1$, $\epsilon > 0$, and

$$H = \frac{(2+\epsilon) D}{\epsilon}.$$

Then $R_H$ is finite; the restart algorithm depends on $A_H$ only through its values on $R_H$; and for every $A_H$ with $c_{A_H}(r) \le \alpha(c(r))$ on $R_H$,

$$c_{\mathrm{Restart}}(r) \le (1+\epsilon)\,\alpha(c(r)) \qquad \text{for all request sequences } r.$$

Milestones (proof of Theorem 4.1, pp. 17–18)

1. $R_H$ is finite.
2. The restart rule produces the greedy decomposition into longest prefixes in $R_H$.
3. The restart algorithm answers $A_H(r(1)), A_H(r(2)), \dots, A_H(r(t))$.
4. $c(r(i)) \ge H$ for $i = 1, \dots, t-1$.
5. $c(r) \ge c(r(1)) + \sum_{i=2}^{t} (c(r(i)) - D(F))$.
6. $c_{\mathrm{Restart}}(r) \le \alpha(c(1)) + \sum_{i=2}^{t} (\alpha(c(i)) + D(F))$.

Significance

Theorem 2.1 shows that, against adaptive off-line adversaries, randomization gives no advantage, but only as an existence statement. Theorem 4.1 turns it into a recipe: a deterministic algorithm need only be good on the finite set $R_H$, which can be prepared in advance, and restarting extends it to all inputs at a loss of $1+\epsilon$. The paper illustrates this with $K$-server problems on finite graphs, where $A_H$ is a finite table and each step of the resulting algorithm costs one dynamic-programming evaluation of an off-line optimum.

The restart construction is of independent use: it is a general way to turn a guarantee on bounded-cost inputs into a guarantee on all inputs when the cost is nearly additive over concatenation.

To our knowledge neither the abstract request-answer game model nor this theorem has a machine-checked proof. The mission produces a formal model of request-answer games with the monotonicity, locality and diameter conditions, the restart algorithm as an explicit definition, and the full chain of inequalities of the proof.

Difficulty

The individual inequalities are elementary; the work lies in the bookkeeping of the construction. The algorithm is defined online, one request at a time, while the analysis is phrased through the decomposition of the whole sequence. Relating the two requires showing that the online rule produces exactly the decomposition into longest prefixes in $R_H$, and that the answers produced on each segment are those of $A_H$ run from scratch, so that the cost of the whole play can be compared with the costs on the segments. The constants must close exactly: with $H = (2+\epsilon)D/\epsilon$ the additive losses at the $t-1$ cuts, on both the algorithm's side and the optimum's side, must be absorbed by the factor $1+\epsilon$, and they do so only for ratios $d \ge 1$.

A tempting shortcut is to conclude Theorem 4.1 from Theorem 2.1 directly: a deterministic $\alpha$-competitive algorithm is trivially $(1+\epsilon)\alpha$-competitive when costs are nonnegative. This proves the sentence of the theorem without its point, and is ruled out below.

Formalization scope

• Request and answer sequences are Lean Lists, oldest first; $f_n(r,a)$ is F.cost r a with r.length = a.length. Costs are real-valued (the paper allows $+\infty$; real costs are a special case).
• The answer set is a Fintype and nonempty; in the goal the request set is a Fintype and nonempty.
• A deterministic algorithm is one function List R → A. Competitiveness of a deterministic algorithm against adaptive off-line adversaries is stated as competitiveness on every request sequence, which is equivalent for deterministic algorithms (p. 8).
• Finite diameter is a real bound $D$ with $|\delta| \le D$ for all pairs, and every statement holds for every such $D$, in particular $D = D(F)$; no real supremum is taken.
• $f_0 \ge 0$ is assumed in the goal; with monotonicity it makes every cost nonnegative. It holds in the paper's examples.
• $\alpha(x) = d\,x$ with $d \ge 1$ in the goal; the cost bound for the restart algorithm (milestone 6) holds for an arbitrary $\alpha$.
• $H$ is fixed to the paper's value $(2+\epsilon)D/\epsilon$.
• The restart algorithm is a definition (a left fold over the requests), not a hypothesis. The paper's assumption of a randomized algorithm competitive against adaptive off-line adversaries is used only, through Theorem 2.1, to obtain $A_H$; the goal quantifies over every $A_H$ that is $\alpha$-competitive on $R_H$. "Computable" has no precise meaning for real costs; its content is the finiteness of $R_H$ together with the fact that the restart algorithm reads $A_H$ only on $R_H$. A formalization that proves only the existence of a deterministic $(1+\epsilon)\alpha$-competitive algorithm, without the construction, does not meet the goal.
• Milestones 5 and 6 are stated for nonempty request sequences, so that $t \ge 1$; milestone 5 is stated for every decomposition into consecutive pieces.

Contributions welcome: proofs of the milestones, and a connection to the other missions of this series, where the randomized model and Theorem 2.1 are formalized.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994). https://doi.org/10.1007/BF01294260
• M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM Journal on Discrete Mathematics 4 (1991), 172–181. https://doi.org/10.1137/0404017

Motivation

Competitive analysis measures an online algorithm, which must answer each request before seeing the next, against the best off-line answer to the whole request sequence. Randomized online algorithms are often much better than deterministic ones against an oblivious adversary, who fixes the requests in advance; the paging problem is the standard example. Against an adaptive adversary, who sees the algorithm's answers before choosing the next request, the advantage can disappear.

Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; preliminary version STOC 1990) made this precise in an abstract framework of request-answer games. Their Corollary 2.1 says: if a game has a randomized algorithm that is $\alpha$-competitive against adaptive on-line adversaries and one that is $\beta$-competitive against oblivious adversaries, then it has a deterministic $\alpha\circ\beta$-competitive algorithm. That proof is non-constructive: it goes through a game-theoretic determinacy argument. Section 3 of the paper gives a constructive version. Most competitive analyses of randomized algorithms against adaptive adversaries are carried out with a potential function, in the style of Manasse, McGeoch and Sleator (J. Algorithms 11, 1990). The paper shows that such a potential function, together with any oblivious-competitive algorithm $H$, determines an explicit deterministic algorithm $M$, answer by answer. This mission formalizes that construction and its guarantee.

Setting

A request-answer game has a request set $R$, a finite answer set $A$ and cost functions $f_n : R^n \times A^n \to \mathbb R$. The off-line optimum of $r \in R^n$ is $c(r) = \min_{a \in A^n} f_n(r, a)$. A deterministic online algorithm $M$ is a sequence of maps $m_i : R^i \to A$; on $r = (r_1,\dots,r_n)$ it answers $M(r) = (m_1(r_1), m_2(r_1,r_2), \dots, m_n(r))$, at cost $c_M(r) = f_n(r, M(r))$. It is $\alpha$-competitive if $c_M(r) \le \alpha(c(r))$ for all $r$. Throughout, $\alpha$ and $\beta$ are affine maps $\mathbb R \to \mathbb R$ (the paper's "linear functions").

A randomized online algorithm $H$ is a probability distribution over deterministic algorithms $H_y$; it is $\beta$-competitive against any oblivious adversary if $\mathbb E_y[f_n(r, H_y(r))] \le \beta(c(r))$ for all $r$. The algorithm $G$ analysed by the potential function is described by its next-answer laws $g_{n+1}(r r_{n+1}, a)$ on $A$, given the requests so far, the new request and its own past answers. An adaptive on-line adversary $S$ chooses each request from the algorithm's past answers and answers it itself, before the algorithm does, for at most $d_Q$ rounds; a configuration after $n$ rounds is $(r, a, b) \in R^n \times A^n \times A^n$: requests, algorithm's answers, adversary's answers.

An augmented potential function for $\alpha$ and $G$ (Definition 3.1) is a family $\Phi_n : R^n \times A^n \times A^n \to \mathbb R$ with (1) $\Phi_0 = 0$; (2) $\Phi_n(r,a,b) \le \alpha(f_n(r,b)) - f_n(r,a)$ for every configuration; (3) $\mathbb E_{a_{n+1} \sim g_{n+1}(r r_{n+1}, a)}[\Phi_{n+1}(r r_{n+1}, a a_{n+1}, b b_{n+1})] \ge \Phi_n(r,a,b)$ for every configuration, every $r_{n+1} \in R$ and every $b_{n+1} \in A$.

Formalization targets

Goal: Theorem 3.1 (p. 15)

Let $\Phi$ be an augmented potential function for $\alpha$ and $G$, and $H$ a $\beta$-competitive algorithm against oblivious adversaries. Say that $M$ obeys the potential rule if for every $r \in R^n$ and $r' = rt$,

$$\mathbb E_y\big[\Phi_{n+1}(r', M(r)\,m_{n+1}(r'), H_y(r'))\big] \ \ge\ \mathbb E_y\big[\Phi_n(r, M(r), H_y(r))\big].$$

Then such an $M$ exists, and every such $M$ satisfies

$$c_M(r) \le \alpha\big(\beta(c(r))\big) \quad \text{for all } r .$$

Both parts are part of the goal: the rule can be followed, and following it guarantees $\alpha\circ\beta$-competitiveness.

Milestones

1. In every play of $G$ against an adaptive on-line adversary, the expected final potential is nonnegative (proof of Lemma 3.1).
2. Lemma 3.1, "if" direction: an augmented potential function for $\alpha$ and $G$ makes $G$ $\alpha$-competitive against any adaptive on-line adversary, $\mathbb E[c_G(S)] \le \mathbb E[\alpha(c_S(G))]$.
3. For every $r$, $t$ and every $a \in A^n$, some $a' \in A$ satisfies $\mathbb E_y[\Phi_{n+1}(rt, aa', H_y(rt))] \ge \mathbb E_y[\Phi_n(r, a, H_y(r))]$.
4. If $M$ obeys the rule, $\mathbb E_y[\Phi_n(r, M(r), H_y(r))] \ge 0$ for every $r$.
5. If $M$ obeys the rule, $f_n(r, M(r)) \le \mathbb E_y[\alpha(f_n(r, H_y(r)))]$ for every $r$: $M$ is $\alpha$-competitive against the randomized adaptive adversary that serves its requests with $H$.

Significance

The theorem turns two separate analyses into one deterministic algorithm with an explicit description. The potential function certifies $G$ against the strongest on-line adversary; the oblivious algorithm $H$ need not be related to $G$, and the paper remarks that $H$ may be $G$ itself. The next answer of $M$ is computable whenever the expected potential under $H$ is (Corollary 3.1, stated informally in the paper), and the paper notes that for the potential functions used in the $K$-server literature this expectation is computable in time polynomial in the number of nodes and $K$. Read in this light, a potential-function proof for a randomized algorithm doubles as a deterministic algorithm.

The result is proved in the paper. As far as is known, neither this theorem nor the abstract framework of request-answer games with adaptive adversaries has a machine-checked formalization. The mission produces that framework and a checked derandomization principle that applies to every request-answer game with real costs, not to one problem.

Difficulty

The obvious argument for the existence of $m_{n+1}(r')$ averages property (3) of $\Phi$; the work is in seeing which configuration to apply it to. The rule compares $M$'s configuration against $H_y$'s answers, not against an adversary playing $G$, and the paper argues through an auxiliary on-line adversary that asks $r'$ and serves it with $H_y$. Making this rigorous requires interchanging the expectation over $H$'s coins with the finite expectation over $G$'s next answer, and checking that the needed expectations are finite.

The second difficulty is the two kinds of randomness. $G$ enters only through its next-answer laws, while $H$ must be a single distribution over deterministic algorithms: the rule evaluates $H_y(r)$ and $H_y(r')$ with the same coins $y$. Replacing $H$ by a behavioural description breaks the coupling between consecutive rounds.

Formalization scope

Requests and answers are Lean lists, oldest first, and $f_n(r,a)$ is F.cost r a on lists of common length; values on lists of different lengths are never used. Costs are real: the paper allows $f_n = +\infty$, so every statement here is about the real-valued games. The answer type is finite and nonempty, so the minimum $c(r)$ exists. Affine maps are written $\alpha(x) = c x + d$. The goal additionally assumes $\alpha$ nondecreasing: the last step of the paper's proof applies $\alpha$ to an inequality, which needs it, and the paper's examples are positive ratios. In Lemma 3.1 and milestone 5 linearity of $\alpha$ is kept as the paper's standing convention, although with $\alpha$ inside the expectation the argument does not use it.

$G$ is a map from (requests, own answers) to a probability mass function on $A$ (behavioural form); its play against an adaptive on-line adversary is a probability mass function on final configurations, with finite support, and its expectations are finite sums. $H$ is a probability measure on a coin space with a deterministic algorithm per coin, each answer measurable in the coins; expectations over $H$ are Bochner integrals of functions with finitely many values. $\alpha$ stays inside expectations, as in the paper's definition of competitiveness against adaptive adversaries. Adversaries stop by returning none and have a uniform depth bound.

The goal cannot be satisfied vacuously: it states the existence of an algorithm obeying the rule alongside the guarantee for every such algorithm, and Definition 3.1 is required at every configuration, not only at reachable ones.

Not formalized: the "only if" direction of Lemma 3.1, which the paper only sketches, and Corollary 3.1, whose notion of computability the paper leaves unspecified. The definitions of request-answer games, online algorithms, adversaries and competitiveness are reusable for the other missions of this paper and for any problem-specific competitive analysis. Contributions welcome: proofs of the milestones, and a lemma relating the mixed and behavioural forms of a randomized algorithm.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994), 2–14. https://doi.org/10.1007/BF01294260
• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11 (1990), 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
• D. Sleator, R. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28 (1985), 202–208. https://doi.org/10.1145/2786.2793
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5

Motivation

A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the $n!$ strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the $c\mu$ rule.

That description uses one inequality for every nonempty set of classes, $2^n-1$ constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in $O(n^2)$ variables with $O(n^2)$ constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.

Setting

There are $n$ customer classes $E=\{1,\dots,n\}$. Class $i$ has arrival rate $\lambda_i>0$ and service rate $\mu_i>0$; its traffic intensity is $\rho_i=\lambda_i/\mu_i$, and the queue is stable: $\sum_{i\in E}\rho_i<1$. For $S\subseteq E$ define

$$b(S)=\frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i},\qquad b(\emptyset)=0 .$$

In the queue, $n_i$ is the steady-state mean number of class $i$ customers and $n_i/\mu_i$ their mean remaining work; $b(S)$ is the mean work of the classes in $S$ when those classes have preemptive priority over the rest.

The performance polymatroid P1 (Theorem 8.3) is the set of $(n_i)\in\mathbb R_+^n$ with

$$\sum_{i\in S}\frac{n_i}{\mu_i}\ge b(S)\quad (S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=b(E).$$

For a permutation $\pi=(\pi_1,\dots,\pi_n)$ of $E$, the vector $v(\pi)$ is the solution of the triangular system $\sum_{j=1}^{k}x_{\pi_j}/\mu_{\pi_j}=b(\{\pi_1,\dots,\pi_k\})$, $k=1,\dots,n$ (Eq. (58) with $f_i^S=1/\mu_i$).

The extended formulation P2 (Theorem 8.4) is the set of nonnegative $(n_i)_{i\in E}$ and $(I_{ij})_{i,j\in E}$ satisfying

$$\mu_iI_{ii}-\lambda_in_i=\lambda_i,\qquad \mu_iI_{ij}+\mu_jI_{ji}-\lambda_jn_i-\lambda_in_j=0\ (i\neq j),\qquad \sum_{i\in E}I_{ij}=n_j .$$

In the queue, $I_{ij}$ is the steady-state mean of the number of class $j$ customers on the event that the server is busy with class $i$. The projection $\mathrm{P2}'$ of P2 is the set of $(n_i)$ for which some $(I_{ij})$ makes $((n_i),(I_{ij}))$ a point of P2.

Formalization targets

Goal: Theorem 8.4

$$\mathrm{P2}'=\mathrm{P1}.$$

Both inclusions are part of the goal. The statement fixes no constants and holds for every $n$, every positive rate vector and every stable load.

Milestones

1. §8.2, proof of Theorem 8.3. The extreme points of P1 are exactly the vectors $v(\pi)$, and P1 is their convex hull:

$$\operatorname{ext}\mathrm{P1}=\{v(\pi)\},\qquad \mathrm{P1}=\operatorname{conv}\{v(\pi)\}.$$

2. §8.2, proof of Theorem 8.4. The easy inclusion, which the paper obtains from its Theorem 4.4:

$$\mathrm{P2}'\subseteq\mathrm{P1}.$$

Significance

The result. Theorem 8.4 replaces $2^n-1$ constraints by $O(n^2)$ constraints in $O(n^2)$ variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy $c\mu$ rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.

Formalizing it. The result is proved in the paper, but the reverse inclusion $\mathrm{P1}\subseteq\mathrm{P2}'$ is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific $b$. We know of no formalization of either result.

Difficulty

The inclusion $\mathrm{P2}'\subseteq\mathrm{P1}$ only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix $(I_{ij})$ satisfying $n^2$ linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries $I_{ij}$. The paper's own argument does not help here, since it produces $I$ as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints $I_{ij}\ge0$ are where the $2^n-1$ inequalities of P1 are encoded, and a proof has to explain how $O(n^2)$ sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.

Formalization scope

Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's $n_i$ is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j $=I_{ij}$, including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix $A^S_i=1/\mu_i$: inequality for every $S\neq E$, equality at $S=E$, nonnegativity. The paper writes $N$ for the class set $E$ in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound $n_i/\mu_i$, not $n_i$. $v(\pi)$ is given by its closed form, $v(\pi)_{\pi_k}=\mu_{\pi_k}\bigl(b(\{\pi_1,\dots,\pi_k\})-b(\{\pi_1,\dots,\pi_{k-1}\})\bigr)$, which solves (58). The standing hypothesis $\lambda_i>0$ is presupposed by the model (Poisson arrivals at rate $\lambda_i$); the load condition is the paper's stability condition and keeps every denominator of $b$ positive.

No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only $\mathrm{P2}'\subseteq\mathrm{P1}$, or assuming $\mathrm{P1}=\operatorname{conv}\{v(\pi)\}$ as a hypothesis of the goal, would not be Theorem 8.4.

A complete development needs: supermodularity of $b$ under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each $v(\pi)$. Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan School WP #3509-92-MSA, 1992; Annals of Applied Probability 4(1):43–75, 1994. https://doi.org/10.1214/aoap/1177005200
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3):810–821, 1980. https://doi.org/10.1287/opre.28.3.810
• J. G. Shanthikumar, D. D. Yao, Multiclass queueing systems: polymatroidal structure and optimal scheduling control, Operations Research 40(S2):S293–S299, 1992. https://doi.org/10.1287/opre.40.3.S293
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2):257–306, 1996. https://doi.org/10.1287/moor.21.2.257
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.

Motivation

Unconstrained submodular maximization (USM) asks for a subset $S$ of a finite ground set $\mathcal N$ maximizing a nonnegative submodular function $f$. It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because $f$ is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.

Timeline of the approximation ratio for USM in the value oracle model:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) showed that a uniformly random set achieves $1/4$, local search achieves $1/3$ and $2/5$, and that no algorithm making polynomially many queries achieves $1/2 + \varepsilon$ for any fixed $\varepsilon > 0$.
• Oveis Gharan and Vondrák (SODA 2011) reached $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) reached $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012) closed the gap with the double greedy algorithms: a deterministic $1/3$-approximation and a randomized $1/2$-approximation, both linear in the number of oracle calls. Their Appendix A gives a third, fractional variant, which is the subject of this mission.

This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.

Setting

Let $\mathcal N$ be a finite ground set with $n$ elements and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$. The function $f$ is submodular if

$$f(A) + f(B) \ge f(A \cup B) + f(A \cap B) \qquad \text{for all } A, B \subseteq \mathcal N .$$

Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ and let $OPT$ be a maximizing set.

The multilinear extension of $f$ is the function on vectors $x \in [0,1]^{\mathcal N}$

$$F(x) = \sum_{S \subseteq \mathcal N} f(S) \prod_{u \in S} x_u \prod_{u \notin S} (1 - x_u) = \mathbb E\bigl[f(R(x))\bigr],$$

where the random set $R(x)$ contains each element $u$ independently with probability $x_u$. A set is identified with its characteristic vector, so $F$ agrees with $f$ on $\{0,1\}^{\mathcal N}$, and $\{u\}$ also denotes the unit vector at $u$. For vectors, $x \vee y$ and $x \wedge y$ are the coordinate-wise maximum and minimum.

Algorithm 4 (MultilinearUSM). Fix an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and start from $x_0 = \emptyset$ and $y_0 = \mathcal N$ (the vectors $\mathbf 0$ and $\mathbf 1$). In iteration $i = 1, \dots, n$ compute

$$a_i = F(x_{i-1} + \{u_i\}) - F(x_{i-1}), \qquad b_i = F(y_{i-1} - \{u_i\}) - F(y_{i-1}),$$

set $a_i' = \max\{a_i, 0\}$, $b_i' = \max\{b_i, 0\}$, and update

$$x_i = x_{i-1} + \frac{a_i'}{a_i' + b_i'} \{u_i\}, \qquad y_i = y_{i-1} - \frac{b_i'}{a_i' + b_i'} \{u_i\},$$

with the convention that the two fractions are $1$ and $0$ when $a_i' = b_i' = 0$. The output is the random set $R(x_n)$. Every choice before the output is deterministic; the algorithm queries $F$ at four points per element.

For the analysis, $OPT_i = (OPT \vee x_i) \wedge y_i$.

Formalization targets

Goal: Theorem A.1, oracle-access clause

For every nonnegative submodular $f$ and every order of the ground set,

$$x_n = y_n \qquad\text{and}\qquad f(OPT) \le 2\,F(x_n) = 2\,\mathbb E\bigl[f(R(x_n))\bigr].$$

Milestones, in the order the proof uses them

1. $a_i + b_i \ge 0$ at every iteration (proof of Lemma A.2; the page cites Lemma II.1).
2. Endpoints: $OPT_0 = OPT$ with $F(OPT) = f(OPT)$, and $OPT_n = x_n = y_n$.
3. (4) and (5): if $a_i \ge 0$ and $b_i > 0$, then $F(x_i) - F(x_{i-1}) = a_i^2/(a_i+b_i)$ and $F(y_i) - F(y_{i-1}) = b_i^2/(a_i+b_i)$.
4. (6): in the same case, $F(OPT_{i-1}) - F(OPT_i) \le a_i b_i/(a_i + b_i)$, whether or not $u_i \in OPT$.
5. Lemma A.2: for every $1 \le i \le n$,

$$F(OPT_{i-1}) - F(OPT_i) \le \tfrac12\bigl[F(x_i) - F(x_{i-1}) + F(y_i) - F(y_{i-1})\bigr].$$

6. Telescoped display: $F(OPT_0) - F(OPT_n) \le \tfrac12[F(x_n) - F(x_0)] + \tfrac12[F(y_n) - F(y_0)] \le \tfrac12(F(x_n) + F(y_n))$.

Significance

The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor $1/2$ is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.

Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: $F$ is affine in each coordinate, its coordinate increments are antitone in the other coordinates on $[0,1]^{\mathcal N}$, and $F$ restricted to characteristic vectors is $f$. These are the standard tools of every continuous-relaxation argument for submodular maximization.

Difficulty

The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies $a_i + b_i \ge 0$ "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of $F$ along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining $F$. Second, inequality (6) is written out only for $u_i \notin OPT$, and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that $x_{i-1}(u_i) = 0$ and $y_{i-1}(u_i) = 1$ when it is touched, that $x_i \le OPT_i \le y_i$, and that every state stays in $[0,1]^{\mathcal N}$, where the antitonicity applies.

Formalization scope

• The ground set is a Fintype $X$ with decidable equality; sets are Finset X; $f$ is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$; $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT; $F$ is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every $x : X \to \mathbb R$.
• The order $u_1, \dots, u_n$ is a duplicate-free list containing every element; $u_i$ is the entry at index $i-1$, and $n$ is the list's length. The state after $i$ iterations is obtained by folding one step over the first $i$ entries from $(\mathbf 0, \mathbf 1)$. Statements hold for every such order.
• The footnote's convention $a_i'/(a_i'+b_i') = 1$, $b_i'/(a_i'+b_i') = 0$ when $a_i' = b_i' = 0$ is an explicit case split; with Lean's $0/0 = 0$ it would otherwise be reversed and the run would no longer end with $x_n = y_n$.
• Corrected slips of the page: lines 3–4 of Algorithm 4 assign $a_i', b_i'$ but define $a_i, b_i$; "$f : \mathcal N \to \mathbb R^+$" means $f : 2^{\mathcal N} \to \mathbb R^+$; "$F(x) \triangleq \mathbb E[R(x)]$" means $\mathbb E[f(R(x))]$; "NSM" in Theorem A.1 means USM. The main text's one-line definition of submodularity, read literally, forces monotonicity; the footnote's lattice form is used.
• Not formalized: the sampling clause of Theorem A.1 (ratio $(1/2) - o(1)$ without oracle access to $F$, whose proof the paper refers to Calinescu, Chekuri, Pál and Vondrák) and the running time. The guarantee is stated for the algorithm as printed, so the trivial existence of a $1/2$-approximation by exhaustive search does not satisfy it. A statement in which $x_n$ is an arbitrary point, or the state any process with $x_i \le y_i$, would not be this theorem.
• Contributions welcome: the multilinear-extension facts above as general lemmas, the run invariants, and proofs of the milestones in any order.

Selected references

• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012, 649–658. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205; its numbering differs and is not used here).
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, 1133–1153. https://doi.org/10.1137/090779346
• S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011, 1098–1117. https://doi.org/10.1137/1.9781611973082.83
• M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011, 342–353. https://doi.org/10.1007/978-3-642-22006-7_29
• G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6), 2011, 1740–1766. https://doi.org/10.1137/080733991

Why randomization matters in online algorithms

An online algorithm must answer each request before it sees the next one. Its performance is compared with an optimum that may choose all its answers after seeing the complete request string. Randomization can improve an online algorithm's guarantee when the request string is fixed in advance. The comparison changes when an adversary chooses later requests after seeing the algorithm's earlier answers. Ben-David, Borodin, Karp, Tardos and Wigderson studied these choices of adversary in a common request-answer model and proved a general relation between their competitive guarantees (Ben-David et al., 1994, manuscript §§2–3).

The paper distinguishes three adversaries. An oblivious adversary fixes the request string before the algorithm's random choices affect any answer. An adaptive off-line adversary chooses the next request from previous answers but serves the resulting request string optimally after the play. An adaptive on-line adversary also chooses its own answer as each request arrives. The ability to react to answers makes the latter two adversaries materially different from the oblivious one for randomized algorithms (Ben-David et al., 1994, manuscript pp. 7–9).

Request-answer games and competitive cost

A request-answer game has a request set $R$, a finite nonempty answer set $A$, and a real cost $f_n(r,a)$ for a request string $r\in R^n$ and an answer string $a\in A^n$. The off-line optimum for $r$ is $c(r)=\min_{a\in A^n}f_n(r,a)$. A deterministic online algorithm $D$ returns its $i$th answer from the first $i$ requests alone; it has no access to the rest of $r$ or to the eventual stopping time. Its cost on $r$ is $c_D(r)=f_n(r,D(r))$.

A randomized online algorithm is a distribution over deterministic online algorithms. With coins $\omega$, write $G_\omega$ for the resulting deterministic algorithm. For a fixed request string $r$, $G$ is $\beta$-competitive against oblivious adversaries when $\mathbb E_\omega[c_{G_\omega}(r)]\leq\beta(c(r))$. The paper calls a transformation “linear” when it has the affine form $x\mapsto ux+v$ (Ben-David et al., 1994, manuscript p. 7).

An adaptive off-line adversary $Q$ has a rule from prior answer strings to either the next request or a stop signal, together with a common finite upper bound on play length. Let $r(G_\omega,Q)$ denote its request string and $c_Q(G_\omega)=c(r(G_\omega,Q))$. Its competitiveness condition places the transformation inside the expectation: $\mathbb E_\omega[c_{G_\omega}(Q)]\leq\mathbb E_\omega[\alpha(c_Q(G_\omega))]$. An adaptive on-line adversary $S$ has the same request rule and an additional answer rule; its own cost is $c_S(G_\omega)$, and the corresponding condition uses $\mathbb E_\omega[\alpha(c_S(G_\omega))]$ on the right (Ben-David et al., 1994, manuscript pp. 8–9).

Formalization targets

Randomization against adaptive off-line adversaries

The first target is Theorem 2.1: if some randomized algorithm is $\alpha$-competitive against every adaptive off-line adversary, a deterministic algorithm has that same guarantee on every request string:

$$\exists G\;\forall Q,\quad \mathbb E[c_G(Q)]\leq\mathbb E[\alpha(c_Q(G))]\quad\Longrightarrow\quad\exists D\;\forall r,\quad c_D(r)\leq\alpha(c(r)).$$

Composition of two guarantees

Theorem 2.2 takes an $\alpha$ guarantee for $G$ against adaptive on-line adversaries and a $\beta$ guarantee for another randomized algorithm against oblivious adversaries. It concludes that $G$ has the composed guarantee against adaptive off-line adversaries:

$$\mathbb E[c_G(Q)]\leq\mathbb E[(\alpha\circ\beta)(c_Q(G))]\qquad\text{for every }Q.$$

The mission goal is Corollary 2.1, the deterministic consequence of these two results:

$$\exists D\;\forall r,\qquad c_D(r)\leq(\alpha\circ\beta)(c(r)).$$

The milestones follow the paper's two theorems and the stated claims in their proofs, including the finite-horizon winning-position formulation and the adversary that simulates a fixed online algorithm (Ben-David et al., 1994, manuscript pp. 9–13).

What the result supplies

The corollary turns the existence of two randomized guarantees under different information rules into the existence of a deterministic online strategy with an explicit composed cost transformation. It is an existence result: it does not say that the deterministic strategy can be computed efficiently from the randomized algorithms. The paper itself notes that such a construction is unavailable in full generality and then examines settings where constructive versions are possible (Ben-David et al., 1994, manuscript p. 13).

The mathematical results were proved in the 1994 paper; this mission asks for machine-checked Lean proofs of the abstract model, the intermediate claims, and Corollary 2.1. The local draft currently contains compiled statements with proof placeholders, so it does not yet provide checked proofs. A completed development would make the adversary distinctions and the exact placement of expectations available for reuse in later online-algorithm formalizations.

Why the proof is difficult

The apparent shortcut is to treat an adaptive request sequence as fixed and apply a guarantee against oblivious adversaries directly. That loses the dependence of later requests on the algorithm's earlier answers. For Theorem 2.1, a winning request strategy must have one finite horizon that works for every answer path; separate finite horizons for each branch do not suffice when the answer set is infinite. For Theorem 2.2, the simulated adversary must make its own answers before the algorithm answers the current request, while still matching a fixed online benchmark along every resulting play. The expectation inequalities must remain valid when the request string itself depends on the algorithm's coins (Ben-David et al., 1994, manuscript pp. 9–11).

Formalization scope

Lean represents requests and answers as oldest-first lists. List index zero is request one in the paper. The general game is a separate definition; the algorithm, adversary, and competitiveness definitions build on it. An off-line adversary's rule returns Option R, where none is the stop signal, and has a uniform finite depth bound. A randomized algorithm consists of a coin probability space and a deterministic prefix algorithm for each coin; its answer events are measurable. Finiteness of $A$ and bounded play depth make the cost of each fixed adversarial play take finitely many values, so its real expectation is an ordinary integrable expectation.

The formal game uses real-valued costs, a deliberate restriction of the paper's $\mathbb R\cup\{\infty\}$ costs. The answer set is finite and nonempty, while the request set may be infinite. The transformations $\alpha$ and $\beta$ are affine. Theorem 2.2 and the goal assume $\alpha$ is monotone: the paper applies $\alpha$ to an inequality in its proof, and its competitive-ratio examples have positive slope. Theorem 2.1 does not need this added assumption. The two randomized algorithms may have different coin spaces, each an arbitrary Lean type at the declaration's universe level. The off-line and on-line adaptive comparisons retain $\alpha$ inside the expectation.

The target ranges over every equal-length request and answer play generated by these rules, including an adversary that stops without a request. It does not allow the deterministic algorithm to see future requests or choose a different policy for each adversary. Reusable contributions include the game interface, bounded adaptive plays, measurable randomized algorithms, and finite-horizon winning positions. The statements of all three principal results, their intervening claims, and proofs of those statements are within scope.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos and A. Wigderson, On the Power of Randomization in On-Line Algorithms, Algorithmica 11, 1994. DOI: 10.1007/BF01294260. The local source is the authors' 20-page manuscript; citations above use its page numbers.

Motivation

An on-line algorithm must answer each request as it arrives, without knowing the requests to come; paging, caching, the $k$-server problem and metrical task systems are standard examples. Its quality is measured by competitive analysis: its cost is compared with the cost of an optimal off-line solution that knows the whole request sequence. For randomized on-line algorithms the comparison depends on how much the adversary producing the requests is allowed to see. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; conference version STOC 1990) introduced the three standard adversaries — oblivious, adaptive on-line and adaptive off-line — and related the competitive ratios achievable against each.

Their Theorem 2.2 (manuscript p. 10) shows that if a randomized algorithm is $\alpha$-competitive against adaptive on-line adversaries and some randomized algorithm is $\beta$-competitive against oblivious adversaries, then the first algorithm is $\alpha\beta$-competitive against adaptive off-line adversaries. This mission formalizes the paper's claim (manuscript p. 11) that this product bound cannot be improved in general, together with the explicit construction on pp. 12–13 that proves it.

Setting

A request-answer game consists of a request set $R$, a finite answer set $A$, and cost functions $f_n : R^n \times A^n \to \mathbb R$. For a request sequence $\underline r \in R^n$, the off-line optimum is $c(\underline r) = \min_{\underline a \in A^n} f_n(\underline r, \underline a)$. A deterministic on-line algorithm $G$ answers the $i$-th request with $a_i = g_i(r_1, \dots, r_i)$; a randomized one is a probability distribution over deterministic algorithms $G_x$, $x$ being the coin tosses.

An adaptive off-line adversary $Q$ chooses each request $r_{i+1} = q_i(a_1, \dots, a_i)$ from the answers given so far, stops after at most $d_Q$ requests, and pays the off-line optimum $c_Q(G) = c(\underline r)$ of the requests it made; the algorithm pays $c_G(Q) = f_n(\underline r, \underline a)$. An adaptive on-line adversary $S$ must in addition answer each request itself, before the algorithm does, with $b_{i+1} = p_i(a_1, \dots, a_i)$, and pays $c_S(G) = f_n(\underline r, \underline b)$. An oblivious adversary fixes $\underline r$ in advance and pays $c(\underline r)$. A randomized $G$ is $\alpha$-competitive against oblivious adversaries if $\mathbb E_x[c_{G_x}(\underline r)] \le \alpha\, c(\underline r)$ for all $\underline r$, and against adaptive on-line adversaries if $\mathbb E_x[c_{G_x}(S)] \le \mathbb E_x[\alpha\, c_S(G_x)]$ for all $S$.

The construction uses the mates game: $R = A$ is a set of $2t$ elements split into $t$ pairs of mates, and for $n \ge 2$ the cost depends only on the first answer $a_1$ and the second request $r_2$: it is $1$ if $a_1 = r_2$, $M$ if $a_1$ is the mate of $r_2$, and $m$ otherwise. The algorithm $G$ draws $a_1$ uniformly at random. The parameters solve

$$\beta = \frac{(2t-2)m + M + 1}{2t}, \qquad \alpha = \frac{1 + (2t-1)M}{2 + (2t-2)m}.$$

Formalization targets

Goal: tightness of Theorem 2.2

For $1 < \beta \le \alpha$ (or $\alpha = \beta = 1$) and every $C < \alpha\beta$, there are a game and a randomized algorithm $G$ such that

$$G \text{ is } \alpha\text{-competitive against adaptive on-line adversaries}, \qquad G \text{ is } \beta\text{-competitive against oblivious adversaries},$$

and for every randomized algorithm $K$ some adaptive off-line adversary $Q$ achieves

$$\mathbb E[c_Q(K)] > 0, \qquad \mathbb E[c_K(Q)] \ge C\cdot \mathbb E[c_Q(K)].$$

Milestones (pp. 12–13)

1. The closed forms $m(t)$, $M(t)$ are the unique solution of the two equations.
2. $m(t) \to \beta$ and $M(t) \to \alpha\beta$ as $t \to \infty$.
3. For all large $t$: $M(t) \ge \max(m(t)^2, C)$, $1 \le m(t) \le M(t)$, $\alpha(m(t)-1) \le M(t) - m(t)$.
4. $G$ is $\beta$-competitive against oblivious adversaries in the mates game.
5. $G$ is $\alpha$-competitive against adaptive on-line adversaries in the mates game.
6. An adaptive off-line adversary makes every algorithm pay $M$ while paying $1$.

Significance

The result. Together with Theorem 2.2, the claim pins down exactly how much the adaptive off-line adversary can gain over the other two: the product $\alpha\beta$ is an upper bound for every game and is approached by a single game for every admissible pair $(\alpha, \beta)$. It shows that no general argument relating the three adversary models can give a bound better than the product, so any improvement for a specific problem (paging, $k$-server) must use the structure of that problem. The paging example cited on p. 11 (RANDOM against the three adversaries) gives one instance of tightness; the mates game gives tightness for every admissible pair.

Formalizing it. The result is proved in the paper, in about one page, with two steps left to the reader ("by inspection of the equations", "a simple case analysis"). No machine-checked proof of this or of any statement about adaptive adversaries is known to us. The formalization makes the model of §2 precise (sequences, stopping, the order in which adversary and algorithm commit, expectations over coins), checks the asymptotics of the parameters, and verifies the case analysis, which on inspection needs an inequality the page does not state. Two printed formulas on p. 12 contain typos; the formal statements carry the correct values.

Difficulty

The construction is explicit, but each competitiveness claim quantifies over all adversaries, which may adapt their requests to the algorithm's random answers, stop at any time, and (for the on-line adversary) commit to their own answers in advance. The algebra of $\alpha$-competitiveness is tight: the adversary's best expected advantage is exactly zero, so every case of its best reply must be checked with no slack. The page's condition $M \ge m^2$ does not suffice for this: when $a_1$ is neither the adversary's first answer nor its mate, the reply "mate of $a_1$" beats the reply "the adversary's own answer" only when $\alpha(m-1) \le M - m$, which holds for the solved parameters but is not implied by $M \ge m^2$. At $\beta = 1 < \alpha$ the solved parameter $m$ is below $1$ for every $t$, and the oblivious bound fails.

Formalization scope

All declarations live in OnlineRandomization.Tightness. The conventions:

• Costs are real-valued; the paper allows $+\infty$, so the game class is a special case.
• Answer sets are nonempty finite types; request sets are arbitrary types.
• Sequences are Lean lists, oldest first; cost r a is $f_n$ on lists of equal length $n$.
• Adversaries return none for "stop" and carry a depth bound $d_Q$; an on-line adversary's answer $b_{i+1}$ depends only on $a_1, \dots, a_i$.
• Randomized algorithms are a probability space of coins with a deterministic algorithm per coin and measurable answers; expectations are Bochner integrals, with $\alpha$ applied inside the expectation. In the goal, coin spaces range over Type.
• Competitiveness uses the ratio functions $x \mapsto \alpha x$ and $x \mapsto \beta x$, with no additive constant.
• The mates game is on Fin t × Bool, with mate $(i, b) \mapsto (i, \lnot b)$. The paper leaves the costs of plays with fewer than two requests undefined; the formalization sets $f_0 = 0$ and $f_1 \equiv 1$ (with $f_1 \equiv 0$ the algorithm would not be $\alpha$-competitive).
• Range. The goal assumes $1 < \beta \le \alpha$ or $\alpha = \beta = 1$; the page's case $\beta = 1 < \alpha$ is not covered by its construction and is left out. In fact the claim is false there for $1 < C < \alpha$: an algorithm that is $1$-competitive against oblivious adversaries answers optimally, almost surely, on every request sequence (its cost is never below the optimum and its expected cost does not exceed it), and an adaptive off-line adversary reaches only finitely many request sequences, so against $K = G$ every adversary has $\mathbb E[c_G(Q)] = \mathbb E[c_Q(G)]$, a ratio of $1 < C$.

The positivity requirement $\mathbb E[c_Q(K)] > 0$ in the goal is essential: without it the adversary that asks nothing satisfies $\mathbb E[c_K(Q)] \ge C \cdot 0$ for every $K$, and the third clause would hold vacuously.

A complete development needs: finite expectations over a uniform coin, the evaluation of the play of an adversary against a constant algorithm, and limit and eventual-inequality arguments for rational functions of $t$. The model of §2 is shared with the other missions of this series and is reusable for any request-answer formulation of an on-line problem. Proofs of individual milestones are welcome.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994) 2–14. https://doi.org/10.1007/BF01294260 (cited from the authors' manuscript, manuscript pp. 7–13).
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5.
• P. Raghavan, M. Snir, Memory versus randomization in on-line algorithms, IBM Journal of Research and Development 38 (1994) 683–707. https://doi.org/10.1147/rd.386.0683

Counting lattice points in fixed dimension

How many integral points does a polytope contain? The question arises in integer programming, where it measures the size of a feasible set, in combinatorics, where many enumeration problems are lattice-point counts in a polytope (contingency tables, magic squares, flows), in the representation theory of Lie groups, and in the analysis of loop nests in compilers. Counting is #P-hard when the dimension is part of the input, so the natural question is whether the count can be computed in polynomial time when the dimension $d$ is fixed.

Timeline:

• 1899. In dimension $2$, Pick's formula leads to a polynomial algorithm.
• 1983. Lenstra shows that integer feasibility is decidable in polynomial time for fixed $d$ (Lenstra 1983). Deciding whether a lattice point exists does not count them.
• 1988, 1992. Brion proves that the exponential sum over the lattice points of a rational polytope is the sum of the exponential sums of its vertex cones.
• 1991. Dyer gives polynomial algorithms in dimensions $3$ and $4$, based on Dedekind sums (Dyer 1991).
• 1994. Barvinok proves that for every fixed $d$ the number of lattice points of an integral simplex, and hence of a rational polyhedron, can be computed in polynomial time (Barvinok 1994). The algorithm was later implemented (LattE, barvinok) and is the standard method.

Setting

Points of $\mathbb{R}^d$ have real coordinates and $\langle c,x\rangle=\sum_l c_lx_l$. For integral vectors $u_1,\dots,u_k\in\mathbb{Z}^d$, the rational cone they generate is $\operatorname{co}\{u_1,\dots,u_k\}=\{\sum_i\lambda_iu_i:\lambda_i\ge0\}$. The generators are simple if they are linearly independent, and primitive if moreover they form a basis of the lattice $\mathbb{Z}^d\cap\operatorname{Lin}\{u_1,\dots,u_k\}$.

The index $\operatorname{Ind}K$ of the cone given by simple generators is the number of integral points in the semi-open parallelepiped $\Pi=\{\sum_i\alpha_iu_i:0\le\alpha_i<1\}$. It equals $1$ exactly for primitive generators.

The exponential sum of $K$ is $\sigma(K;c)=\sum_{x\in K\cap\mathbb{Z}^d}e^{\langle c,x\rangle}$. Where it converges it has the closed form

$$\sigma(K;c)=\Bigl(\sum_{x\in\Pi\cap\mathbb{Z}^d}e^{\langle c,x\rangle}\Bigr)\prod_{i=1}^k\frac{1}{1-e^{\langle c,u_i\rangle}},$$

and this closed form defines $\sigma$ at every regular point, i.e. every $c$ with $\langle c,u_i\rangle\ne0$ for all $i$.

An integral simplex is $\Delta=\operatorname{conv}\{v_1,\dots,v_{k+1}\}$ with affinely independent $v_j\in\mathbb{Z}^d$. Its supporting cone at a vertex $v$ is $K_v=\{u:v+\delta u\in\Delta\text{ for all sufficiently small }\delta>0\}$. A signed decomposition $K=\sum_i\varepsilon_iK_i$ with integers $\varepsilon_i$ means $\chi_K=\sum_i\varepsilon_i\chi_{K_i}$ on all of $\mathbb{R}^d$. The constant term of the Laurent expansion of $f$ at $t=0$ is the coefficient of $t^0$ in the expansion of $f$ around its pole at $0$.

Formalization targets

Goal: the short signed formula (Theorem 1.2, mathematical content)

For $d\ge2$ and every integral simplex $\Delta\subseteq\mathbb{R}^d$ there are, for each vertex $v_j$, primitive cones $K_{j,i}$ and integers $\varepsilon_{j,i}$ with $K_{v_j}=\sum_i\varepsilon_{j,i}K_{j,i}$ and at most $(2^d)^{T_j}$ terms. Here $T_j$ is the smallest integer

$$T_j\ge\frac{-\log\log1.9+\log\log\operatorname{Ind}_j}{\log d-\log(d-1)},$$

and $\operatorname{Ind}_j$ is the index of the edge vectors at $v_j$. Moreover, for every $c$ orthogonal to no generator of any $K_{j,i}$,

$$\#(\Delta\cap\mathbb{Z}^d)=\sum_j\sum_i\varepsilon_{j,i}\,R(K_{j,i},v_j,c),$$

where $R(K,v,c)$ is the constant term at $t=0$ of $t\mapsto e^{t\langle c,v\rangle}\sigma(K;tc)$.

Milestones

1. Proposition 2.4 with Remark 2.5: the closed form of $\sigma$ for simple cones.
2. Proposition 4.1: for primitive cones, $\sigma(K;c)=\prod_i(1-e^{\langle c,u_i\rangle})^{-1}$.
3. Proposition 2.7 (Brion), for integral simplices.
4. Corollary 4.2: $R(K,v,c)=Q_k(x;y)\prod_ix_i^{-1}$ with $\deg Q_k\le k$.
5. Primitive generators iff $\operatorname{Ind}K=1$ (§5).
6. Lemma 5.2: a short lattice vector $w$ with $\operatorname{Ind}K_j\le(\operatorname{Ind}K)^{(d-1)/d}$.
7. Lemma 5.3: at most $2^d$ cones of smaller index, with signs $\pm1$.
8. Theorem 5.4: decomposition into at most $(2^d)^T$ primitive cones.
9. The display in the proof of Theorem 5.4: $(2^d)^T\le C_1(d)(\log\operatorname{Ind}K)^{C_2(d)}$.
10. Lemma 6.1: some $c(t)=(1,t,\dots,t^{d-1})$, $t\in\{0,\dots,m(d-1)\}$, is orthogonal to none of $m$ nonzero vectors.

Significance

The goal is the reason Barvinok's algorithm is polynomial. For fixed $d$, the number of terms is bounded by a polynomial in $\log\operatorname{Ind}K$, which is polynomial in the input size. Each term is an explicit rational function of inner products (Corollary 4.2). The identity therefore turns lattice-point counting into the evaluation of a short sum. Its consequences include polynomial-time counting for rational polyhedra in fixed dimension, polynomial-time computation of Ehrhart quasi-polynomials, and the theory of short rational generating functions (Barvinok–Woods), which underlies algorithms for parametric integer programming.

The result is proved and classical. As far as known it has not been machine-checked: Mathlib has convex cones, Minkowski's convex body theorem and lattices, but no signed cone decompositions, no generating functions of cones and no Brion identity. The mission produces a formal account of the algorithm's correctness and of the size of its output. Its milestones are statements of independent use: the closed form of cone generating functions, Brion's identity for simplices, and the index-reduction lemma.

Difficulty

The obvious approach is to triangulate the supporting cones into unimodular (primitive) cones. This fails: a cone of index $\operatorname{Ind}K$ may need about $\operatorname{Ind}K$ unimodular cones in any triangulation, which is exponential in the input size. The step that makes the count small is signed decomposition. Signed decomposition uses cones that are not contained in $K$, combined with signs $\pm1$, and controls the index through the geometry of numbers rather than through a subdivision of $K$. The second difficulty is that $c=0$, where the exponential sum equals the count, is a singular point of every $\sigma(K_i;\cdot)$. The count is recovered as a constant term of a Laurent expansion, so every identity has to be valid as an identity of meromorphic functions on regular points, and not only where the series converge.

Formalization scope

• Points of $\mathbb{R}^d$ are Fin d → ℝ, integral vectors Fin d → ℤ used through their real cast, and $\langle\cdot,\cdot\rangle$ is dotProduct. A cone is given by its generator list, because index, parallelepiped and the closed form of $\sigma$ depend on the generators. Logarithms are natural, and $|u|$ is the sup norm.
• Theorem 1.2 is represented by its mathematical content. The paper's statement is "there exists a polynomial time algorithm". No machine model is formalized. The goal is the identity proved on p. 778, with the count of the proof of Theorem 5.4 (p. 777). The algorithmic clauses of Lemmas 5.2, 5.3, 6.1 and Theorem 5.4 are each replaced by the existence statement of the object the algorithm constructs. Lemma 5.3(c), whose constant is unquantified, is omitted.
• Over $\mathbb{R}$. The paper uses $c\in\mathbb{C}^d$ only to speak of meromorphic functions. Here $c$ is real, $\sigma$ is defined by its closed form, and regularity means $\langle c,u_i\rangle\ne0$ for every generator. The constant term is a predicate: $t^Nf(t)$ agrees near $0$ with a real-analytic function whose $N$-th Taylor coefficient is the value.
• Added hypotheses. These are $d\ge2$ wherever $T$ appears, $k\ge1$ in Lemma 5.2, $d\ge1$ in Lemma 5.3, $u_i\ne0$ in Lemma 6.1, and $\operatorname{Ind}K\ge2$ in the display bound. $T=0$ when the index is $1$. Brion's identity is stated for integral simplices, the only case the proof uses.
• Trivializations ruled out. $\sigma$ is never an infinite sum, which would take a junk value off its convergence region. "Primitive" means a lattice basis and not mere linear independence; with the weaker notion the decomposition is trivial. Decompositions hold for every $x\in\mathbb{R}^d$, not only on $\mathbb{Z}^d$. The halfspace of Lemma 5.2 is linear, since an affine one would make it vacuous.
• Infrastructure. A complete development needs generating functions of simplicial cones, Brion's theorem for simplices, the identity theorem for rational functions in $e^{c_1},\dots,e^{c_d}$, Minkowski's theorem on a sublattice, and inclusion–exclusion for triangulations. Each is reusable beyond this mission, and contributions of any of these pieces are welcome.

Selected references

• A. I. Barvinok, A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed, Mathematics of Operations Research 19(4), 1994, 769–779. https://doi.org/10.1287/moor.19.4.769
• M. Brion, Points entiers dans les polyèdres convexes, Annales scientifiques de l'École Normale Supérieure 21(4), 1988, 653–663. https://doi.org/10.24033/asens.1572
• M. Dyer, On counting lattice points in polyhedra, SIAM Journal on Computing 20(4), 1991, 695–707. https://doi.org/10.1137/0220044
• H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4), 1983, 538–548. https://doi.org/10.1287/moor.8.4.538
• R. P. Stanley, Enumerative Combinatorics, Vol. 1, Wadsworth & Brooks/Cole, 1986, §4.6. https://doi.org/10.1007/978-1-4615-9763-6
• A. Barvinok, K. Woods, Short rational generating functions for lattice point problems, Journal of the AMS 16(4), 2003, 957–979. https://doi.org/10.1090/S0894-0347-03-00428-4