List ranking by pointer jumping

DefinitionIterated successor#✓fully proved

For a successor map \(\mathrm{succ}\) on the nodes \(0, \dots, n-1\), where \(\mathrm{succ}(v)\) is either a node or undefined, the \(k\)-step jump from \(v\) is the node reached by applying \(\mathrm{succ}\) \(k\) times starting at \(v\), and is undefined if some step is undefined: the \(0\)-step jump from \(v\) is \(v\), and the \((k+1)\)-step jump is \(\mathrm{succ}\) of the \(k\)-step jump.

def jump (succ : Fin n → Option (Fin n)) : ℕ → Fin n → Option (Fin n)
  | 0, v => some v
  | k + 1, v => (jump succ k v).bind succ

Used by 13

Used byThe characteristic property of the rank · Rank of a node in a linked list · Rank decreases along jumps · Pointer-jumping sums are the suffix sums once \(n \le 2^t\) · After enough rounds, the distances are the ranks · The invariant of pointer jumping for suffix sums · The invariant of pointer jumping for list ranking · Segment sums add up · Segment sums of unit values count nodes · The value \(k\) steps ahead · The characteristic property of suffix sums · List ranking is the special case of unit values · Terminating successor functions

DefinitionTerminating successor functions#✓fully proved

A successor function \(\mathrm{succ}\) on the nodes \(0, \dots, n - 1\), mapping each node to its successor or to nothing, terminates when from every node \(v\) the walk of \(n\) steps along \(\mathrm{succ}\) runs off the end, that is, there is no node \(n\) steps down the list from \(v\).

def Terminates (succ : Fin n → Option (Fin n)) : Prop := ∀ v, jump succ n v = none

Uses 1 · Used by 11

Statement usesIterated successor

Used byThe characteristic property of the rank · Pointer jumping ranks every list in ⌈log₂ n⌉ rounds · Pointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds · Rank of a node in a linked list · Rank decreases along jumps · Pointer-jumping sums are the suffix sums once \(n \le 2^t\) · After enough rounds, the distances are the ranks · The invariant of pointer jumping for list ranking · Segment sums of unit values count nodes · The characteristic property of suffix sums · List ranking is the special case of unit values

DefinitionRank of a node in a linked list#✓fully proved

Let \(\mathrm{succ}\) be a successor map on the nodes \(0, \dots, n-1\) whose lists terminate. The rank of a node \(v\) is the least \(k\) such that following \(\mathrm{succ}\) for \(k + 1\) steps from \(v\) runs off the end of the list, that is, the number of nodes after \(v\) in its list.

noncomputable def rank (hs : Terminates succ) (v : Fin n) : ℕ :=
  Nat.find (p := fun k => jump succ (k + 1) v = none) ⟨n - 1, by
    rcases Nat.eq_zero_or_pos n with rfl | hn
    · exact v.elim0
    · rw [Nat.sub_add_cancel hn]; exact hs v⟩

Uses 2 · Used by 8

Statement usesTerminating successor functions · Iterated successor

Used byThe characteristic property of the rank · Pointer jumping ranks every list in ⌈log₂ n⌉ rounds · Rank decreases along jumps · After enough rounds, the distances are the ranks · The invariant of pointer jumping for list ranking · Segment sums of unit values count nodes · The characteristic property of suffix sums · List ranking is the special case of unit values

TheoremThe characteristic property of the rank#✓fully proved

Let \(\mathrm{succ}\) be a successor map on the nodes \(0, \dots, n-1\) whose lists terminate. For every node \(v\) and every \(k \in \mathbb{N}\), following \(\mathrm{succ}\) for \(k\) steps from \(v\) runs off the end of the list if and only if \(k > \operatorname{rank}(v)\).

theorem jump_eq_none_iff (hs : Terminates succ) (v : Fin n) (k : ℕ) :
    jump succ k v = none ↔ rank hs v < k

Uses 3 · Used by 6

Statement usesTerminating successor functions · Iterated successor · Rank of a node in a linked list

Used byRank decreases along jumps · After enough rounds, the distances are the ranks · The invariant of pointer jumping for list ranking · Segment sums of unit values count nodes · The characteristic property of suffix sums · List ranking is the special case of unit values

TheoremRank decreases along jumps#✓fully proved

Let \(\mathrm{succ}\) be a successor map on the nodes \(0, \dots, n-1\) whose lists terminate. If following \(\mathrm{succ}\) for \(a\) steps from a node \(v\) reaches the node \(u\), then \(a \le \operatorname{rank}(v)\) and \(\operatorname{rank}(u) = \operatorname{rank}(v) - a\).

theorem rank_of_jump (hs : Terminates succ) {a : ℕ} {v u : Fin n} (h : jump succ a v = some u) :
    a ≤ rank hs v ∧ rank hs u = rank hs v - a

Uses 4 · Used by 2

Statement usesTerminating successor functions · Iterated successor · Rank of a node in a linked list

Proof usesThe characteristic property of the rank

Used byThe invariant of pointer jumping for list ranking · The characteristic property of suffix sums

StructurePointer-jumping state for list ranking#✓fully proved

A pointer-jumping state on the nodes \(0, \dots, n - 1\) assigns to each node a pointer, which is either a node or empty (once it points past the end of the list), and a distance in \(\mathbb{N}\), the distance covered by the pointer.

structure State (n : ℕ) where
  /-- The node's pointer (`none` once it points past the end). -/
  ptr : Fin n → Option (Fin n)
  /-- The distance covered by the pointer. -/
  dist : Fin n → ℕ

Used by 7

Used byInitial state of pointer jumping · Pointer jumping ranks every list in ⌈log₂ n⌉ rounds · One round of pointer jumping · The list-ranking state after \(t\) rounds · After enough rounds, the distances are the ranks · The invariant of pointer jumping for list ranking · Tabulating a list-ranking state

DefinitionInitial state of pointer jumping#✓fully proved

For a successor map \(\mathrm{succ}\) on the nodes \(0, \dots, n-1\), where \(\mathrm{succ}(v)\) is either a node or undefined (at the end of a list), the initial pointer-jumping state gives each node \(v\) the pointer \(\mathrm{succ}(v)\) and the distance \(0\) if \(\mathrm{succ}(v)\) is undefined and \(1\) otherwise.

def init (succ : Fin n → Option (Fin n)) : State n :=
  ⟨succ, fun v => if succ v = none then 0 else 1⟩

Uses 1 · Used by 2

Statement usesPointer-jumping state for list ranking

Used byThe list-ranking state after \(t\) rounds · List-ranking rounds on arrays

DefinitionOne round of pointer jumping#✓fully proved

In one parallel round, every node \(v\) whose pointer is a node \(u\) adds the distance of \(u\) to its own distance and moves its pointer to the pointer of \(u\) (undefined if that of \(u\) is); a node whose pointer is undefined keeps its distance and its undefined pointer.

def round (s : State n) : State n :=
  ⟨fun v => (s.ptr v).bind s.ptr, fun v =>
    match s.ptr v with
    | none => s.dist v
    | some u => s.dist v + s.dist u⟩

Uses 1 · Used by 2

Statement usesPointer-jumping state for list ranking

Used byPointer jumping ranks every list in ⌈log₂ n⌉ rounds · The list-ranking state after \(t\) rounds

DefinitionThe list-ranking state after \(t\) rounds#✓fully proved

For a successor function \(\mathrm{succ}\) on the nodes \(0, \dots, n - 1\), the pointer-jumping state after \(t\) rounds is defined by recursion on \(t\): after \(0\) rounds it is the initial state of \(\mathrm{succ}\), and after \(t + 1\) rounds it is one round of pointer jumping applied to the state after \(t\) rounds.

def rounds (succ : Fin n → Option (Fin n)) : ℕ → State n
  | 0 => init succ
  | t + 1 => round (rounds succ t)

Uses 3 · Used by 3

Statement usesPointer-jumping state for list ranking · Initial state of pointer jumping · One round of pointer jumping

Used byPointer jumping ranks every list in ⌈log₂ n⌉ rounds · After enough rounds, the distances are the ranks · The invariant of pointer jumping for list ranking

TheoremThe invariant of pointer jumping for list ranking#✓fully proved

Let \(\mathrm{succ}\) map each of the nodes \(0, \dots, n - 1\) to its successor or to nothing, and suppose the lists terminate: from every node, \(n\) steps run off the end. Write \(\mathrm{rank}(v)\) for the number of nodes after \(v\). Then for every \(t \ge 0\) and every node \(v\), after \(t\) rounds of pointer jumping, the pointer of \(v\) is the node \(2^t\) steps down the list from \(v\) (no node if the list ends before that), and the distance of \(v\) is \(\min(2^t, \mathrm{rank}(v))\).

theorem rounds_spec (hs : Terminates succ) : ∀ t v,
    (rounds succ t).ptr v = jump succ (2 ^ t) v ∧
      (rounds succ t).dist v = min (2 ^ t) (rank hs v)

Uses 7 · Used by 1

Statement usesPointer-jumping state for list ranking · Terminating successor functions · Iterated successor · Rank of a node in a linked list · The list-ranking state after \(t\) rounds

Proof usesThe characteristic property of the rank · Rank decreases along jumps

Used byAfter enough rounds, the distances are the ranks

TheoremAfter enough rounds, the distances are the ranks#✓fully proved

Let \(\mathrm{succ}\) be a successor map on the nodes \(0, \dots, n-1\) whose lists terminate, and let \(t\) be a natural number with \(n \le 2^t\). Then after \(t\) rounds of pointer jumping from the initial state, the distance of every node \(v\) is the rank of \(v\).

theorem rounds_dist (hs : Terminates succ) {t : ℕ} (ht : n ≤ 2 ^ t) (v : Fin n) :
    (rounds succ t).dist v = rank hs v

Uses 7 · Used by 1

Statement usesPointer-jumping state for list ranking · Terminating successor functions · Rank of a node in a linked list · The list-ranking state after \(t\) rounds

Proof usesIterated successor · The characteristic property of the rank · The invariant of pointer jumping for list ranking

Used byPointer jumping ranks every list in ⌈log₂ n⌉ rounds

DefinitionTabulating a list-ranking state#✓fully proved

The tabulation of a pointer-jumping state \(s\) on the nodes \(0, \dots, n - 1\) is the pair of arrays of length \(n\) whose entries at \(v\) are the pointer and the distance of \(v\) in \(s\).

Evaluating the state after \(t\) rounds directly re-reads earlier rounds' pointers at every query, a cost growing exponentially with the number of rounds; the tabulated rounds cost \(O(n)\) array operations each.

def tabulate (s : State n) : Array (Option (Fin n)) × Array ℕ :=
  (Array.ofFn s.ptr, Array.ofFn s.dist)

Uses 1 · Used by 2

Statement usesPointer-jumping state for list ranking

Used byPointer jumping ranks every list in ⌈log₂ n⌉ rounds · List-ranking rounds on arrays

DefinitionOne pointer-jumping round on arrays#✓fully proved

Given an array \(P\) of pointers (each a node among \(0, \dots, n-1\) or undefined) and an array \(D\) of natural-number distances, one round returns arrays \(P'\) and \(D'\) of length \(n\) where, for each node \(v\), \(P'[v]\) is \(P[u]\) if \(P[v] = u\) and is undefined if \(P[v]\) is undefined, and \(D'[v] = D[v] + D[u]\) if \(P[v] = u\) and \(D'[v] = D[v]\) if \(P[v]\) is undefined. Entries missing from the input arrays are read as undefined pointers and distance \(0\).

def roundTab (s : Array (Option (Fin n)) × Array ℕ) : Array (Option (Fin n)) × Array ℕ :=
  (Array.ofFn fun v : Fin n => (s.1.getD v none).bind fun u => s.1.getD u none,
    Array.ofFn fun v : Fin n =>
      match s.1.getD v none with
      | none => s.2.getD v 0
      | some u => s.2.getD v 0 + s.2.getD u 0)

Used by 2

Used byPointer jumping ranks every list in ⌈log₂ n⌉ rounds · List-ranking rounds on arrays

DefinitionList-ranking rounds on arrays#✓fully proved

For a successor function \(\mathrm{succ}\) on the nodes \(0, \dots, n - 1\) and \(t \ge 0\), the arrays after \(t\) rounds are a pair of arrays (pointers and distances) defined by recursion on \(t\): after \(0\) rounds they are the tabulation of the initial state of \(\mathrm{succ}\), and after \(t + 1\) rounds they are one round on arrays applied to the arrays after \(t\) rounds.

def roundsTab (succ : Fin n → Option (Fin n)) : ℕ → Array (Option (Fin n)) × Array ℕ
  | 0 => tabulate (init succ)
  | t + 1 => roundTab (roundsTab succ t)

Uses 3 · Used by 2

Statement usesInitial state of pointer jumping · One pointer-jumping round on arrays · Tabulating a list-ranking state

Used byList ranking by pointer jumping · Pointer jumping ranks every list in ⌈log₂ n⌉ rounds

DefinitionList ranking by pointer jumping#✓fully proved

For a successor map \(\mathrm{succ}\) on the nodes \(0, \dots, n-1\), list ranking by pointer jumping runs \(\lceil \log_2 n \rceil\) rounds of pointer jumping on arrays, starting from the initial state, and returns the resulting array of distances, whose entry \(v\) is the distance of node \(v\).

When the lists terminate, entry \(v\) is the rank of node \(v\).

def listRanks (succ : Fin n → Option (Fin n)) : Array ℕ := (roundsTab succ (Nat.clog 2 n)).2

Uses 1 · Used by 1

Statement usesList-ranking rounds on arrays

Used byPointer jumping ranks every list in ⌈log₂ n⌉ rounds

TheoremPointer jumping ranks every list in ⌈log₂ n⌉ rounds#✓fully proved

Let \(\mathrm{succ}\) be a successor map on the nodes \(0, \dots, n-1\) whose lists terminate. Then for every node \(v\), entry \(v\) of the table returned by list ranking by pointer jumping, which runs \(\lceil \log_2 n \rceil\) rounds, is the rank of \(v\).

theorem listRanks_getD (hs : Terminates succ) (v : Fin n) :
    (listRanks succ).getD v 0 = rank hs v

Uses 10

Statement usesTerminating successor functions · List ranking by pointer jumping · Rank of a node in a linked list

Proof usesPointer-jumping state for list ranking · One round of pointer jumping · One pointer-jumping round on arrays · The list-ranking state after \(t\) rounds · List-ranking rounds on arrays · After enough rounds, the distances are the ranks · Tabulating a list-ranking state

DefinitionThe value \(k\) steps ahead#✓fully proved

Let \(n\) nodes be linked into lists by a partial successor function, each node \(u\) carrying a value \(x_u\) in an additive monoid \(M\). For \(k \in \mathbb{N}\) and a node \(v\), this is \(x_u\) where \(u\) is the node \(k\) steps after \(v\) along its list, and \(0\) if the list ends before \(k\) steps.

def stepVal (succ : Fin n → Option (Fin n)) (x : Fin n → M) (k : ℕ) (v : Fin n) : M :=
  match jump succ k v with
  | some u => x u
  | none => 0

Uses 1 · Used by 4

Statement usesIterated successor

Used bySegment sums · Segment sums add up · Segment sums of unit values count nodes · The characteristic property of suffix sums

DefinitionSegment sums#✓fully proved

Let \(n\) nodes be linked into lists by a partial successor function, and let each node \(v\) carry a value \(x_v\) in an additive monoid \(M\) (not necessarily commutative). For \(k \in \mathbb{N}\) and a node \(v\), the segment sum of length \(k\) from \(v\) is the sum, in list order, of the values of the first \(k\) nodes of the list starting at \(v\) (fewer if the list ends sooner); for \(k = 0\) it is \(0\).

def segSum (succ : Fin n → Option (Fin n)) (x : Fin n → M) : ℕ → Fin n → M
  | 0, _ => 0
  | k + 1, v => segSum succ x k v + stepVal succ x k v

Uses 1 · Used by 7

Statement usesThe value \(k\) steps ahead

Used byPointer-jumping sums are the suffix sums once \(n \le 2^t\) · The invariant of pointer jumping for suffix sums · Segment sums add up · Segment sums of unit values count nodes · Suffix sums · The characteristic property of suffix sums · List ranking is the special case of unit values

TheoremSegment sums add up#✓fully proved

Let \(\mathrm{succ}\) be a partial successor function on nodes \(0, \dots, n-1\) and \(x_v\) values in an additive monoid \(M\). For \(k \in \mathbb{N}\) write \(S_k(v)\) for the sum, in list order, of the values of the nodes reached from \(v\) in \(0, 1, \dots, k - 1\) steps along \(\mathrm{succ}\) (a missing node contributes \(0\)). Then for all \(a, b \in \mathbb{N}\) and every node \(v\), \(S_{a+b}(v) = S_a(v) + S_b(u)\) if the node \(u\) reached from \(v\) in \(a\) steps exists, and \(S_{a+b}(v) = S_a(v)\) otherwise.

theorem segSum_add (a b : ℕ) (v : Fin n) : segSum succ x (a + b) v =
    segSum succ x a v + match jump succ a v with

Uses 3 · Used by 3

Statement usesSegment sums · Iterated successor

Proof usesThe value \(k\) steps ahead

Used byPointer-jumping sums are the suffix sums once \(n \le 2^t\) · The invariant of pointer jumping for suffix sums · The characteristic property of suffix sums

DefinitionSuffix sums#✓fully proved

Let \(n\) nodes be linked into lists by a partial successor function, each node \(v\) carrying a value \(x_v\) in an additive monoid \(M\). The suffix sum of a node \(v\) is the segment sum of length \(n\) from \(v\): the sum, in list order, of the values of the first \(n\) nodes of the list starting at \(v\) (fewer if it ends sooner).

When the list from \(v\) ends, it has at most \(n\) nodes, so this is the sum of the values from \(v\) to the end of its list.

def suffixSum (succ : Fin n → Option (Fin n)) (x : Fin n → M) (v : Fin n) : M := segSum succ x n v

Uses 1 · Used by 4

Statement usesSegment sums

Used byPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds · Pointer-jumping sums are the suffix sums once \(n \le 2^t\) · The characteristic property of suffix sums · List ranking is the special case of unit values

TheoremThe characteristic property of suffix sums#✓fully proved

Let \(n\) nodes be linked into lists by a partial successor function such that, starting from any node, \(n\) steps run off the end of its list, and let each node \(v\) carry a value \(x_v\) in an additive monoid \(M\). Then for every node \(v\), the suffix sum of \(v\) is \(x_v\) plus the suffix sum of the successor of \(v\), or just \(x_v\) if \(v\) has no successor.

theorem suffixSum_eq (hs : Terminates succ) (v : Fin n) :
    suffixSum succ x v = x v + match succ v with

Uses 9

Statement usesSuffix sums · Terminating successor functions

Proof usesSegment sums · Segment sums add up · The value \(k\) steps ahead · Iterated successor · The characteristic property of the rank · Rank of a node in a linked list · Rank decreases along jumps

TheoremSegment sums of unit values count nodes#✓fully proved

Let \(n\) nodes be linked into lists by a partial successor function such that, starting from any node, \(n\) steps run off the end of its list, and give every node the value \(1 \in \mathbb{N}\). Then for every \(k \in \mathbb{N}\) and every node \(v\), the segment sum of length \(k\) from \(v\) (the sum of the values of the first \(k\) nodes from \(v\), fewer at the end of the list) is \(\min(k, \operatorname{rank}(v) + 1)\), where \(\operatorname{rank}(v)\) is the number of nodes after \(v\) in its list.

theorem segSum_one (hs : Terminates succ) (k : ℕ) (v : Fin n) :
    segSum succ (fun _ => (1 : ℕ)) k v = min k (rank hs v + 1)

Uses 6 · Used by 1

Statement usesSegment sums · Terminating successor functions · Rank of a node in a linked list

Proof usesThe value \(k\) steps ahead · Iterated successor · The characteristic property of the rank

Used byList ranking is the special case of unit values

TheoremList ranking is the special case of unit values#✓fully proved

Let \(n\) nodes be linked into lists by a partial successor function such that, starting from any node, \(n\) steps run off the end of its list. If every node has value \(1 \in \mathbb{N}\), then the suffix sum of every node \(v\) is \(\operatorname{rank}(v) + 1\), where \(\operatorname{rank}(v)\) is the number of nodes after \(v\) in its list.

theorem suffixSum_one (hs : Terminates succ) (v : Fin n) :
    suffixSum succ (fun _ => (1 : ℕ)) v = rank hs v + 1

Uses 7

Statement usesSuffix sums · Terminating successor functions · Rank of a node in a linked list

Proof usesSegment sums · Segment sums of unit values count nodes · Iterated successor · The characteristic property of the rank

StructureState of pointer jumping for suffix sums#✓fully proved

For \(n\) nodes and a type \(M\), a state assigns to each node \(v\) a pointer, which is either a node or none (past the end of the list), and an accumulated value in \(M\). The accumulated value is meant to be the sum of the node values from \(v\) up to, but not including, the pointer's target.

structure State (n : ℕ) (M : Type*) where
  /-- The node's pointer (`none` once it points past the end). -/
  ptr : Fin n → Option (Fin n)
  /-- The sum of the values from the node up to, not including, the pointer's target. -/
  acc : Fin n → M

Used by 7

Used byInitial state of pointer jumping for suffix sums · Pointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds · One round of pointer jumping for suffix sums · State after \(t\) rounds of pointer jumping for suffix sums · Pointer-jumping sums are the suffix sums once \(n \le 2^t\) · The invariant of pointer jumping for suffix sums · Pointer-jumping state as arrays

DefinitionInitial state of pointer jumping for suffix sums#✓fully proved

Given nodes \(0, \dots, n-1\) with a partial successor function \(\mathrm{succ}\) and values \(x_v\) in an additive monoid \(M\), the initial state gives each node \(v\) the pointer \(\mathrm{succ}(v)\) (undefined at the end of a list) and the sum \(x_v\).

def init (succ : Fin n → Option (Fin n)) (x : Fin n → M) : State n M := ⟨succ, x⟩

Uses 1 · Used by 2

Statement usesState of pointer jumping for suffix sums

Used byState after \(t\) rounds of pointer jumping for suffix sums · Arrays after \(t\) rounds of pointer jumping for suffix sums

DefinitionOne round of pointer jumping for suffix sums#✓fully proved

Given a state in which each node \(v\) has a pointer \(p(v)\), either a node or undefined, and a sum \(s(v)\) in an additive monoid \(M\), one round produces a new state as follows. If \(p(v)\) is undefined, the pointer of \(v\) stays undefined and its sum stays \(s(v)\). If \(p(v) = u\), the new pointer of \(v\) is \(p(u)\) and its new sum is \(s(v) + s(u)\), with \(s(u)\) added on the right so that list order is kept.

def round (s : State n M) : State n M :=
  ⟨fun v => (s.ptr v).bind s.ptr, fun v =>
    match s.ptr v with
    | none => s.acc v
    | some u => s.acc v + s.acc u⟩

Uses 1 · Used by 2

Statement usesState of pointer jumping for suffix sums

Used byPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds · State after \(t\) rounds of pointer jumping for suffix sums

DefinitionState after \(t\) rounds of pointer jumping for suffix sums#✓fully proved

Given a partial successor function \(\mathrm{succ}\) on nodes \(0, \dots, n-1\), values \(x_v\) in an additive monoid \(M\) and \(t \in \mathbb{N}\), the state after \(t\) rounds is obtained from the initial state (pointers \(\mathrm{succ}(v)\), sums \(x_v\)) by applying one round of pointer jumping \(t\) times.

def rounds (succ : Fin n → Option (Fin n)) (x : Fin n → M) : ℕ → State n M
  | 0 => init succ x
  | t + 1 => round (rounds succ x t)

Uses 3 · Used by 3

Statement usesState of pointer jumping for suffix sums · Initial state of pointer jumping for suffix sums · One round of pointer jumping for suffix sums

Used byPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds · Pointer-jumping sums are the suffix sums once \(n \le 2^t\) · The invariant of pointer jumping for suffix sums

TheoremThe invariant of pointer jumping for suffix sums#✓fully proved

Let \(\mathrm{succ}\) be a partial successor function on nodes \(0, \dots, n-1\) and \(x_v\) values in an additive monoid \(M\). For every \(t \in \mathbb{N}\) and every node \(v\), after \(t\) rounds of pointer jumping the pointer of \(v\) is the node reached from \(v\) in \(2^t\) steps along \(\mathrm{succ}\) (undefined if the list ends sooner), and the sum of \(v\) is the sum, in list order, of the values of the nodes reached from \(v\) in \(0, 1, \dots, 2^t - 1\) steps (a missing node contributes \(0\)).

theorem rounds_spec : ∀ t v, (rounds succ x t).ptr v = jump succ (2 ^ t) v ∧
    (rounds succ x t).acc v = segSum succ x (2 ^ t) v

Uses 5 · Used by 1

Statement usesState of pointer jumping for suffix sums · State after \(t\) rounds of pointer jumping for suffix sums · Segment sums · Iterated successor

Proof usesSegment sums add up

Used byPointer-jumping sums are the suffix sums once \(n \le 2^t\)

TheoremPointer-jumping sums are the suffix sums once \(n \le 2^t\)#✓fully proved

Let \(\mathrm{succ}\) be a partial successor function on nodes \(0, \dots, n-1\) under which every list ends, that is, from every node, the node reached in \(n\) steps along \(\mathrm{succ}\) is undefined, and let \(x_v\) be values in an additive monoid \(M\). If \(t \in \mathbb{N}\) satisfies \(n \le 2^t\), then for every node \(v\) the sum of \(v\) after \(t\) rounds of pointer jumping is the suffix sum of \(v\): the sum, in list order, of the values from \(v\) to the end of its list.

theorem rounds_acc (hs : Terminates succ) {t : ℕ} (ht : n ≤ 2 ^ t) (v : Fin n) :
    (rounds succ x t).acc v = suffixSum succ x v

Uses 8 · Used by 1

Statement usesState of pointer jumping for suffix sums · State after \(t\) rounds of pointer jumping for suffix sums · Suffix sums · Terminating successor functions

Proof usesThe invariant of pointer jumping for suffix sums · Segment sums · Segment sums add up · Iterated successor

Used byPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds

DefinitionPointer-jumping state as arrays#✓fully proved

A suffix-sum pointer-jumping state on \(n\) nodes is stored as a pair of arrays of length \(n\): the array whose entry \(v\) is the pointer of node \(v\), and the array whose entry \(v\) is the accumulated value of node \(v\).

Evaluating the rounds of pointer jumping directly re-reads earlier rounds at every query, a cost exponential in the number of rounds; on arrays each round costs \(O(n)\) operations.

def tabulate (s : State n M) : Array (Option (Fin n)) × Array M :=
  (Array.ofFn s.ptr, Array.ofFn s.acc)

Uses 1 · Used by 2

Statement usesState of pointer jumping for suffix sums

Used byPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds · Arrays after \(t\) rounds of pointer jumping for suffix sums

DefinitionOne round of pointer jumping on arrays#✓fully proved

Given an array \(P\) of pointers (each a node among \(0, \dots, n-1\) or undefined) and an array \(S\) of sums in an additive monoid \(M\), one round returns arrays \(P'\) and \(S'\) of length \(n\) where, for each node \(v\): if \(P[v]\) is undefined, then \(P'[v]\) is undefined and \(S'[v] = S[v]\); if \(P[v] = u\), then \(P'[v] = P[u]\) and \(S'[v] = S[v] + S[u]\). A read outside an array gives an undefined pointer or the sum \(0\).

def roundTab (s : Array (Option (Fin n)) × Array M) : Array (Option (Fin n)) × Array M :=
  (Array.ofFn fun v : Fin n => (s.1.getD v none).bind fun u => s.1.getD u none,
    Array.ofFn fun v : Fin n =>
      match s.1.getD v none with
      | none => s.2.getD v 0
      | some u => s.2.getD v 0 + s.2.getD u 0)

Used by 2

Used byPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds · Arrays after \(t\) rounds of pointer jumping for suffix sums

DefinitionArrays after \(t\) rounds of pointer jumping for suffix sums#✓fully proved

Given a partial successor function \(\mathrm{succ}\) on nodes \(0, \dots, n-1\) and values \(x_v\) in an additive monoid \(M\), the pair of arrays after \(0\) rounds stores the pointers \(\mathrm{succ}(v)\) and the sums \(x_v\), and the pair after \(t + 1\) rounds is one round of pointer jumping on arrays applied to the pair after \(t\) rounds.

def roundsTab (succ : Fin n → Option (Fin n)) (x : Fin n → M) :
    ℕ → Array (Option (Fin n)) × Array M
  | 0 => tabulate (init succ x)
  | t + 1 => roundTab (roundsTab succ x t)

Uses 3 · Used by 2

Statement usesInitial state of pointer jumping for suffix sums · One round of pointer jumping on arrays · Pointer-jumping state as arrays

Used bySuffix sums by pointer jumping on arrays · Pointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds

DefinitionSuffix sums by pointer jumping on arrays#✓fully proved

Given a partial successor function \(\mathrm{succ}\) on nodes \(0, \dots, n-1\) and values \(x_v\) in an additive monoid \(M\), this is the array of sums obtained after \(\lceil \log_2 n \rceil\) rounds (the least \(k\) with \(n \le 2^k\)) of pointer jumping on arrays, starting from the pointers \(\mathrm{succ}(v)\) and the sums \(x_v\).

When every list ends, entry \(v\) is the suffix sum of node \(v\).

def listSums (succ : Fin n → Option (Fin n)) (x : Fin n → M) : Array M :=
  (roundsTab succ x (Nat.clog 2 n)).2

Uses 1 · Used by 1

Statement usesArrays after \(t\) rounds of pointer jumping for suffix sums

Used byPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds

TheoremPointer jumping computes all suffix sums in \(\lceil \log_2 n \rceil\) rounds#✓fully proved

Let \(\mathrm{succ}\) be a partial successor function on nodes \(0, \dots, n-1\) under which every list ends, that is, from every node, the node reached in \(n\) steps along \(\mathrm{succ}\) is undefined, and let \(x_v\) be values in an additive monoid \(M\). Then for every node \(v\), entry \(v\) of the array of sums computed by \(\lceil \log_2 n \rceil\) rounds of pointer jumping on arrays is the suffix sum of \(v\): the sum, in list order, of the values from \(v\) to the end of its list.

theorem listSums_getD (hs : Terminates succ) (v : Fin n) :
    (listSums succ x).getD v 0 = suffixSum succ x v

Uses 10

Statement usesSuffix sums by pointer jumping on arrays · Suffix sums · Terminating successor functions

Proof usesState of pointer jumping for suffix sums · One round of pointer jumping for suffix sums · One round of pointer jumping on arrays · State after \(t\) rounds of pointer jumping for suffix sums · Arrays after \(t\) rounds of pointer jumping for suffix sums · Pointer-jumping sums are the suffix sums once \(n \le 2^t\) · Pointer-jumping state as arrays

34 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.