Z algorithm

DefinitionZ-algorithm#✓fully proved

Given a word \(s = s_0 \dots s_{n-1}\) over a type \(\alpha\) with a Boolean equality test, Gusfield's Z-box algorithm returns an array \(Z\) of \(n\) natural numbers with \(Z_0 = n\). It visits \(i = 1, \dots, n - 1\) in turn, keeping a box \([\ell, r)\), initially empty, that is the rightmost match of a prefix of \(s\) found so far. If \(\ell \le i < r\) and \(Z_{i - \ell} < r - i\), it sets \(Z_i = Z_{i - \ell}\). Otherwise it finds \(Z_i\) by comparing symbols directly, starting at offset \(r - i\) if \(i < r\) and at offset \(0\) if not, and if \(Z_i > 0\) the box becomes \([i, i + Z_i)\). When the equality test is lawful, \(Z_i\) is the length of the longest common prefix of \(s\) and its suffix \(s_i \dots s_{n-1}\). The cost counts one unit for each visited position \(i \ge 1\) and one unit for each symbol comparison; on the empty word the result is empty with cost \(0\).

public def computeZ {α : Type u} [BEq α] {n : Nat}
    (input : Vector α n) : TimeM Nat (Vector Nat n) :=
  if h : 0 < n then
    zScan input 1 ⟨(Vector.replicate n 0).set 0 n h, 0, ⟨0, by omega⟩⟩
  else
    pure (Vector.replicate n 0)

Used by 12

Used byBoyer–Moore preprocessing · Bad-character table of Boyer–Moore preprocessing · Good-suffix table of Boyer–Moore preprocessing · Cost of Boyer–Moore preprocessing · Z-values are at most the suffix length · Z-values are longest common prefix lengths · Z-array of a repeated symbol · Z-algorithm cost on a repeated symbol followed by a distinct one · Z-algorithm cost on a repeated symbol · Linear lower bound for the Z-algorithm · Linear upper bound for the Z-algorithm · The first Z-value is the word length

TheoremThe first Z-value is the word length#✓fully proved

Let \(\alpha\) be a type with a Boolean equality test. For every nonempty word of length \(n\) over \(\alpha\), the Z-array \(Z\) computed by the Z-algorithm has \(Z_0 = n\).

Gusfield leaves this entry undefined; this convention completes it.

public theorem computeZ_zero {α : Type u} [BEq α] {n : Nat}
    (input : Vector α n) (h : 0 < n) : (computeZ input).ret[0] = n

Uses 1 · Used by 2

Statement usesZ-algorithm

Used byZ-values are longest common prefix lengths · Z-array of a repeated symbol

TheoremZ-values are longest common prefix lengths#✓fully proved

Let \(\alpha\) be a type with a lawful Boolean equality test, let \(s = s_0 \dots s_{n-1}\) be a word over \(\alpha\), and let \(Z\) be the Z-array computed by the Z-algorithm on \(s\). For every position \(i < n\) and every natural number \(q\), \(q \le Z_i\) holds if and only if \(q \le n - i\) and \(s_k = s_{i+k}\) for all \(k < q\). Hence \(Z_i\) is the length of the longest common prefix of \(s\) and its suffix \(s_i \dots s_{n-1}\).

public theorem computeZ_prefix_iff {α : Type u} [BEq α] [LawfulBEq α] {n : Nat}
    (input : Vector α n) (i : Fin n) (q : Nat) :
    q ≤ (computeZ input).ret[i.val] ↔ q ≤ n - i.val ∧
      input.toList.take q = (input.toList.drop i.val).take q

Uses 2 · Used by 1

Statement usesZ-algorithm

Proof usesThe first Z-value is the word length

Used byGood-suffix table of Boyer–Moore preprocessing

TheoremZ-values are at most the suffix length#✓fully proved

Let \(\alpha\) be a type with a Boolean equality test, not necessarily lawful, and let \(s\) be a word of length \(n\) over \(\alpha\). For every position \(i < n\), the entry at \(i\) of the Z-array computed by the Z-algorithm on \(s\) is at most \(n - i\).

public theorem computeZ_getElem_le {α : Type u} [BEq α] {n : Nat}
    (input : Vector α n) (i : Fin n) : (computeZ input).ret[i.val] ≤ n - i.val

Uses 1

Statement usesZ-algorithm

TheoremLinear upper bound for the Z-algorithm#✓fully proved

Let \(\alpha\) be a type with a Boolean equality test, not necessarily lawful. On every word of length \(n\) over \(\alpha\), the Z-algorithm has cost at most \(3(n - 1)\), read as \(0\) when \(n = 0\), where the cost counts one unit for each visited position \(i \ge 1\) and one unit for each symbol comparison.

public theorem computeZ_time_le {α : Type u} [BEq α] {n : Nat}
    (input : Vector α n) : (computeZ input).time ≤ 3 * (n - 1)

Uses 1 · Used by 1

Statement usesZ-algorithm

Used byCost of Boyer–Moore preprocessing

TheoremLinear lower bound for the Z-algorithm#✓fully proved

Let \(\alpha\) be a type with a Boolean equality test, not necessarily lawful. On every word of length \(n\) over \(\alpha\), the Z-algorithm has cost at least \(n - 1\), where the cost counts one unit for each visited position \(i \ge 1\) and one unit for each symbol comparison.

public theorem computeZ_time_ge {α : Type u} [BEq α] {n : Nat}
    (input : Vector α n) : n - 1 ≤ (computeZ input).time

Uses 1

Statement usesZ-algorithm

TheoremZ-array of a repeated symbol#✓fully proved

Let \(\alpha\) be a type with a lawful Boolean equality test, let \(a \in \alpha\) and \(n \in \mathbb{N}\). The Z-array computed by the Z-algorithm on the word \(a^n\) has entry \(n - i\) at every position \(i < n\).

public theorem computeZ_replicate {α : Type u} [BEq α] [LawfulBEq α]
    (a : α) (n : Nat) :
    (computeZ (Vector.replicate n a)).ret = Vector.ofFn (fun i : Fin n => n - i.val)

Uses 2

Statement usesZ-algorithm

Proof usesThe first Z-value is the word length

TheoremZ-algorithm cost on a repeated symbol#✓fully proved

Let \(\alpha\) be a type with a lawful Boolean equality test, let \(a \in \alpha\) and \(n \in \mathbb{N}\). The Z-algorithm run on the word \(a^n\) has cost exactly \(2(n - 1)\), read as \(0\) when \(n = 0\), where the cost counts one unit for each visited position \(i \ge 1\) and one unit for each symbol comparison. Thus it makes \(n - 1\) visits and \(n - 1\) comparisons.

public theorem computeZ_replicate_time {α : Type u} [BEq α] [LawfulBEq α]
    (a : α) (n : Nat) : (computeZ (Vector.replicate n a)).time = 2 * (n - 1)

Uses 1

Statement usesZ-algorithm

TheoremZ-algorithm cost on a repeated symbol followed by a distinct one#✓fully proved

Let \(\alpha\) be a type with a lawful Boolean equality test and let \(a \ne b\) be elements of \(\alpha\). For every \(n \ge 1\), the Z-algorithm run on the word \(a^n b\) has cost exactly \(3n - 1\), where the cost counts one unit for each visited position \(i \ge 1\) and one unit for each symbol comparison. In terms of the input length \(N = n + 1\), this is \(3N - 4\).

public theorem computeZ_replicate_push_time {α : Type u} [BEq α] [LawfulBEq α]
    (a b : α) (hab : a ≠ b) (n : Nat) (hn : 0 < n) :
    (computeZ ((Vector.replicate n a).push b)).time = 3 * n - 1

Uses 1

Statement usesZ-algorithm

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.