Theoretical Computer Science

Motivation

A high dimensional expander is a simplicial complex whose local structure forces global expansion. The high order random walks on such a complex move from a $k$-face to a $k$-face through a common $(k+1)$-face. They were studied for their connection to agreement tests in probabilistically checkable proofs (Dinur–Kaufman 2017; Kaufman–Mass 2017), and they later became a tool for sampling. Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) used the mixing bound of this mission to prove the Mihail–Vazirani conjecture: the bases-exchange walk of every matroid mixes rapidly.

Timeline:

• 1973. Garland (Ann. of Math. 97) shows that spectral gaps in the links of a complex control its cohomology. Inner products are localized to links; this is now called Garland's method.
• 2017. Kaufman and Mass (arXiv:1604.02947) bound the second eigenvalue of the high order walks on complexes with well-expanding links. Dinur and Kaufman obtain the optimal bound under a two-sided spectral gap in the links, as Kaufman–Oppenheim explain.
• 2018. Oppenheim (Discrete Comput. Geom. 59) shows how spectral gaps descend from top-dimensional links to lower ones ("trickling down").
• 2017–2021. Kaufman and Oppenheim (arXiv:1707.02799v3) obtain the optimal mixing bound under a one-sided gap only: negative eigenvalues of the links do not matter. This is the target of this mission.

Setting

Let $V$ be a type of vertices. A pure $n$-dimensional finite simplicial complex $X$ is a finite family of finite subsets of $V$ that is closed under subsets, has faces of at most $n+1$ elements, and has every face contained in a face of exactly $n+1$ elements. A face with $k+1$ elements is a $k$-face; $X(k)$ is the set of $k$-faces, and $X(-1)=\{\emptyset\}$.

A weight function is a map $m$ from the faces of $X$ to $(0,\infty)$ that is balanced: for $-1\le k\le n-1$ and $\tau\in X(k)$,

$$m(\tau)=\sum_{\sigma\in X(k+1),\ \tau\subseteq\sigma}m(\sigma).$$

A $k$-cochain is a function $\phi:X(k)\to\mathbb R$. The cochains carry the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ and the norm $\|\cdot\|$. The cochains orthogonal to the constants form $C^k_0(X,\mathbb R)=\{\phi:\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)=0\}$.

The upper random walk $M^+_k$ acts on $k$-cochains by

$$M^+_k\phi(\tau)=\frac{1}{k+2}\,\phi(\tau)+\sum_{\tau'\in X(k),\ \tau\cup\tau'\in X(k+1)}\frac{m(\tau\cup\tau')}{(k+2)\,m(\tau)}\,\phi(\tau').$$

It stays put with probability $1/(k+2)$, and otherwise moves to a neighbouring $k$-face with probability proportional to the weight of their union.

The link of a face $\tau$ is $X_\tau=\{\eta\in X:\eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$, weighted by $m_\tau(\eta)=m(\tau\cup\eta)$. On the vertices of $X_\tau$, the non-lazy upper walk $(M')^+_{\tau,0}=2M^+_{\tau,0}-I$ is the weighted random walk on the 1-skeleton of the link. Let $\mu_\tau$ be its second largest eigenvalue. $X$ is a one-sided $\lambda$-local spectral expander if $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$. The empty face is included, and its link is $X$ itself.

Formalization targets

Goal: Theorem 5.4 (p. 17)

Let $0\le\lambda\le1$ and let $X$ be a one-sided $\lambda$-local spectral expander. Then for every $0\le k\le n-1$ and every $\phi\in C^k_0(X,\mathbb R)$,

$$\|M^+_k\phi\|\le\Big(\frac{k+1}{k+2}+\frac{k+1}{2}\,\lambda\Big)\|\phi\|.$$

Milestones

They follow the paper's proof order:

• Lemma 3.6 and Corollary 3.7: the adjoint $d^*$ of the signless differential $d$, and the factorizations $d^*d=(k+2)M^+_k$, $dd^*=(k+1)M^-_k$.
• Proposition 4.1 (1)–(3), Garland's localization identities, and Proposition 4.2:

$$\|d\phi\|^2=\|d^*\phi\|^2+\|\phi\|^2+\sum_{\tau\in X(k-1)}\langle (M')^+_{\tau,0}(I-M^-_{\tau,0})\phi_\tau,\phi_\tau\rangle .$$

• Lemma 4.3, which bounds the link terms by $(k+1)\mu\|\phi\|^2$.
• Lemma 5.1.
• Theorem 5.2 (the Decomposition Theorem).
• Corollary 5.3, in its general and its one-sided form:

$$\|d\phi\|^2\le\sum_{j=0}^{k}\Big(k+1-j+\frac{(k+j+2)(k+1-j)}{2}\lambda\Big)\|\phi^j\|^2,\qquad \|\phi\|^2=\sum_{j=0}^k\|\phi^j\|^2.$$

Significance

The result. The coefficient $\frac{k+1}{k+2}$ is the baseline in the paper's mixing bound, and the bound is optimal up to the $O(\lambda)$ term. It needs a gap on one side only: links may have eigenvalues near $-1$. This matters in two places. The links of a matroid's independence complex are only one-sided expanders, so the matroid application needs exactly this case. And the links of Ramanujan complexes are one-sided expanders, so this bound gives optimal mixing on them; the two-sided bound of Dinur–Kaufman does not apply to them.

Formalizing it. The theorem is proved on paper; the Lean statements in this mission are proof targets. Completing the mission would give machine-checked proofs of the mixing bound, Garland's localization identities, and the Decomposition Theorem, built on definitions of weighted simplicial complexes, links, and their random walks. Lemma 4.3 and Corollary 5.3 are stated with a correction: as printed they are false when a link eigenvalue bound is negative (see Formalization scope).

Difficulty

The obvious argument fails. The tempting route bounds the second eigenvalue of $M^+_k$ directly from the link spectra, by induction on $k$. But $M^+_k$ has large eigenvalues near $\frac{k+1-j}{k+2}$ for every $j$, coming from cochains of the form $d\psi$ with $\psi$ of lower degree. A single spectral-gap estimate cannot separate these levels from one another. The paper instead splits $\phi$ into contributions from every degree $j\le k$; this is the Decomposition Theorem, and each piece is controlled separately. Formally, the main costs are:

• the double-counting behind Proposition 4.1 (Appendix A, pp. 28–29);
• a square root of a positive self-adjoint operator on a weighted finite-dimensional space (Theorem 5.2);
• the bookkeeping of degrees and links.

Formalization scope

Faces are Finset V. $X$ is a Finset (Finset V), and $X(k)$ is cells X (k + 1): faces are indexed by their number of vertices. Cochains are functions Finset V → ℝ that are read only on the relevant faces. Every operator is zero off $X$. The weight is positive on faces; the paper writes $\mathbb R^+$, and $m$ appears in denominators. Every goal-level statement carries the standing assumption of §2: $X$ is pure $n$-dimensional and $m$ is a weight. Orthogonality to the constants is always weighted by $m$ (or by $m_\tau$ in a link).

The adjoint $d^*$ is defined by its explicit formula; that it is the adjoint is Lemma 3.6. The eigenvalue condition $\mu_\tau\le\lambda$ is stated in Rayleigh form: $\langle (M')^+_{\tau,0}g,g\rangle\le\lambda\|g\|^2$ for every $g$ on the vertices of $X_\tau$ that is $m_\tau$-orthogonal to the constants. It is equivalent to the eigenvalue form even for disconnected links. A Rayleigh bound over all $g$, constants included, would be unsatisfiable for $\lambda<1$ and would make the goal vacuous; it is ruled out. The predicate quantifies over every face of dimension $-1$ to $n-2$, including $\emptyset$.

Corrections, all disclosed in the items:

• Lemma 4.3 is stated with a bound $\mu\ge\max(\mu_k,0)$. The printed version with $\mu_k<0$ fails already for the complete graph on three vertices.
• Corollary 5.3 accordingly takes $\mu_i\ge0$ and $\lambda\ge0$. Its two formal statements retain the page's assumption that every link of dimension at least one is connected, including $X$ itself.
• The proof of Theorem 5.4 ends with $(k+1)\lambda$; the statement's $\frac{k+1}{2}\lambda$ is formalized.

Welcome contributions: proofs of any milestone. Reusable lemmas on finite weighted inner products, on double counting over faces of a Finset (Finset V), and on links are useful beyond this mission; the companion mission on two-sided expanders uses the same objects.

Selected references

• T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
• N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: High-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
• H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Ann. of Math. 97:375–423, 1973. https://doi.org/10.2307/1970781
• T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
• I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete Comput. Geom. 59(2):293–330, 2018. https://arxiv.org/abs/1709.04431

Motivation

Distributed programs often establish a conversation among several participants, then exchange messages without waiting for each send to be received. A specification of each participant in isolation does not by itself say whether their actions will fit together. Multiparty asynchronous session types address this by describing the intended conversation once as a global type and checking each participant against a projected local type. Honda, Yoshida and Carbone develop this calculus and state a progress result for a restricted class of well-typed programs: if execution has not finished, another reduction is available. The restriction matters because independently initiated sessions can interfere and deadlock even when their communications are individually typed. Honda, Yoshida and Carbone (2016)

Setting

A program is a process before execution: it contains no message queues or restricted session channels, even after structural rearrangement, and it has no free session channels or process variables. A requester on a shared name $a$ starts a session with participants numbered $2$ through $n$. Each participant receives the same vector $\widetilde s$ of fresh session channels. An asynchronous send appends a message to the appropriate FIFO queue; a receive reads the queue head. Requests, sends, delegations and selections are emitting prefixes. Accepts, receives and branches are receiving prefixes. The reduction relation $P\longrightarrow Q$ includes these communications, conditionals, guarded declaration unfolding, and closure under parallel composition, restriction and structural congruence $\equiv$. Honda, Yoshida and Carbone (2016), Figs. 1–3 and Def. 2.1

A global type $G$ specifies which numbered role sends a value or choice to another role on channel index $k$, followed by the remainder of the conversation. It may also contain parallel components and guarded recursion. A partial projection $G\upharpoonright p$ gives role $p$ its endpoint type. Global types must be linear: causally ordered actions on a common channel have both input and output dependency chains. A global type is coherent when it is linear and projects to all its participants; the runtime typing $\Delta$ is coherent when each session family comes from such a global type. Honda, Yoshida and Carbone (2016), Defs. 3.12, 4.1–4.2 and 5.9

The runtime judgement $\Gamma\vdash P\triangleright_{\widetilde s}\Delta$ records the types of the process and the queue channels it mentions. Type contexts remember messages already in transit and compose with endpoint types. A process is queue-full when the channels in $\widetilde s$ equal the channels occurring in $\Delta$. A prefix is active when it is outside another prefix and outside either branch of a conditional, after permitted declaration unfolding. A process is well-linked when every reachable process has each active shared-name prefix in a redex. A process is simple when it has a typing derivation whose session environments obey the singleton and emptiness restrictions of Definition 5.25, with no delegation input or output rule. Honda, Yoshida and Carbone (2016), pp. 28–37

Formalization targets

The goal is Corollary 5.30. For every simple, well-linked program $P$ whose free names have shared sorts, and every reachable process $P'$,

$$P\longrightarrow^*P'\quad\Longrightarrow\quad P'\equiv 0\ \lor\ \exists P''\;P'\longrightarrow P''.$$

Here $0$ is inaction, and $P'\equiv 0$ includes completed sessions whose empty queues disappear by structural congruence. The milestones are the closed-typing preservation clause of Theorem 5.19(3), the linearity and message agreement clauses of Theorem 5.22, and the immediate-step claim of Proposition 5.29(1). Those are statements of the paper and give separate targets before the progress corollary. Honda, Yoshida and Carbone (2016), pp. 34–37

Significance

For the specified class of programs, progress excludes a reachable state that is neither finished nor reducible. It combines static endpoint information with the operational facts about queues and shared-name synchronisation. The communication-safety milestone also states that a value receive is paired with a value message of matching arity, channel reception with a channel vector of matching length, and branching with an offered label. These claims describe behavior of the paper's asynchronous multiparty calculus, rather than a property of a particular implementation. Honda, Yoshida and Carbone (2016), Theorem 5.22 and Corollary 5.30

The paper supplies mathematical proofs, but this mission's statements have no completed machine-checked proofs. Formalizing the result requires a precise account of the calculus, including queue messages, scope, recursive calls, type contexts, projection and the limited form of simplicity. The definitions can support later work on subject reduction and session fidelity in the same model. A contribution may prove any milestone or the goal, or improve the shared definitions while preserving the source's hypotheses and conclusions.

Difficulty

Typing each participant does not immediately give a reduction of their parallel composition. A send can be present while a receive is blocked by an earlier queue message, and a session initiation can be blocked by a shared-name prefix in a different session. Communication safety must relate active prefixes to a unique queue and its actual head message. Progress additionally needs the restrictions on derivations and shared-name links to rule out interference among sessions. The rules for structural congruence and declaration unfolding make the location of a redex depend on more than the outer syntactic constructor. Honda, Yoshida and Carbone (2016), §§5.4–5.5

Formalization scope

Lean uses natural numbers for role identifiers, shared names, channels, labels and process variables. Channel indices are one based, following $s[1..m]$. A global type, value sort and endpoint type are separate syntax classes; finite branch families are lists with nonempty, distinct labels where a well-formed type is required. Recursion is read equi-recursively by an endpoint bisimulation, and global-type linearity is checked on every finite unfolding. Projection returns an optional endpoint type so undefined projections cannot acquire a default value. The session typings are finite maps represented by association lists, with distinct roles and disjoint channel domains. The judgement's subscript $\widetilde s$ lists queue channels, while the domain of $\Delta$ lists all sessions under typing.

The formalization uses named process binders and a structural-congruence relation containing alpha conversion. Received-value and call substitution is capture avoiding under explicit freshness conditions. Expression evaluation is fixed to the ordinary Boolean connectives used in the paper's typing rules. Runtime typing includes the queue rules and the partial composition of type contexts. The restricted typing system for simplicity retains runtime queue rules and excludes both delegation directions. The paper prints “[RCV]” in Definition 5.25(2), but its appendix explicitly excludes “[SREC]”; this draft follows the appendix and records that reading in its audit notes. The result quantifies over actual programs and makes simplicity imply typability, so a free, blocked input or an untyped syntax check cannot satisfy the goal. Honda, Yoshida and Carbone (2016), Def. 5.25 and Appendix B.8

Every prefix rule acts on a singleton entry $\widetilde s:T@p$ (Notation 4.5); process-variable signatures carry one singleton entry per session vector, as in [VAR]; [SREC] receives the channel names it binds, without substitution (Remark 2.2). Proposition 5.29(1) and Corollary 5.30 are false as printed for open terms: a free name of sort bool used as a conditional guard, or a free process variable, is a stuck simple process. The formal statements therefore add that the free names of the process have shared sorts and, for Proposition 5.29(1), that it has no free process variables (a program has none by definition).

The development needs Mathlib's finite sets, lists and reflexive-transitive closure, plus its own definitions of the process calculus and typing judgements. The Lean declarations in this proposal are draft statements and definitions for review; they are not proofs of the paper's results.

Selected references

• Kohei Honda, Nobuko Yoshida and Marco Carbone, Multiparty Asynchronous Session Types, Journal of the ACM 63(1), Article 9, 2016. DOI 10.1145/2827695

Motivation

Multiparty communication protocols involve several participants who send messages over shared session channels. An implementation may send a later message before an earlier one has been received, so a written sequence of interactions does not by itself prevent a receiver from taking the wrong message. Honda, Yoshida, and Carbone use global types to specify the whole conversation and a linearity condition to rule out conflicting uses of a channel. Their condition is part of the type system that supports subject reduction and session fidelity in the same paper. Honda, Yoshida, and Carbone, 2016

Global types can contain recursion. Reading their full behaviour as a regular tree may therefore involve infinitely many copies of the same interaction. Proposition 3.13(1) says that checking just one finite unfolding suffices to determine whether every later finite unfolding satisfies the paper's linearity condition. This mission formalizes that proposition and the definitions on which its statement depends. Honda, Yoshida, and Carbone, 2016, §3.5 and Appendix A

Setting

A global type $G$ describes actions among roles $p,q$ on channels identified by positive indices $k$. Its constructors are a value communication $p\to q:k\langle U\rangle.G'$, a labelled branch $p\to q:k\{\ell_j:G_j\}_{j\in J}$, parallel composition $G_1\mid G_2$, recursion $\mu t.G'$, a recursion variable $t$, and termination $\mathrm{end}$. The carried value type $U$ may contain shared names whose sorts include another global type, or it may be a located end-point type. The formal syntax represents end-point sends, receives, selections, branches, recursion, variables, and termination because shared global types can occur within the sorts carried by those types. Honda, Yoshida, and Carbone, 2016, Figs. 4 and 6

An action node is an occurrence of a communication or branching action in the tree of a finite unfolding. Each node has a sender, receiver, and channel index. The action order $n_1\prec n_2$ holds when one action lies before another in the same continuation or branch, according to Definition 3.7. Actions in different branches or parallel components have no order solely because they appear next to each other in the syntax. Honda, Yoshida, and Carbone, 2016, pp. 15–16

The paper refines that order into three dependency relations. An II step matches receivers; an IO step connects a receiver to a later sender; and an OO step matches both sender and channel. An input dependency is a chain of IO steps ending in II. An output dependency is a nonempty chain of OO or IO steps. A finite type is linear when every ordered pair of actions on the same channel has both dependencies, including the corresponding condition on the global types carried within its values. The last II step matters because a chain ending at an output has not checked the ordering of the final input. Honda, Yoshida, and Carbone, 2016, Defs. 3.11–3.12

Write $G^{(n)}$ for the finite result of unfolding every recursion in $G$ $n$ times and replacing remaining recursion variables by $\mathrm{end}$. For a single recursion $G=\mu t.H$, the paper gives $G^{(0)}=H[\mathrm{end}/t]$ and $G^{(n+1)}=H[G^{(n)}/t]$. Unfolding does not enter carried types. The one-time unfolding is $G^{(1)}$. Honda, Yoshida, and Carbone, 2016, p. 20 and Notation A.1

Formalization targets

The milestone is the direction the paper calls the “if-direction”: for a well-formed global type and a positive unfolding index, linearity at that index implies linearity at the first one.

$$\operatorname{WellFormed}(G)\ \land\ n\ge 1\ \land\ \operatorname{Linear}(G^{(n)}) \quad\Longrightarrow\quad \operatorname{Linear}(G^{(1)}).$$

The mission goal is Proposition 3.13(1), the equivalence between the first unfolding and any positive unfolding.

$$\forall G\text{ well formed}\,\forall n\ge 1,\qquad \operatorname{Linear}(G^{(1)}) \quad\Longleftrightarrow\quad \operatorname{Linear}(G^{(n)}).$$

The lower bound $n\ge1$ is essential. The paper explicitly begins its Appendix A induction at $n=1$ and gives examples that satisfy linearity at the zeroth unfolding but fail after one unfolding. Proposition 3.13(2), the paper's decidability claim, is outside this mission: formalizing computational decidability would require an effective representation and decision procedure rather than a classical Decidable instance. Honda, Yoshida, and Carbone, 2016, p. 20 and Appendix A

Significance

The proposition turns a property stated over arbitrarily deep recursive behaviour into a fixed finite test. It supports the paper's decidability result and supplies the channel-ordering premise used later in coherent global types and runtime typing. Without the stabilization claim, checking a recursive global type by inspecting one finite copy would leave later channel conflicts unresolved. Honda, Yoshida, and Carbone, 2016, Props. 3.13–3.14 and Def. 4.2

The result is already proved in the paper. The formalization work is to give the paper's finite unfolding, action order, dependency chains, and recursive carried-type condition exact Lean meanings, then verify the equivalence against those meanings. The local mission currently contains open theorem statements and compiled definitions; it does not claim a machine-checked proof of Proposition 3.13(1). Those definitions can also be reused when formalizing the paper's coherence and subject-reduction results.

Difficulty

The main obstacle is the interaction between recursion and causality. Unfolding creates further occurrences of actions, while an input dependency requires a chain with a specific final II edge and an output dependency allows only OO or IO edges. The action order also depends on a node's place in a branch, continuation, or parallel component. Merely comparing channel labels across two unfoldings does not establish the required dependencies. The carried-type condition adds another level: unfolding the outer type leaves its carried types intact, but their own linearity must still be checked. Honda, Yoshida, and Carbone, 2016, Defs. 3.7, 3.11–3.12 and Appendix A

Formalization scope

Lean represents roles, labels, type variables, and channel indices by natural numbers, with channel indices interpreted as one-based. Branches are lists; WellFormed G records nonempty branches with distinct labels, closed guarded recursion, positive channel indices, and distinct sender and receiver, also checking carried global types. Both theorem statements assume it to make the paper's standing syntax conventions explicit. The sort grammar includes Boolean and natural-number sorts, shared-name sorts, and coded additional base sorts for the paper's ellipsis. The recursion constructor is named mu and the sort type SType because rec and Sort have special meanings in Lean.

Node names are finite child-index paths. Prec is the transitive closure of the five clauses of Definition 3.7. Every II, IO, or OO step includes this order. Input dependency requires at least one step, resolving the printed $n\ge0$ against the same sentence's mandatory final II step. Carried types are reached through value and end-point type syntax, and nested carriers are included transitively. Linear checks each such carried type at every finite unfolding. The definitions also encode the paper's positive-index and non-reflexive interaction conventions in WellFormed. A linearity predicate that ignores carried types or treats separate parallel components as ordered would change the target theorem. Honda, Yoshida, and Carbone, 2016, pp. 12–13, 16, 19–20

Useful contributions include results about finite unfolding and the action order, preservation of labels at recurring positions, and dependency-chain properties under unfolding. The two folding claims in Appendix A are not listed as milestones here because a faithful folding operation for nested recursion and multiple occurrences has not yet been specified. Their absence is a scope limit on the attack path, not an assumption in the goal.

Selected references

• Kohei Honda, Nobuko Yoshida, and Marco Carbone, Multiparty Asynchronous Session Types, Journal of the ACM 63(1), Article 9, 2016. DOI: 10.1145/2827695.

Motivation

Scheduling jobs on parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$ is a basic model of service and computing systems. Two features of practice are hard to combine with performance guarantees: jobs are not known in advance but arrive over time, and their processing times are random, with only their distributions known when they arrive. Machines are moreover often unrelated: a job's processing time distribution depends arbitrarily on the machine, and some jobs cannot run on some machines at all.

Gupta, Moseley, Uetz and Xie (arXiv:1703.01634, Math. Oper. Res. 2020) give the first performance guarantee for this combination: a simple greedy policy whose expected cost is within a factor depending only on the variability of the processing times of the best nonanticipatory policy, which knows all jobs in advance.

Timeline. For deterministic jobs arriving over time, Hall, Schulz, Shmoys and Wein (1997) gave an 8-competitive algorithm on unrelated machines. Megow, Uetz and Vredeveld (2006) introduced the stochastic online model and analysed greedy policies on identical machines with modified release dates. Skutella, Sviridenko and Uetz (2016) gave LP-based approximation algorithms for offline stochastic scheduling on unrelated machines, with guarantees linear in the squared coefficient of variation. The present paper (conference version IPCO 2017) treats the online, stochastic, unrelated case with release dates.

Setting

There is a finite set $M$ of machines and jobs $j=1,\dots,n$. Job $j$ is released at an integer time $r_j\ge0$, jobs are indexed so that $r_1\le\dots\le r_n$, and job $j$ has weight $w_j\ge0$. If job $j$ runs on machine $i$ its processing time is a random variable $P_{ij}$ with values in $\{0,1,2,\dots\}$; on forbidden pairs the page writes $\mathbb E[P_{ij}]=\infty$, and every job has an allowed machine. On allowed pairs $\mathbb E[P_{ij}]\ge1$ and the variance is finite. Different jobs are independent; one job's times on different machines need not be. The squared coefficient of variation is $\mathbb{CV}[P_{ij}]^2=\operatorname{Var}[P_{ij}]/\mathbb E[P_{ij}]^2$, and $\Delta$ bounds it on every allowed pair.

A policy decides, for each job, a machine and a start time; jobs are nonpreemptive and a machine runs one job at a time. It is nonanticipatory if its decisions up to time $t$ use only what is known at $t$: the processing time of a job is learned when the job completes. $\mathsf{OPT}$ is the least expected cost $\mathbb E[\sum_jw_jC_j]$ of a nonanticipatory policy that knows all jobs, release dates and distributions in advance.

The greedy algorithm (§6.1) is first defined for deterministic times $p_{ij}$. On machine $i$ job $j$ gets the modified release date $r_{ij}=\max\{r_j,c\,p_{ij}\}$. On arrival, job $j$ is assigned to a machine $m(j)$ minimizing an explicit upper bound $\operatorname{cost}(j\to i)$ on the increase of the objective (Definition 4), and each machine runs WSPT (largest $w_k/p_{ik}$ first) among its jobs whose modified release dates have passed. Run on $p_{ij}=\mathbb E[P_{ij}]$ with $c=\frac23$ it yields the nominal schedule $(m,s)$. The stochastic greedy policy (§6.3) keeps $m$ and the nominal order on each machine, and starts the $\ell$th job on machine $i$ at $S_{i,\ell}=\max\{s_{i,\ell},S_{i,\ell-1}+P_{i,\ell-1}\}$, never before its nominal start. Its expected cost is $\mathsf{ALG}$, and

$$h(\Delta)=1+\tfrac{\sqrt\Delta}2\ (\Delta\le1),\qquad h(\Delta)=1+\tfrac{\Delta}{\Delta+1}\ (\Delta\ge1).$$

Formalization targets

Goal: Theorem 4

$$\mathsf{ALG}\;\le\;(7.216+3.608\,\Delta)\,h(\Delta)\,\mathsf{OPT}.$$

The goal is stated against every admissible nonanticipatory policy, for every tie-breaking of the greedy algorithm.

Milestones

1. Lemma 6: the deterministic greedy schedule has $\mathsf{ALG}\le\sum_j\operatorname{cost}(j\to m(j))$.
2. Lemma 7, feasibility: with $\alpha_j=\operatorname{cost}(j\to m(j))$, $\beta_{i,t}$ the weight of jobs on machine $i$ released by $t$ and unfinished at $t$, and the speed-scaled values (12), $(\alpha^f/a,\beta^f/b)$ is feasible for the dual $(\mathrm D_r)$ when $af\ge2(2+c)$, $1/c\le f(a-1)$, $af\ge b$.
3. (13): $z^{P_r}\le(1+\frac\Delta2)z^{S_r}\le(1+\frac\Delta2)\mathsf{OPT}$ for the time-indexed relaxations with release dates.
4. Lemma 10: $\mathbb E[(X-\mu)^+]\le\mu\sqrt\Delta/2$ for $\Delta\le1$ and $\le\mu\Delta/(\Delta+1)$ for $\Delta\ge1$.
5. Lemma 8: $\mathbb E[S_j]\le h(\Delta)\,s_j$ for every job.

Significance

The result. Theorem 4 is the first constant-factor guarantee, for fixed $\Delta$, for stochastic online scheduling on unrelated machines with release dates, and it is achieved by a combinatorial policy that needs no LP solution. For deterministic jobs ($\Delta=0$, $h=1$) it gives a deterministic 7.216-competitive algorithm (Theorem 3), improving the ratio 8 of Hall et al.; for exponential processing times ($\Delta=1$) the factor is $(7.216+3.608)\cdot\frac32$. The order $O(\Delta)$ matches earlier offline results on unrelated machines and online results on identical machines.

Formalizing it. The result is proved on paper and has no machine-checked proof. A formalization needs nonanticipatory policies with machine choice, a time-indexed LP relaxation with countably many variables and its weak duality, and a dual-fitting argument. It also exposes a gap: the second sentence of Lemma 7, the bound $z^{D_r}(\alpha^f/a,\beta^f/b)\ge\mathsf{ALG}/(7+\frac{11}{51})$, fails as printed. On one machine with jobs $r=(0,0,0,5)$, $p=(\frac54,\frac54,1,3)$, $w=(2,1,\frac1{1000},\frac1{100})$ the greedy schedule has $\mathsf{ALG}=\frac{6049}{600}$ while $z^{D_r}=\frac{8879}{6400}<\mathsf{ALG}/(7+\frac{11}{51})=\frac{4471}{3200}$. The step $\sum_{i,s}\beta^f_{is}=\mathsf{ALG}/f$ counts a job at $\lfloor C_k/f\rfloor-\lceil r_k/f\rceil+1$ integer slots, up to one more than $C_k/f$. A complete proof of the goal has to close this gap.

Difficulty

Three parts are hard. First, the comparison is with an optimal adaptive policy, so the lower bound has to come from a relaxation that every nonanticipatory policy satisfies in expectation. Writing the time-indexed LP for policies that choose machines at start time, idle deliberately and start at real times, and showing it is a relaxation, requires nonanticipation and job independence to decouple a job's machine from its own processing time. Second, the dual fitting runs through a speed-scaled instance with a non-integer speed $f=\frac{23}6$, so the dual's integer slots and the schedule's real times do not align; this is where the printed objective bound breaks. Third, the obvious stochastic policy, WSEPT list scheduling without forced idleness, fails: Remark 2 of the paper gives an instance where it has $\mathbb E[C]=\Omega(n)$ against $O(1)$. The analysis therefore has to work with deliberately delayed starts.

Formalization scope

Machines are a Fintype, Nonempty type; jobs are Fin n in release order. Processing times are ℕ-valued measurable functions on a probability space, with finite second moment and mean at least one on eligible pairs, and with jobs independent (iIndepFun over jobs of the machine-indexed vectors). Forbidden pairs are an eligibility relation, never a zero or junk mean. Release dates are natural numbers: the relaxation of §6.2 has integer slots $s\ge r_j$, and (13) is false for a fractional release date. Weights are nonnegative; $\Delta$ is any upper bound on the squared coefficients of variation, which is at least as strong as the page's maximum.

$\mathsf{OPT}$ is never written as an infimum. The goal and (13) quantify over every admissible policy: a map from realizations to machines and real start times that is feasible (eligible machine, start at or after release, disjoint half-open processing intervals per machine), nonanticipatory, and has integrable completion times. A non-integrable comparator would have Bochner integral $0$ and would make the bound trivial or false; the integrability requirement rules this out. The greedy algorithm is a predicate on an outcome (assignment and start times): cost-minimal assignment, no start before the modified release date, no unnecessary idleness, and the WSPT priority. Every tie-breaking is covered, and the goal fixes $c=\frac23$. The stochastic policy is the recursion $S_{i,\ell}=\max\{s_{i,\ell},S_{i,\ell-1}+P_{i,\ell-1}\}$ itself. LP feasibility includes summability of every series, and LP optima appear only through "for every feasible point there is a feasible point" statements.

A complete development needs: weak duality for $(\mathrm P_r)$/$(\mathrm D_r)$ with countably many variables; the identity $\mathbb E[C_j]=C^S_j$ for the expected occupation variables of a nonanticipatory policy (reusable for any time-indexed stochastic scheduling relaxation); Lemma 10, a self-contained probability inequality; and the dual fitting. Contributions are welcome on each milestone and on a repaired objective bound for Lemma 7.

Selected references

• V. Gupta, B. Moseley, M. Uetz, Q. Xie, Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling, Mathematics of Operations Research, 2020; arXiv:1703.01634v4. https://arxiv.org/abs/1703.01634, https://doi.org/10.1287/moor.2019.0999
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• N. Megow, M. Uetz, T. Vredeveld, Models and algorithms for stochastic online scheduling, Mathematics of Operations Research 31(3):513–525, 2006. https://doi.org/10.1287/moor.1060.0201
• M. Skutella, M. Sviridenko, M. Uetz, Unrelated machine scheduling with stochastic processing times, Mathematics of Operations Research 41(3):851–864, 2016. https://doi.org/10.1287/moor.2015.0757

Motivation

Online scheduling asks for decisions before the full job set is known. In the online-list model, jobs are revealed one at a time and each must be assigned to a machine before the next job is revealed; the scheduler may choose the processing order after the list is complete. When processing durations are random and machines are unrelated, the same job may have different duration distributions on different machines. An assignment decision therefore affects both its own completion time and the waiting time of other jobs. Gupta, Moseley, Uetz and Xie study a greedy assignment rule for this setting and prove a bound against a scheduler that knows all distributions and all jobs in advance but cannot see future processing-time realizations (arXiv:1703.01634v4, §§2–5). This comparison is relevant to systems that must commit work to heterogeneous servers as requests arrive, while service times remain uncertain.

Setting

Let $M$ be a nonempty finite set of machines and $J=\{0,\ldots,n-1\}$ a finite set of jobs indexed by their presentation order. Job $j$ has a nonnegative weight $w_j$. An eligibility relation $E\subseteq M\times J$ records which machines can process each job; every job has at least one eligible machine. For an eligible pair $(i,j)$, $P_{ij}$ is a nonnegative integer-valued random processing time with mean $\mu_{ij}=\mathbb E[P_{ij}]\ge1$ and a finite second moment. The vector $(P_{ij})_{i\in M}$ for one job may have dependence across machines, but the vectors for different jobs are independent. A parameter $\Delta\ge0$ bounds $\operatorname{Var}(P_{ij})/\mu_{ij}^{2}$ for all eligible pairs. These conventions follow the standing model and coefficient-of-variation bound in the paper (§2, pp. 4–6 and Definition 3, p. 7).

The greedy assignment sends each newly presented job to an eligible machine that minimizes the instantaneous increase in expected total weighted completion time. For a fixed machine, jobs are sequenced by decreasing ratio $w_j/\mu_{ij}$, with job index breaking equal-ratio ties. This is the weighted shortest expected processing time, or WSEPT, order. The algorithm runs each machine continuously from time zero in that order. Its expected objective, $\mathrm{ALG}$, is the expectation of $\sum_j w_j C_j$ for the resulting realized completion times, not a value assigned by a closed formula (§4, pp. 8–9).

A comparator policy can choose machines and start times as earlier jobs finish. It must schedule nonpreemptively, use only information available when a decision is made, and have integrable completion times. It may know the full job set and every processing-time distribution before time zero, but not the future realizations. Write $C_j^\Pi$ for its realized completion time and $\mathrm{OPT}$ for the least expected weighted completion cost among such policies when an optimum exists (§2.1, pp. 5–6).

Formalization targets

The goal is the paper's Theorem 1 (p. 11). It compares every eligible-minimum greedy assignment, including every tie choice, with every admissible nonanticipatory comparator $\Pi$:

$$\mathrm{ALG}\le(4+2\Delta)\,\mathbb E\!\left[\sum_{j\in J}w_j C_j^\Pi\right].$$

This universal comparison expresses $\mathrm{ALG}\le(4+2\Delta)\mathrm{OPT}$ without requiring an optimizer to exist. The milestone list contains the paper's integer tail identities (Lemma 1), the completion-time expression for one job (Lemma 9), the comparison of two time-indexed relaxations and its policy consequence (Lemma 2 and Corollary 1), and the three dual-variable claims used around the greedy algorithm (Lemmas 3–5). Their printed indices and formulas are attached to the proposal in proof order.

Significance

The result supplies a performance guarantee for a combinatorial online algorithm on heterogeneous machines with random durations. The factor varies explicitly with the processing-time variability: for deterministic eligible processing times, $\Delta=0$ and the bound is $4$; greater permitted variability increases it linearly. Forbidden machine-job pairs are included, so the claim applies when some jobs have a restricted set of possible servers. The comparator may postpone machine selection until processing begins and adapt to completed work, so the bound is not limited to fixed-assignment schedules (Theorem 1 and §2.1).

The theorem is proved in the cited paper. In this proposal, the Lean statements and definitions have compiled, while the theorem modules still contain sorry; the remaining formalization work is to supply machine-checked proofs. A completed development would contribute reusable definitions for nonanticipatory unrelated-machine policies, time-indexed stochastic scheduling relaxations, and comparisons with countably many LP variables. Those interfaces can support later scheduling results that use the same information structure.

Difficulty

The most immediate comparison treats the greedy assignment costs as dual variables. For this paper's linear program, the direct halved dual point is feasible, but the resulting dual objective is zero, so feasibility alone gives no useful upper bound on $\mathrm{ALG}$ (Lemmas 3–4 and the beginning of §5). The random processing times also require care when translating occupancy probabilities into completion costs: the time-indexed expression uses both first and second moments, and a policy's start decision must not depend on the job's unobserved duration. The proof must reconcile the greedy order, those probability identities, and a comparison with policies that may change machines and start times adaptively.

Formalization scope

The Lean model uses Fin n in arrival order and permits $n=0$; the empty instance gives a trivial inequality. The machine type is finite and nonempty. Processing times are natural-valued random variables, while policy start times are real. Processing intervals are half-open, so a zero-duration job occupies no machine time. An ineligible pair is represented by the eligibility relation, never by a zero mean. Each eligible processing time has finite second moment and mean at least one; $\Delta$ is any nonnegative upper bound on squared coefficients of variation. The paper leaves $w_j\ge0$ implicit; it is included because negative weights invalidate the comparison. Dependence across machines for the same job is allowed, and the entire time vector is independent across jobs.

Nonanticipation is stated by comparing two realizations that agree on the durations observed by time $t$ and on the fact that running jobs have not yet completed. Admissible comparator policies must work for every realization and have integrable completion times, preventing a default zero value for a nonintegrable integral. The goal quantifies over all such policies, so it cannot be made true by choosing a restricted benchmark. The greedy predicate reads only earlier assignments and admits every eligible minimizing machine; it does not fix a favorable tie choice.

The LP variables $y_{ijs}$ are real and nonnegative, supported on eligible pairs, and their countable sums and time-weighted sums must converge. LP comparisons use feasible witnesses instead of a real infimum, whose value would be misleading for an empty feasible set. A source-level discretization issue is isolated in Lemma 4: $\sum_s\beta_{is}$ counts whole slots up to a nominal completion time, so the printed second equality requires integer means. Its first equality and the goal do not take that condition. A complete proof needs measurable-policy reasoning, tail-sum identities, summability arguments, WSEPT order properties and dual weak duality. Definitions and lemmas that isolate those components are welcome.

Selected references

• V. Gupta, B. Moseley, M. Uetz and Q. Xie, Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling, accepted version of Mathematics of Operations Research, 2020. arXiv:1703.01634v4; DOI:10.1287/moor.2019.0999.

Motivation

A suffix tree of a text $T[1..n]$ answers pattern-matching and string-analysis queries (longest repeats, maximal repeats, matching statistics) in time close to optimal, but it occupies $\Theta(n)$ machine words. For highly repetitive collections, such as many genomes of one species or the versions of a document, this is far more than the information the text contains. A standard measure of that information is $r$, the number of runs (maximal blocks of one repeated symbol) of the Burrows–Wheeler transform of $T$. On repetitive collections $r$ is orders of magnitude smaller than $n$, and indexes using $O(r)$ words are of direct practical interest in bioinformatics and in versioned document stores.

Gagie, Navarro and Prezza (arXiv:1809.02792v2, 2019) build a compressed suffix tree in $O(r\log(n/r))$ words (their Theorem 9, p. 28). A compressed suffix tree in the style of Abeliuk, Cánovas and Navarro (Algorithms 2013) needs the longest common prefix array $LCP$ in compressed form, and stores it differentially, as $DLCP$. The paper's route to compressing $DLCP$ is one exact combinatorial fact: $DLCP$ has a bidirectional macro scheme of size at most $4r+1$ (p. 28). A cited conversion of macro schemes into run-length grammars (Lemma 18, from Gagie, Navarro and Prezza, LATIN 2018) then gives the $O(r\log(n/r))$ grammar. This mission formalizes that combinatorial fact and the lemmas it rests on.

Setting

A text $T[1..n]$, $n\ge 1$, is a string over the alphabet $[1..\sigma]$ whose last symbol T[n]=\=1$is the smallest symbol and occurs nowhere else. The **suffix**$T[i..]$is$T[i]T[i+1]\cdots T[n]$. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$ listing the starting positions of the suffixes in increasing lexicographic order.

The Burrows–Wheeler transform is $BWT[p]=T[SA[p]-1]$ if $SA[p]>1$ and $BWT[p]=T[n]$ if $SA[p]=1$: the symbol preceding the $p$-th smallest suffix, read cyclically. The LF mapping is

$$LF(p)=C[BWT[p]]+\operatorname{rank}[p],$$

where $C[c]$ counts the symbols of $BWT$ smaller than $c$ and $\operatorname{rank}[p]$ counts the occurrences of $BWT[p]$ in $BWT[1..p]$. A position $p$ starts a run if $p=1$ or $BWT[p]\ne BWT[p-1]$; $r$ is the number of run starts, written $p_1<\dots<p_r$.

Let $\operatorname{lcp}(S,S')$ be the length of the longest common prefix of two strings. Then

$$LCP[1]=0,\quad LCP[p]=\operatorname{lcp}(T[SA[p-1]..],T[SA[p]..]),\qquad DLCP[1]=LCP[1],\quad DLCP[i]=LCP[i]-LCP[i-1].$$

The differential suffix array is $DSA[1]=SA[1]$, $DSA[p]=SA[p]-SA[p-1]$.

A bidirectional macro scheme (BMS) of size $b$ on a sequence $S[1..n]$ of any symbol type (Definition 6, p. 28, after Storer and Szymanski) is a partition $S=S_1\cdots S_b$ into consecutive blocks, each either an explicit symbol (a block of length 1) or a pointer to another occurrence $S[j..j']$ of the same content. The source map sends a position at offset $i'$ inside a pointer block to $f(i)=j+i'-1$. The scheme is correct if, from every position $i$, some iterate $f^k(i)$, $k\ge0$, is an explicit symbol.

Formalization targets

Goal: a macro scheme of size at most $4r+1$

$$\exists\ \text{a correct BMS of } DLCP[1..n] \text{ of size } b\le 4r+1.$$

This is the sentence following Lemma 16 on p. 28, proved by Lemma 17. It fixes no constant beyond the paper's own count, and it is the exact input Lemma 18 needs.

Milestones

1. LF is a single cycle (§2.3, p. 8): $LF$ permutes $[1..n]$ and the orbit of position 1 visits every position in fewer than $n$ steps.
2. $LF$ walks the text backwards (§2.4, p. 9): $SA[LF(p)]=SA[p]-1$ whenever $SA[p]>1$.
3. Lemma 12 (p. 20): if $BWT[p-1]=BWT[p]$ then $LF(p-1)=LF(p)-1$ and $DSA[LF(p)]=DSA[p]$.
4. Lemma 16 (p. 28): if $BWT[p-2]=BWT[p-1]=BWT[p]$ then $LF(p-1)=LF(p)-1$ and $DLCP[LF(p)]=DLCP[p]$.
5. Lemma 17 (p. 28): the partition of $DLCP$ into the explicit symbols $DLCP[p_i+k]$, $k\in\{0,1,2\}$, and the regions $DLCP[p_i+3..p_{i+1}-1]$ pointing to $DLCP[LF(p_i+3)..LF(p_{i+1}-1)]$, is a BMS.

Significance

The result. The bound $4r+1$ ties the compressibility of the $LCP$ array, a structure of size $n$ that does not obviously inherit the repetitiveness of the BWT, to the number of BWT runs. Through Lemma 18 it yields a run-length grammar of size $O(r\log(n/r))$ for $DLCP$ (Lemma 19, p. 29), and the paper's compressed suffix tree supports its navigation primitives on that grammar. The same pattern, runs of the BWT inducing copies in a differential array, drives the paper's $O(r\log(n/r))$-word access to $SA$ and $ISA$ (§5), of which Lemma 12 is the first step.

Formalizing it. The result is proved in the paper; to our knowledge none of it, nor the basic theory of suffix arrays and the Burrows–Wheeler transform, has a machine-checked proof on this platform. The mission produces a self-contained Lean development of the BWT and LF mapping from their counting definitions, of the $LCP$ and $DLCP$ arrays, and of macro schemes with their correctness condition. The single-cycle property of $LF$ and the identity $SA[LF(p)]=SA[p]-1$ are folklore results that underlie every FM-index; they are formalized here from the counting formula, not assumed.

Difficulty

The obvious proof of the goal counts blocks: at most $3r$ explicit symbols and at most $r+1$ regions. The counting is easy; the content lies in the two properties the count presupposes. First, the copies must be correct: a whole region $DLCP[p_i+3..p_{i+1}-1]$ must coincide with the stretch starting at $LF(p_i+3)$, which needs $LF$ to map a run onto consecutive positions and $LCP$ differences to be preserved, and it needs three consecutive equal BWT symbols, not two, because $DLCP[p]$ involves the suffixes in cells $p-2$, $p-1$ and $p$. Second, the scheme must be correct as a whole: following pointers must never cycle. A scheme in which two regions point at each other satisfies every local condition and still fails. Ruling this out requires the global fact that $LF$ is one cycle through all of $[1..n]$, which in turn rests on the lexicographic order of suffixes and the uniqueness of the terminator \$$. Connecting the counting definition of LF$to the backward step$SA[LF(p)]=SA[p]-1$ is itself a nontrivial argument about ranks of symbols among sorted suffixes.

Formalization scope

Positions are 1-based natural numbers, as in the paper. The text and the suffix array are functions $\mathbb N\to\mathbb N$ read only on $[1..n]$, symbols are natural numbers, and \=1$. The suffix array is a hypothesis (`IsSuffixArray`: a permutation of$[1..n]$sorting the suffixes strictly), never a construction;$BWT$and$LF$are the counting formulas of p. 8, with$T[0]$read as$T[n]$.$LCP$is computed from a recursive$\operatorname{lcp}$on suffix lists;$DLCP$and$DSA$are integer-valued. A macro scheme is defined for any symbol type as a list of blocks laid out consecutively from position 1, each with a length and an optional source start; its size is the list length. Explicit blocks have length 1; a pointer block starting at$i$has a source$j\ne i$inside$[1..n]$, possibly overlapping the block. The value of$f$on explicit symbols, arbitrary on the page, is the identity. The explicit cells$p_i+k$of Lemma 17 are taken only where they exist ($\le n$), and coinciding cells of short runs are counted once; the convention$p_0=-2$only empties the region before$p_1=1$. Lemma 17 is stated as a characterisation of the scheme: explicit blocks exactly at explicit cells, pointer blocks exactly the maximal stretches of the remaining cells, each pointing to$LF$of its first cell with$LF$mapping every cell in the block to the corresponding source cell. The identity$SA[LF(p)]=SA[p]-1$carries the guard$SA[p]>1$, since for$SA[p]=1$ it holds only cyclically.

The paper's $O(\cdot)$ space and time claims (Theorem 9, Lemma 19) and the cited grammar conversion (Lemma 18) are out of scope; the goal is their explicit combinatorial content.

Every sequence has a macro scheme of size $n$ (all symbols explicit), and a set of pointers that only point at each other satisfies every local condition, so a formalization that bounds the size of an arbitrary partition, or that drops the condition that every chain of copies reaches an explicit symbol, would be empty or false; both are excluded by the definition used. $SA$, $BWT$ and $LF$ are not defined through the properties the milestones assert.

Contributions welcome: proofs of the milestones, and reusable lemmas about the LF mapping and lexicographic order of suffixes, which the paper's other missions (locating with sampled phrases, counting distinct substrings) also use.

Selected references

• T. Gagie, G. Navarro, N. Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv preprint, 2019 (v2). https://arxiv.org/abs/1809.02792
• J. A. Storer, T. G. Szymanski, Data compression via textual substitution, Journal of the ACM 29(4):928–951, 1982. https://doi.org/10.1145/322344.322346
• A. Abeliuk, R. Cánovas, G. Navarro, Practical compressed suffix trees, Algorithms 6(2):319–351, 2013. https://doi.org/10.3390/a6020319
• T. Gagie, G. Navarro, N. Prezza, On the approximation ratio of Lempel-Ziv parsing, Proc. LATIN 2018, LNCS 10807, pp. 490–503.
• M. Burrows, D. Wheeler, A block sorting lossless data compression algorithm, Technical Report 124, Digital Equipment Corporation, 1994.
• V. Mäkinen, G. Navarro, Succinct suffix arrays based on run-length encoding, Nordic Journal of Computing 12(1):40–66, 2005.

Motivation

Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length $n$, not with the amount of distinct content. The number $r$ of runs in the Burrows–Wheeler transform (BWT) of the text is a standard measure of repetitiveness, and the run-length FM-index of Mäkinen and Navarro counts the occurrences of a pattern in $O(r)$ words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to $n/s$ for a sampling step $s$, which defeats the purpose on repetitive data.

Timeline.

• 1994: Burrows and Wheeler introduce the transform (DEC SRC Research Report 124).
• 2000–2005: Ferragina and Manzini build the FM-index, with backward search and the LF mapping (J. ACM 52(4), 2005).
• 2005: Mäkinen and Navarro give the run-length FM-index, which counts occurrences in $O(r)$ words (Nordic J. Computing 12(1), 2005).
• 2016–2018: Prezza (PhD thesis, Udine, 2016) and Policriti and Prezza (Algorithmica 80(7), 2018) keep one known suffix-array cell, a "toehold", during backward search.
• 2017–2020: Gagie, Navarro and Prezza show that $O(r)$ words suffice to locate every occurrence (arXiv:1705.10382; arXiv:1809.02792; J. ACM 67(1), 2020). This mission formalizes the combinatorial core of that result.

Setting

A text $T[1..n]$ is a sequence over the alphabet $[1..\sigma]$ whose last symbol T[n]=\=1$is the smallest symbol and occurs nowhere else. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$that lists the suffixes$T[SA[p]..n]$in strictly increasing lexicographic order, and the **inverse suffix array** satisfies$SA[ISA[i]]=i. The BWT records the character preceding each sorted suffix, $$BWT[p]=T[SA[p]-1]\ (SA[p]>1),\qquad BWT[p]=T[n]=\\ (SA[p]=1),$$ so that $T[0]$ is read as $T[n]$. The LF mapping is the counting formula $LF(p)=C[BWT[p]]+\operatorname{rank}[p]$, where $C[c]$ counts BWT symbols smaller than $c$ and $\operatorname{rank}[p]$ counts copies of $BWT[p]$ in $BWT[1..p]$.

A run is a maximal block of equal consecutive BWT symbols, and $r$ is their number. A text position is sampled when its character is the first or last BWT character in its run (Definition 1); at most $2r$ positions are sampled. Definition 3 cuts $T$ into phrases that begin exactly at the sampled positions. For a text position $k$, the phrase head $i$ of $T[k]$ is the greatest sampled position $\le k$. The permutation $\phi(i)=SA[ISA[i]-1]$ (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are $DSA[p]=SA[p]-SA[p-1]$ and $DISA[i]=ISA[i]-ISA[i-1]$. A text position starts a phrase of $ISA$ when $ISA[i]$ is the first position of a run.

Formalization targets

Goal: the identity in the proof of Lemma 3

Let $SA[p]=k+1$, let $i$ be the phrase head of $T[k]$, let $q=ISA[i+1]$, and let $N[i]=\langle x,y\rangle=\langle SA[q-1],SA[q+1]\rangle$ be the sample stored at $i$. Then

$$SA[p-1]=x+k-i\quad(p\ge 2),\qquad SA[p+1]=y+k-i\quad(p<n),$$

and $q\ge 2$, $q<n$ respectively, so that $N[i]$ is defined.

Milestones

1. §2.4, p. 9. $SA[LF(p)]=SA[p]-1$ for $SA[p]>1$, with $LF(p)\in[1..n]$.
2. Lemma 12, p. 20. If $BWT[p-1]=BWT[p]$, then $LF(p-1)=LF(p)-1$ and $DSA[LF(p)]=DSA[p]$.
3. Run-free claim, proof of Lemma 3, pp. 12–13. For $0\le t<k-i$, the cells $LF^t(p-1),LF^t(p),LF^t(p+1)$ are contiguous and lie in one BWT run.
4. Lemma 14, p. 23. If $i$ does not start a phrase of $ISA$, then $\phi(i-1)=\phi(i)-1$ and $DISA[i]=DISA[\phi(i)]$.

A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both $c$ and a non-$c$ symbol contains an occurrence of $c$ at the first or last position of a run.

Significance

The goal says that the $O(r)$ numbers $N[i]$, one pair per sampled position, determine the neighbours of every suffix-array cell, after one predecessor search over the sampled positions. Combined with the toehold of Lemma 2, which provides one known cell inside the interval $SA[sp..ep]$ of a pattern, it lets an index list all occurrences in $O(r)$ space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to $s$ neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for $SA$ and $ISA$ in §5.

The results are proved in the paper; none of them has a machine-checked proof. The mission contributes a formal model of suffix arrays, BWT, LF and runs that is independent of any data-structure encoding, a checked proof of the LF identity from the counting formula, and the exact correctness statement behind the $r$-index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.

Difficulty

The obvious argument follows the three cells $p-1,p,p+1$ backwards under LF for $k-i$ steps. It rests on two facts that are easy to state and not routine to prove. First, $SA[LF(p)]=SA[p]-1$ must be derived from the counting formula $C[c]+\operatorname{rank}[p]$: this is a stable-sorting argument about suffixes that begin with the same symbol, and it uses the uniqueness of \$$. Second, LF must map adjacent cells of a run to adjacent cells, and one must check that the neighbouring cells never leave the run while the middle cell walks from T[k]$back to$T[i+1]$. This is where the choice of$i$as the *greatest* sampled position$\le k$matters, and also where the case of no sampled position in$[1..k]$needs care. Finally, one more LF step from$T[i+1]$to$T[i]$produces the cell$q$, and the shift by$k-i$ must be tracked through natural-number arithmetic.

Formalization scope

Positions are 1-based natural numbers, as in the paper. $T$ and $SA$ are functions $\mathbb N\to\mathbb N$ read only on $[1..n]$. $SA$ is a hypothesis, IsSuffixArray: it maps $[1..n]$ injectively into $[1..n]$ and sorts the suffixes strictly in Lean's lexicographic order on lists. Since \=1$is unique and smallest, this order agrees with the paper's. BWT and LF are defined by the formulas of p. 8, never by the properties the milestones assert.$ISA[i]$is$0$if no cell holds$i$. Sampled positions follow the first sentence of Definition 1 (first or last in its run); the paper's "That is" clause omits the last character of the final run.$DSA$and$DISA$ are integer-valued.

Pins and guards:

• Wrap-around phrase. If no sampled position lies in $[1..k]$, the phrase containing $T[k]$ began at T[n]=\$$, which is always sampled. Its head is encoded as 0$($T[0]\equiv T[n]$), so that$q=ISA[1]$is the cell holding$$$. The goal covers this case; it does not assume a sampled position$\le k$.
• Neighbours. Each half of the goal and of the run-free claim is guarded by the existence of the neighbour ($p\ge 2$, $p<n$).
• SA[LF(p)]. The identity is stated for $SA[p]>1$; for $SA[p]=1$ it holds only cyclically.
• Lemma 14. "$[i-1..i]$ within a phrase of $ISA$" means that $i$ does not start a phrase of $ISA$, which begin only at run-first cells. Definition 3's phrases begin at run-first and run-last cells; the two parses are kept apart.

The space and time claims of Lemmas 2–3 and Theorem 1 ($O(r)$ words, $O(\log\log_w(n/r))$ time on a word RAM) are out of scope; the goal is their explicit combinatorial content. Two trivializing formalizations are ruled out: defining LF as "the cell holding $SA[p]-1$", which would make milestone 1 a tautology; and defining the phrase head by iterating LF, which would build the proof into the definition. The phrase head is the maximum of the sampled positions $\le k$.

A full development needs elementary facts about lexicographic order on lists, counting over finite intervals, and iterates of LF. The suffix-array and BWT layer is reusable beyond this mission; two parallel missions on the same paper share the same core definitions. Proofs of the milestones in any order are welcome, as are alternative routes, e.g. through Lemma 14 and $\phi$ for the left half of the goal.

Selected references

• T. Gagie, G. Navarro, N. Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv:1809.02792v2, 2019. https://arxiv.org/abs/1809.02792
• T. Gagie, G. Navarro, N. Prezza, Fully Functional Suffix Trees and Optimal Text Searching in BWT-Runs Bounded Space, J. ACM 67(1), 2020. https://doi.org/10.1145/3375890
• T. Gagie, G. Navarro, N. Prezza, Optimal-Time Text Indexing in BWT-runs Bounded Space, arXiv:1705.10382, 2017 (SODA 2018). https://arxiv.org/abs/1705.10382
• P. Ferragina, G. Manzini, Indexing Compressed Text, J. ACM 52(4):552–581, 2005. https://doi.org/10.1145/1082036.1082039
• A. Policriti, N. Prezza, LZ77 Computation Based on the Run-Length Encoded BWT, Algorithmica 80(7):1986–2011, 2018. https://doi.org/10.1007/s00453-017-0327-z
• V. Mäkinen, G. Navarro, Succinct Suffix Arrays Based on Run-Length Encoding, Nordic Journal of Computing 12(1):40–66, 2005 (no DOI).
• M. Burrows, D. J. Wheeler, A Block Sorting Lossless Data Compression Algorithm, Technical Report 124, Digital Equipment Corporation, 1994 (no DOI).