The OR Formalization Drive

Motivation

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.

Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the $k$-server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.

Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove $w(S,d)=2n-1$ for every $n$-state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the $k$-server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between $H(n)$ and $2H(n)$, is the subject of the companion mission.

Setting

A task system $(S,d)$ has a finite set $S$ of $n$ states and a transition-cost matrix $d$ with $d(i,i)=0$, $d(i,j)>0$ for $i\neq j$, and the triangle inequality $d(i,j)+d(j,k)\ge d(i,k)$. It is metrical if also $d(i,j)=d(j,i)$.

A task $T$ is a vector of nonnegative processing costs $T(s)$, $s\in S$. Given a task sequence $\mathbf T=T^1\cdots T^m$ and an initial state $s_0$, a schedule is a map $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$; task $T^i$ is processed in state $\sigma(i)$, and the cost is

$$c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).$$

The off-line optimum $c_0(\mathbf T)$ is the minimum over all schedules. An on-line algorithm $A$ chooses $\sigma(i)$ knowing only $s_0$ and $T^1,\dots,T^i$; its cost is $c_A(\mathbf T)$. For $w>0$, $A$ is $w$-competitive if there is a constant $K_w$ with $c_A(\mathbf T)\le w\,c_0(\mathbf T)+K_w$ for every finite task sequence. The competitive ratio of $A$ is $w(A)=\inf\{w: A\text{ is }w\text{-competitive}\}$, and the competitive ratio of the task system is $w(S,d)=\inf_A w(A)$.

For the upper bound the paper also uses continuous-time schedules, in which task $T^i$ occupies the interval $[i,i+1)$ and the scheduler may change state at any real time, paying $\int_i^{i+1}T^i(\sigma(t))\,dt$ for processing. For a general (possibly asymmetric) matrix $d$, the cycle offset ratio $\psi(d)$ is the maximum over closed walks $s_0,\dots,s_k=s_0$ of $\sum_i d(s_{i-1},s_i)\big/\sum_i d(s_i,s_{i-1})$; it equals $1$ when $d$ is symmetric.

Formalization targets

Goal: Theorem 1.1

For every metrical task system $(S,d)$ with $n$ states,

$$w(S,d)=2n-1 .$$

The value depends on $n$ only, not on the distances.

Milestones

• Lemma 2.1. If $c_0(T^1\cdots T^m)\to\infty$ along an infinite task sequence $\mathbf T$, then $w(A)\ge w_{\mathbf T}(A)=\limsup_m c_A/c_0$.
• Theorem 2.2. Against the cruel taskmaster $M(\varepsilon)$, which charges $\varepsilon$ in the state the algorithm currently occupies,

$$w_{\mathbf T(\varepsilon)}(A)\ge\frac{2n-1}{1+\varepsilon/\min_{i\neq j}d(i,j)} .$$

• Lemma 3.1. Every on-line continuous-time algorithm is matched, on every task sequence, by an on-line discrete-time algorithm.
• Lemmas 6.3, 6.4, 6.2. Properties of the functions $f_k$ that drive the algorithm $A^*_d$: $f_k(s)-f_k(s')\le d(s',s)$; the identity $2\sum_{s\ne s_k}f_k(s)+f_k(s_k)=C_{k-1}+\sum_{i\le k}d(s_i,s_{i-1})$; and $f_k\le h_k$, the off-line cost at the $k$-th transition time.
• Theorem 6.1 (= Theorem 1.2). For every task system, symmetric or not, $A^*_d$ has competitive ratio at most $(2n-1)\psi(d)$.

Significance

The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat $2n-1$ on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives $(2n-1)\psi(d)$. The $2n-1$ lower bound is also the benchmark against which restricted models, such as paging and the $k$-server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.

The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.

Difficulty

The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant $2n-1$, rather than some $\Omega(n)$ bound, requires a sharp estimate of the off-line cost of that sequence.

The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined $f_k$ (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.

Formalization scope

States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all $n\ge1$, where $n=1$ gives $w(S,d)=1$. Task costs are finite nonnegative reals; the paper also allows $+\infty$ entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's $T^{i+1}$, and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending $(s_0,[T^1,\dots,T^i])$ to $\sigma(i)$, so on-line behaviour is built into the type. Competitiveness is written additively, $c_A\le w\,c_0+K$, with $K$ independent of the task sequence and of $s_0$.

The competitive ratio competitiveRatio d is the real infimum of the set of all $w$ for which some on-line algorithm is $w$-competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has $W_A=\emptyset$, whose real infimum is $0$, and that would drag $w(S,d)$ to $0$ for every system. Since the goal's value $2n-1$ is at least $1$ while the empty set's real infimum is $0$, the goal cannot hold vacuously.

Continuous-time algorithms are given as lists of $(\text{state},\text{length})$ pieces per unit interval; processing integrals are exact finite sums. The algorithm $A^*_d$ minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be $0$, its entry times are Option ℝ, and its cost is a sum in $[0,\infty]$, so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio $\psi(d)$ excludes closed walks that never move, and Theorems 2.2 and 6.1 require $n\ge2$, where $\min_{i\ne j}d(i,j)$ and $\psi(d)$ are defined. Lemma 3.1 is stated comparing $A$ with $A'$ (the printed statement says "as well as $A$").

A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining $A^*_d$. Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.

Selected references

• A. Borodin, N. Linial, M. E. Saks, An optimal on-line algorithm for metrical task system, Journal of the ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W

Who bears the inventory risk

A supplier and a retailer trade a product with a single selling season and uncertain demand. Someone has to decide, before demand is known, how many units exist, and someone has to be left holding the units that do not sell. With a push contract the retailer orders (prebooks) before the season and bears all of this risk; with a pull contract the supplier produces to stock and the retailer only orders during the season, so the supplier bears it. Both are single wholesale price contracts, the simplest and most common contracts in practice. Cachon (Management Science 50(2), 2004) asks which of these contracts two negotiating firms could plausibly agree on, independently of how they bargain, and answers it by computing the Pareto set of push and pull contracts together.

Push alone is the "selling to the newsvendor" problem studied by Lariviere and Porteus (MSOM 2001), whose unimodality result this mission uses. The novelty of §4 of Cachon's paper is to put push and pull contracts in one contract space and to show that the Pareto set then contains contracts of both kinds.

Setting

Demand has distribution function $F$ and density $f$. The paper's standing assumptions (§3, p. 225) are: $F(0) = 0$, $F$ strictly increasing, and the generalized failure rate $g(x) = x f(x)/(1 - F(x))$ strictly increasing (IGFR); the normal, exponential, gamma and Weibull laws qualify. Units cost $c$ to produce, sell at the retail price $p > c$, and are salvaged at $v < c$.

Expected sales with $q$ units available are $S(q) = q - \int_0^q F(x)\,dx$, and the integrated chain earns $\Pi(q) = (p - v)S(q) - (c - v)q$. It is maximized at the newsvendor quantity $q^o$, $F(q^o) = (p - c)/(p - v)$, with $\Pi^o = \Pi(q^o)$; the efficiency of a contract is $\Pi(q)/\Pi^o$.

A contract is described by the quantity $q$ it induces.

• Push at wholesale price $\hat w_1$: the retailer prebooks $q$ and earns $\hat\pi_r = (p - v)S(q) - (\hat w_1 - v)q$; the supplier earns $\hat\pi_s = (\hat w_1 - c)q$. The price inducing $q$ is $\hat w_1(q) = p - (p - v)F(q)$, and $\hat\pi_r(q)$, $\hat\pi_s(q)$ are the payoffs at that price.
• Pull at wholesale price $w_1 = w_2$: the supplier produces $q$ and earns $\pi_s = (w_1 - v)S(q) - (c - v)q$; the retailer earns $\pi_r = (p - w_1)S(q)$. The inducing price is $w_1(q) = (c - vF(q))/(1 - F(q))$.

Write $j(q) = S(q)/(1 - F(q))$ and $h(q) = f(q)/(1 - F(q))$ (the hazard rate). The retailer's preferred pull contract is $q^* = \arg\max \pi_r$ and the supplier's preferred push contract is $\hat q^* = \arg\max \hat\pi_s$.

A contract $k'$ Pareto dominates $k$ if no firm is worse off and one firm is strictly better off; the Pareto set consists of the contracts no other contract dominates.

A pull contract is only played as pull if the retailer does not prefer to prebook anyway. In the prebook game (§4.5) the retailer prebooks $y \ge 0$ and the supplier then chooses her production $Q \ge y$ to maximize $(w_1 - v)y + (w_2 - v)(S(Q) - S(y)) - (c - v)Q$. A pull contract survives the push challenge if the retailer's profit is strictly highest at $y = 0$.

Formalization targets

Goal: Theorem 6 with Lemma 5

There is a quantity $q^P$, $0 < q^P < q^o$, the unique positive quantity at which each firm is indifferent between the pull and the push contract, such that

$$\text{Pareto set} = \{\text{push}, \text{pull}\} \times [q^P, q^o],$$

and every pull contract with $q \in [q^P, q^o]$ survives the push challenge.

Milestones, in the order the proof uses them

• Eqs. (1)–(2), (3), (7): the newsvendor quantity $q^o$; the prices $\hat w_1(q)$, $w_1(q)$ induce $q$.
• Eqs. (5), (9) and Lariviere–Porteus: $\hat\pi_r$ and $\pi_s$ are increasing, $\hat\pi_s$ is unimodal.
• Lemma 1: $j(q)h(q)$ is increasing for $q > 0$. Theorem 2: $\pi_r$ is concave.
• Theorem 3: $\pi_r(q^*) > \hat\pi_s(\hat q^*)$, $q^* > \hat q^*$, $\Pi(q^*) > \Pi(\hat q^*)$.
• Lemma 4: $q^P$ exists, is the unique positive root of $\pi_r = \hat\pi_r$ and of $\pi_s = \hat\pi_s$, the unique maximizer of $\pi_r - \hat\pi_s$, and $q^P > q^*$.
• Eqs. (20)–(21) and Lemma 5: the supplier's reply to a prebook $y$ is $\max\{y, q_s\}$; pull contracts with $q \ge q^P$ survive the push challenge.

Significance

The theorem says that when both allocations of inventory risk are on the table, neither firm's preferred contract ($\hat q^*$ for the supplier, $q^*$ for the retailer) is Pareto, and the least efficient Pareto contract, $q^P$, is more efficient than the least efficient contract of either push-only or pull-only negotiation. In the Pareto set the supplier prefers every pull contract to every push contract and the retailer the reverse, so each firm earns more by bearing the risk itself. The results are proved in the paper, with the calculus informal, the unimodality of $\hat\pi_s$ cited, and half of Theorem 6's proof called "analogous". The mission produces a machine-checked version under exactly stated hypotheses; the IGFR concavity and single-crossing facts (Lemma 1, Theorem 2, Lemma 4) are reusable for other contract analyses. No part of this paper is formalized elsewhere; a related platform statement, Snyder–Shen Theorem 14.3 (SupplyChainTheory.wholesale_supplier_unimodal), is the Lariviere–Porteus lemma under stronger assumptions (nonnegative salvage value, finite mean, a continuous positive density, and only a weakly increasing failure rate).

Difficulty

The comparisons are between functions of different shapes: the supplier's push profit is a margin times a quantity, the retailer's pull profit a margin times expected sales. Signing derivatives needs the monotonicity of $j(q)h(q)$ (Lemma 1), and that fails to be routine at $q \to 0$, where $F$ need not be differentiable. The set equality compares four profit curves at once, and survival of the push challenge is a statement about a different game, the supplier's best reply to every prebook.

Formalization scope

Demand is a probability measure $\mu$ on $\mathbb R$ with $F$ = ProbabilityTheory.cdf μ. The predicate DemandModel μ f records $F(0) = 0$, $F$ strictly increasing on $[0, \infty)$, $F' = f$ on $(0, \infty)$, and $g'(x) > 0$ for $x > 0$. Differentiability is not required at $0$: the exponential law has a kink there, and it is the paper's own IGFR example. Prices satisfy $v < c < p$; no sign is imposed on $v$. Quantities range over $[0, \infty)$. The paper's $q^o$ is a parameter characterized by $F(q^o) = (p - c)/(p - v)$, and the first milestone proves it exists and is unique.

Profits are defined in the paper's primitive (quantity, price) forms composed with the inducing prices; the closed forms are milestones, not definitions.

Readings of informal words, each named in the item concerned:

• "increasing" in Lemma 1 and in Eqs. (2), (5), (9) is strict, as the proofs show; "concave" in Theorem 2 is strict concavity, as the proof shows via Lemma 1.
• "unimodal" means strictly increasing on $[0, \hat q]$ and strictly decreasing on $[\hat q, \infty)$ for some $\hat q > 0$.
• Uniqueness in Lemma 4 (i)–(ii) is over $q > 0$, since all profits vanish at $0$. Theorem 3 and Lemma 4 (v) hold for every maximizer, and the maximizers' existence is stated.
• Theorem 6's "includes all" is set equality, which its proof establishes. The survival conjunct comes from Lemma 5, which the proof's last sentence invokes.
• "prefers to prebook zero … rather than any positive amount" is strict preference.
• The contract space is the admissible contracts, $q \ge 0$ with wholesale price in $[c, p]$ (equivalently $0 \le q \le q^o$ in both modes). This is an explicit addition. The paper restricts prices to $\hat w_1 < p$ and $w_1 = w_2 < p$ and states that contracts with $q > q^o$ are Pareto inferior; but $\hat w_1 < p$ admits push with $q > q^o$ ($\hat w_1 < c$), where the retailer earns over $\Pi^o$ and nothing dominates.
• Eqs. (20)–(21) are stated for $w_2 > c$, which is what makes (21) solvable.

The statement does not follow trivially from a degenerate encoding. The demand assumptions are satisfiable, since the exponential law meets them. $q^o$, $q^P$, $q^*$ and $\hat q^*$ are shown to exist inside the statements that use them, and the Pareto set is taken over both modes and every admissible quantity, not only over the claimed interval.

Welcome contributions: basic facts about $S$, $j$ and $jh$ under the demand assumptions, reusable across the series' other two missions.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971

Motivation

A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.

The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.

Setting

Demand is a random variable with distribution function $F$ and density $f$. The paper assumes $F(0) = 0$, $F$ strictly increasing, and an increasing generalized failure rate (IGFR): $g(x) = x f(x)/(1 - F(x))$ has $g'(x) > 0$. Production costs $c$ per unit, the retail price is $p$, and leftover units are salvaged for $v$, with $v < c < p$. Expected sales with $q$ units available are

$$S(q) = q - \int_0^q F(x)\,dx,$$

and the integrated supply chain's expected profit is $\Pi(q) = (p - v)S(q) - (c - v)q$. It is maximized at $q^o$ with $F(q^o) = (p-c)/(p-v)$; write $\Pi^o = \Pi(q^o)$. The efficiency of a contract is $\Pi(q)/\Pi^o$, where $q$ is the quantity produced.

A contract is a pair of wholesale prices $\{w_1, w_2\}$ with $w_1 \le w_2$. The retailer first prebooks $y \ge 0$ units at $w_1$ each. The supplier, seeing $y$, produces $q \ge y$. During the season the retailer sells the prebook and, once it runs out, places at-once orders at $w_2$ per unit from the supplier's remaining stock, provided $w_2 \le p$. The supplier's and retailer's expected profits are

$$\pi_s(y, q) = (w_1 - v)y + (w_2 - v)(S(q) - S(y)) - (c - v)q,$$ $$\pi_r(y, q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)(S(q) - S(y)),$$

with the at-once terms absent when $w_2 > p$. An outcome of a contract is a pair $(y, q)$ where $q$ maximizes the supplier's profit given $y$, and $y$ maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push ($w_1 < p < w_2$), pull ($w_1 = w_2 \le p$) and advance-purchase discount ($w_1 < w_2 \le p$). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).

Formalization targets

Goal: Theorem 7

For every $w_1$ with $c \le w_1 \le p$, the contract $\{w_1, p\}$ has an outcome and is Pareto; every outcome $(y, q)$ of every Pareto contract satisfies

$$\Pi(q) = \Pi^o;$$

and for every $r \in [0, \Pi^o]$ some contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome with payoffs

$$\bigl(\pi_r, \pi_s\bigr) = \bigl(r,\ \Pi^o - r\bigr).$$

Milestones

1. Eq. (2): $\Pi$ is concave on $[0, \infty)$ and maximized exactly where $F(q^o) = (p-c)/(p-v)$.
2. Eqs. (20)–(21): for $c \le w_2 \le p$, the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - c)/(w_2 - v)$.
3. Eq. (22): for $c \le w_1 \le w_2 \le p$, $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$ is the unique maximizer of $\pi_r(\cdot, q)$.
4. Eq. (3): in push mode the retailer's optimal prebook solves $F(q) = (p - \hat w_1)/(p - v)$.

A further draft theorem states the step of the proof in which the retailer's outcome profit along $\{w_1, p\}$ falls strictly from $\Pi^o$ to $0$ as $w_1$ rises from $c$ to $p$.

Significance

The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces $q^o$; the prebook price then acts as a pure transfer. Every division of $\Pi^o$ is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.

The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.

Difficulty

The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when $w_2 = p$. Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook $y = 0$ always being available and on $w_1 \ge c$. Third, the division claim is surjectivity of the retailer's equilibrium payoff over $w_1 \in [c, p]$, which needs the solution of $F(y_r) = (p - w_1)/(p - v)$ to vary continuously with $w_1$, including at both ends ($y_r = q^o$ at $w_1 = c$, $y_r = 0$ at $w_1 = p$).

Formalization scope

Demand is a probability measure $\mu$ on $\mathbb R$ with $F$ = ProbabilityTheory.cdf μ. The standing assumptions are a structure: $F(0) = 0$, $F$ strictly increasing on $[0, \infty)$, $F' = f$ on $(0, \infty)$, and $g' > 0$ on $(0, \infty)$. Differentiability is required only on $(0, \infty)$, so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over $[0, \infty)$. $q^o$ is a parameter with the hypothesis $F(q^o) = (p-c)/(p-v)$; its existence is part of milestone 1.

Readings of informal words: "includes all" means every contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the $w_2 = p$ family; "any division is achievable" is surjectivity onto $[0, \Pi^o]$; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is $\max\{y, q_s\}$" is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when $w_2 \le p$ (p. 226, "with push $w_2 > p$, so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires $w_1 \ge c$ (p. 228 sets aside $\hat w_1 < c$ as Pareto inferior); pull includes $w_1 = w_2 = p$ (the paper's remark in the proof) and advance-purchase discounts include $w_2 = p$ (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.

Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of $\{w_1, p\}$ as $(y_r, q^o)$ would turn the goal into algebra, and is ruled out.

Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of $S$, and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• G. P. Cachon and M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445

Motivation

A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.

In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.

Setting

Demand $D$ for the season has law $\mu$ on $\mathbb R$, distribution function $F$ and density $f$. As in §3 of the paper, $F(0) = 0$, $F$ is strictly increasing on $[0,\infty)$, $F' = f$ on $(0,\infty)$, and the generalized failure rate $g(x) = x f(x)/(1 - F(x))$ is strictly increasing (IGFR). The expected sales from $q$ available units are

$$S(q) = q - \int_0^q F(x)\,dx .$$

The retail price is $p$, the unit production cost $c$, the salvage value $v$, with $v < c < p$.

A contract is a pair of wholesale prices $\{w_1, w_2\}$. Before production the retailer submits a prebook order of $y \ge 0$ units at $w_1$. The supplier then produces $q \ge y$. During the season, after running out of prebooked stock, the retailer places at-once orders at $w_2$, filled from the supplier's remaining stock. Pull is $w_1 = w_2 < p$; an advance-purchase discount is $w_1 < w_2$. In §5.1 the supplier pays an extra shipping and handling cost $\tau > 0$ per at-once unit. The profits are

$$\pi_r(y,q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)\bigl(S(q) - S(y)\bigr),$$ $$\pi_s(y,q) = (w_1 - v)y + (w_2 - \tau - v)\bigl(S(q) - S(y)\bigr) - (c - v)q .$$

A supplier best response to $y$ maximizes $\pi_s(y,\cdot)$ over $q \ge y$. An outcome of $\{w_1, w_2\}$ is a pair $(y, q)$ with $q$ a best response to $y$ and $y \ge 0$ maximizing $\pi_r$ when every alternative prebook is followed by a best response to it.

Formalization targets

Goal: Theorem 8

Fix $w_2 < p$ and $\tau > 0$, and suppose the retailer does not prebook under the pull contract $\{w_2, w_2\}$: $y = 0$ is his unique best reply, followed by the supplier's best response $q_0$. Then there is $w_1$ with

$$c < w_1 < w_2$$

such that $\{w_1, w_2\}$ has an outcome, and every outcome $(y, q)$ of it satisfies

$$\pi_r^{\{w_1,w_2\}}(y,q) > \pi_r^{\{w_2,w_2\}}(0,q_0), \qquad \pi_s^{\{w_1,w_2\}}(y,q) > \pi_s^{\{w_2,w_2\}}(0,q_0).$$

Milestones

1. Eq. (22): for $v < w_1 \le w_2 \le p$ the retailer's profit is concave in $y$ and uniquely maximized at $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$, whatever $q$.
2. Eqs. (20)–(21) with $w_2 - \tau$: the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - \tau - c)/(w_2 - \tau - v)$, independent of $w_1$, and $q_s$ is smaller than without the shipping cost.
3. §5.1: for fixed $w_2$ the retailer is never worse off with $w_1 \le w_2$ than with $w_1 = w_2$.
4. $y_r(w_1) > 0$ for every $w_1 < w_2$.
5. The derivative of $w_1 \mapsto \pi_s(y_r(w_1), q)$, where the density at $y_r(w_1)$ is positive:

$$\frac{d\pi_s(y_r(w_1), q)}{dw_1} = y_r(w_1) - \frac{(w_1 - v) - (w_2 - \tau - v)(1 - F(y_r(w_1)))}{(w_2 - v) f(y_r(w_1))}.$$

6. $y_r(w_1) \to 0$ as $w_1 \to w_2$, and, when $f$ has a positive right limit $f(0)$ at $0$, the derivative in 5 tends to $-\tau/((w_2 - v) f(0)) < 0$.

Significance

Without shipping costs, advance-purchase discounts with $w_2 = p$ coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.

The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at $0$ is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.

Difficulty

The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as $w_1 \to w_2$. That limit involves $f(0)$, which the model does not provide: $F$ is differentiable only on $(0, \infty)$, and for gamma demand with shape above $1$ the density vanishes at $0$, so the paper's limit is $-\infty$. A proof of the goal must therefore not rest on the limit display alone.

The second obstacle is the retailer's global choice. The calculus concerns prebooks $y_r(w_1)$ below the supplier's production $q_s$. Once $w_1 < w_2$, the retailer might instead prefer a prebook at least $q_s$, turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for $w_1$ close to $w_2$ requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at $y_r$.

Formalization scope

Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on $(0,\infty)$ only, so the exponential law is admitted. Quantities range over $[0, \infty)$. Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for $w_2 \le p$, and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue $w_2 - \tau$. The prebook function $y_r$ in milestones 5 and 6 is a function pinned on $(v, w_2)$ by Eq. (22), which determines it uniquely.

Readings of the paper's words:

• "the retailer does not prebook when $w_1 = w_2$" is read as "$y = 0$ is the retailer's unique best reply" (every $y > 0$ gives strictly less); with a tie the conclusion can fail;
• "profit increases for both" is read as a strict increase for both firms, in every outcome of the discounted contract;
• the conclusion $c < w_1$ strengthens "advance-purchase discount" ($w_1 < w_2$);
• "reduces the supplier's optimal production" (milestone 2) is a strict decrease; its formula is stated for $c \le w_2 - \tau$;
• "$f(0)$" in milestone 6 is the right limit of $f$ at $0$, assumed positive there only; the positivity of $f(y_r(w_1))$ in milestone 5 is the hypothesis of the implicit-function step;
• "never worse off" (milestone 3) compares every outcome of $\{w_1, w_2\}$ with every outcome of $\{w_2, w_2\}$.

A version of the goal that assumed $f(0) > 0$, assumed $y_r(w_1) < q_s$, compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with $\ge$, would be weaker than Theorem 8 and is not the target.

A complete development needs the concavity and first-order conditions for $S$, the inverse-function derivative for $F$, and the regime comparison between prebooks below and above $q_s$. The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere, E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971

Motivation

Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written $1|r_j|\sum C_j$), the problem is strongly NP-hard, so research has focused on approximation algorithms whose guarantees are stated against every feasible schedule.

The standard route runs through the preemptive relaxation. When jobs may be interrupted and resumed, the shortest-remaining-processing-time rule (SRPT) produces an optimal schedule, and its value is a lower bound for every nonpreemptive schedule. The question is how to turn that preemptive schedule into a nonpreemptive one without losing too much.

Timeline:

• 1995, Phillips, Stein and Wein (WADS 1995, pp. 86–97): order the jobs by their SRPT completion times and schedule them nonpreemptively in that order. This gives a 2-approximation. Later 2-approximations are by Hoogeveen and Vestjens (IPCO 1996), Stougie (1995), and Goemans (SODA 1997). Hoogeveen and Vestjens also showed that deterministic on-line algorithms cannot beat 2.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1)): order by $\alpha$-points instead of completion times, choose $\alpha$ at random, and take the best $\alpha$ off-line. This gives the $e/(e-1)\approx1.58$ bound for Best-$\alpha$ that is the goal of this mission, and an optimal randomized on-line algorithm.
• 1999, Afrati et al. (FOCS 1999): a polynomial-time approximation scheme for $1|r_j|\sum w_jC_j$. This settled the approximability of the problem, but the resulting algorithms are far from simple.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has a processing time $p_j>0$, a release date $r_j\ge0$, and, where the objective is weighted, a weight $w_j>0$. There is one machine.

A nonpreemptive schedule assigns each job a start time $S_j\ge r_j$ such that the intervals $[S_j,S_j+p_j)$ are pairwise disjoint. Its completion times are $C_j=S_j+p_j$.

A preemptive schedule $P$ specifies, for each time $t$, which job runs at $t$, if any. Job $J_j$ runs only at times $t\ge\max(0,r_j)$, receives exactly $p_j$ units of processing in total, and finishes by some finite time. Its completion time $C^P_j$ is the first time by which all of $J_j$ has been processed. For $\alpha\in(0,1]$, its $\alpha$-point $C^P_j(\alpha)$ is the first time by which $\alpha p_j$ units have been processed.

For a job $J_i$, $T_i$ denotes the idle time of $P$ before $C^P_i$. $x_{ij}$ denotes the fraction of $J_j$ processed before $C^P_i$. The paper writes $S^P_i(\beta)$ for the set of jobs with $x_{ij}=\beta$, and also for their total processing time.

One-machine list scheduling in a given order runs the jobs nonpreemptively in that order. Each job starts at the later of its release date and the completion of the previous job in the list. An $\alpha$-schedule is list scheduling in nondecreasing order of the $\alpha$-points $C^P_j(\alpha)$. $C^\alpha_j$ denotes the completion times of an $\alpha$-schedule.

Random-$\alpha$ draws $\alpha$ from a distribution on $(0,1]$ and outputs the $\alpha$-schedule. Best-$\alpha$ outputs the $\alpha$-schedule of smallest total completion time $\min_\alpha\sum_j C^\alpha_j$.

Formalization targets

Goal: Corollary 2.7

Let $P$ be optimal among preemptive schedules for $\sum_j C_j$. Then there is $\alpha\in(0,1]$ such that every $\alpha$-schedule derived from $P$ satisfies

$$\sum_j C^\alpha_j\;\le\;\frac{e}{e-1}\sum_j C_j\qquad\text{for every feasible nonpreemptive schedule } (C_j)_j .$$

Since Best-$\alpha$ returns a schedule no worse than this $\alpha$-schedule, Best-$\alpha$ is an $e/(e-1)$-approximation.

Milestones

1. The calculus behind the constant. For $f(\alpha)=e^\alpha/(e-1)$ and every $\beta\in(0,1]$,

$$\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha=\frac1{e-1}.$$

2. Lemma 2.2: $C^P_i=T_i+\sum_{0<\beta\le1}\beta S^P_i(\beta)$.
3. Lemma 2.3: $C^\alpha_i\le T_i+(1+\alpha)\sum_{\beta\ge\alpha}S^P_i(\beta)+\sum_{\beta<\alpha}\beta S^P_i(\beta)$.
4. Lemma 2.5: if $\alpha$ has density $f$ on $(0,1]$, then $E[C^\alpha_i]\le(1+\delta)C^P_i$ with $\delta=\max_{0<\beta\le1}\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha$.
5. Theorem 2.6, for the weighted objective with $P$ optimal among preemptive schedules: the expected approximation ratio of Random-$\alpha$ is at most $2$ for uniform $\alpha$, at most $1.8$ for $\alpha=1$ w.p. $3/5$ and $\alpha=1/2$ w.p. $2/5$, and at most $e/(e-1)$ for the density $e^\alpha/(e-1)$.

Companion statements, not milestones:

• the upper bound of Theorem 2.1, $\sum_jC^\alpha_j\le(1+1/\alpha)\sum_jC^P_j$;
• the existence of an optimal preemptive schedule.

Significance

The $e/(e-1)$ bound shows that conversion from the preemptive relaxation can beat the factor 2 of the natural ordering. It does so by exploiting that no single instance is bad for many values of $\alpha$ at once. The $\alpha$-point technique was also used with LP relaxations, for example by Goemans (SODA 1997) and by Schulz and Skutella. The randomized version is an optimal randomized on-line algorithm for $1|r_j|\sum C_j$. Lemma 2.3 is a statement about any preemptive schedule, so it applies wherever a good preemptive or fractional schedule is available.

All results of the mission are proved in the paper, except that the proof of Theorem 2.6, part 2 is omitted there. No machine-checked proof of them is known. A complete development would give a verified model of preemptive one-machine schedules, $\alpha$-points and list scheduling, together with the averaging argument over $\alpha$. These are reusable for the later results of the same paper and for the $\alpha$-point literature.

Difficulty

The obvious argument bounds each job's $\alpha$-schedule completion time directly against its preemptive completion time. That argument loses a factor $1+1/\alpha$ (Theorem 2.1), which is at least 2 for every fixed $\alpha$. The improvement needs Lemma 2.3. There the charge to each job depends on how much of it was done by $C^P_i$ relative to $\alpha$, and the idle time $T_i$ is not inflated at all. Proving Lemma 2.3 requires reasoning about a preemptive schedule as a measure on time, and about how moving pieces of jobs changes completion times. A proof that treats the preemptive schedule as a finite list of pieces must first show that nothing is lost by this discretization.

The averaging step needs the expectation over $\alpha$ to be an honest integral. The map $\alpha\mapsto C^\alpha_i$ must be shown integrable, which requires a fixed rule for ties between equal $\alpha$-points.

Formalization scope

• Model. Jobs are Fin n, time is real, $p_j>0$ and $r_j\ge0$. The paper admits $p_j=0$ only in its tightness instances.
  • A preemptive schedule is a function $\sigma:\mathbb R\to$ Option (Fin n) (none = idle). Each job's run set is measurable, lies in $[\max(0,r_j),\infty)$, is bounded above, and has Lebesgue measure $p_j$.
  • Completion times and $\alpha$-points are infima of nonempty sets that are bounded below.
  • $T_i$ is the measure of the idle set in $[0,C^P_i)$.
  • The paper's sums over $\beta$ are sums over jobs, weighted by the fraction $x_{ij}$.
• List scheduling is strict: jobs never overtake the list order, and the machine is free from time $0$.
  • Lemma 2.3, Theorem 2.1, Theorem 2.6.2 and the goal hold for every tie-break among equal $\alpha$-points.
  • The expectations (Lemma 2.5, Theorem 2.6.1 and 2.6.3) use the tie-break by job index. They assert integrability as part of the conclusion.
• Optimality. "Approximation ratio $c$" is stated as an inequality against every feasible nonpreemptive schedule, never against an infimum.
  • The optimality of $P$ among preemptive schedules is the paper's standing assumption for its upper bounds (p. 151). It appears as a hypothesis of Theorem 2.6 and of the goal.
  • The lemmas hold for arbitrary $P$ and do not carry it.
  • An existence statement shows the hypothesis can be met.
• Lemma 2.5's $\delta$ is replaced by any upper bound of the integrals over $\beta\in(0,1]$. This is equivalent, and it avoids assuming that the maximum is attained.
• Not stated:
  • the running time $O(n^2)$ of Best-$\alpha$ and the optimality of SRPT;
  • the tightness parts of Theorem 2.1 and Corollary 2.4, and the lower bounds of Theorem 2.9, which use zero-length jobs;
  • the on-line Theorem 2.8, which needs a model of on-line algorithms.
• Trivializing formalization ruled out. Dropping the optimality of $P$ from the goal would turn it into a statement about arbitrary preemptive schedules, which is Lemma 2.5, not Corollary 2.7. Comparing against $\sum_jC^P_j$ instead of every nonpreemptive schedule would likewise remove the content of the corollary.

Contributions are welcome at every level. The calculus milestone and Lemma 2.2 are good first targets.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• C. Phillips, C. Stein, J. Wein, Scheduling jobs that arrive over time, Proc. 4th Workshop on Algorithms and Data Structures (WADS), 1995, pp. 86–97 (reference [25] of the paper; no link verified).
• J. A. Hoogeveen, A. P. A. Vestjens, Optimal on-line algorithms for single-machine scheduling, Proc. 5th IPCO, 1996, pp. 404–414 (reference [21]; no link verified).
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 1997, pp. 591–598 (reference [12]; no link verified).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th FOCS, 1999 (reference [2]; no link verified).