Boyer–Moore string-search algorithm

DefinitionBoyer–Moore preprocessing#✓fully proved

Given a pattern \(p = p_0 \cdots p_{m-1}\) over the alphabet \(\{0, \dots, \sigma - 1\}\), this computes a bad-character table \(B\) of length \(\sigma\) and a strong good-suffix table \(G\) of length \(m\). The table \(B\) starts with every entry equal to \(m\), and then for \(k = 0, 1, \dots, m - 2\) in turn the entry \(B_{p_k}\) is set to \(m - 1 - k\). For \(G\), let \(s_i\) be the length of the longest common suffix of \(p_0 \cdots p_i\) and \(p\), computed with the Z algorithm on the reversed pattern. The table \(G\) starts with every entry equal to \(m\); then for \(i = m - 1, \dots, 0\) in turn, if \(s_i = i + 1\), every entry \(G_j\) with \(j < m - 1 - i\) that still equals \(m\) is set to \(m - 1 - i\); finally, for \(i = 0, 1, \dots, m - 2\) in turn, the entry \(G_{m - 1 - s_i}\) is set to \(m - 1 - i\).

The event cost includes table slots, copies, fill iterations and canonical Z events; it does not count machine instructions or unbounded-integer bit operations.

Cslib.Algorithms.Lean.StringMatching.BoyerMoore.preprocess · 17 lines

public def preprocess {σ m : Nat} (p : Vector (Fin σ) m) :
    TimeM Nat (Vector Nat σ × Vector Nat m) := do
  TimeM.tick σ
  let bad := Vector.replicate σ m
  if hm : 0 < m then do
    let bad ← badScan p 0 bad
    TimeM.tick m
    let reversed := p.reverse
    let z ← computeZ reversed
    TimeM.tick m
    let suffix := z.reverse
    TimeM.tick m
    let filled ← borderScan suffix m (by omega) 0 (Vector.replicate m m)
    let good ← suffixScan suffix 0 filled.2
    pure (bad, good)
  else
    pure (bad, Vector.replicate m m)

Uses 1 · Used by 11

Statement usesZ-algorithm

Used byBoyer–Moore matcher for all occurrences · Boyer–Moore with a pattern longer than the text · Boyer–Moore returns offsets in strictly increasing order · Worst-case cost of Boyer–Moore matching · Exact Boyer–Moore cost when pattern and text repeat the same letter · Exact Boyer–Moore cost when the pattern repeats one letter and ends in another, which alone makes up the text · Boyer–Moore returns exactly the occurrences · Bad-character table of Boyer–Moore preprocessing · The full-match shift is the least period of the pattern · Good-suffix table of Boyer–Moore preprocessing · Cost of Boyer–Moore preprocessing

TheoremCost of Boyer–Moore preprocessing#✓fully proved

For a pattern of length \(m\) over an alphabet of size \(\sigma\), the event cost of the Boyer–Moore preprocessing is at most \(\sigma\) when \(m = 0\) and at most \(\sigma + 10m - 6\) when \(m \ge 1\).

The cost counts the selected events of the preprocessor, including initialization of the alphabet table; it is not a word-RAM or bit-cost bound.

public theorem preprocess_time_le {σ m : Nat} (p : Vector (Fin σ) m) :
    (preprocess p).time ≤ if m = 0 then σ else σ + 10 * m - 6

Uses 3 · Used by 1

Statement usesBoyer–Moore preprocessing

Proof usesZ-algorithm · Linear upper bound for the Z-algorithm

Used byWorst-case cost of Boyer–Moore matching

TheoremBad-character table of Boyer–Moore preprocessing#✓fully proved

Let \(p = p_0 \cdots p_{m-1}\) be a pattern over the alphabet \(\{0, \dots, \sigma - 1\}\) and let \(B\) be the bad-character table computed by the Boyer–Moore preprocessing of \(p\). For every symbol \(c\), either \(B_c = m\) and \(p_k \ne c\) for every \(k\) with \(k + 1 < m\), or there is \(j\) with \(j + 1 < m\) and \(p_j = c\) such that \(B_c = m - 1 - j\) and every \(k\) with \(k + 1 < m\) and \(p_k = c\) satisfies \(k \le j\).

Thus \(B_c\) is the distance from the last position of \(p\) to the rightmost occurrence of \(c\) before that position, or \(m\) if \(c\) does not occur there.

public theorem preprocess_badCharacter {σ m : Nat} (p : Vector (Fin σ) m) (c : Fin σ) :
    ((preprocess p).ret.1[c.val] = m ∧
      ∀ (k : Nat) (hk : k + 1 < m), p[k] ≠ c) ∨
    ∃ (j : Nat) (hj : j + 1 < m), p[j] = c ∧
      (preprocess p).ret.1[c.val] = m - 1 - j ∧
      ∀ (k : Nat) (hk : k + 1 < m), p[k] = c → k ≤ j

Uses 2 · Used by 2

Statement usesBoyer–Moore preprocessing

Proof usesZ-algorithm

Used byExact Boyer–Moore cost when the pattern repeats one letter and ends in another, which alone makes up the text · Boyer–Moore returns exactly the occurrences

TheoremGood-suffix table of Boyer–Moore preprocessing#✓fully proved

Let \(p = p_0 \cdots p_{m-1}\) be a pattern over the alphabet \(\{0, \dots, \sigma - 1\}\), let \(G\) be the good-suffix table computed by the Boyer–Moore preprocessing of \(p\), and let \(i < m\). Call a positive integer \(e\) an admissible shift at \(i\) if \(p_{t - e} = p_t\) for every \(t < m\) with \(i < t\) and \(e \le t\), and \(p_{i - e} \ne p_i\) whenever \(e \le i\). Then \(1 \le G_i \le m\) and \(G_i\) is the least admissible shift at \(i\).

After a mismatch at position \(i\), shifting by \(G_i\) keeps the matched suffix \(p_{i+1} \cdots p_{m-1}\) aligned where it overlaps and, when \(G_i \le i\), places the symbol \(p_{i - G_i} \ne p_i\) under the mismatched position.

public theorem preprocess_goodSuffix {σ m : Nat} (p : Vector (Fin σ) m) (i : Fin m) :
    let d := (preprocess p).ret.2[i.val]
    0 < d ∧ d ≤ m ∧
      (∀ t : Fin m, i.val < t.val → d ≤ t.val → p[t.val - d] = p[t.val]) ∧
      (d ≤ i.val → p[i.val - d] ≠ p[i.val]) ∧
      ∀ e, 0 < e →
        (∀ t : Fin m, i.val < t.val → e ≤ t.val → p[t.val - e] = p[t.val]) →
        (e ≤ i.val → p[i.val - e] ≠ p[i.val]) → d ≤ e

Uses 3 · Used by 8

Statement usesBoyer–Moore preprocessing

Proof usesZ-algorithm · Z-values are longest common prefix lengths

Used byBoyer–Moore matcher for all occurrences · Boyer–Moore with a pattern longer than the text · Boyer–Moore returns offsets in strictly increasing order · Worst-case cost of Boyer–Moore matching · Exact Boyer–Moore cost when pattern and text repeat the same letter · Exact Boyer–Moore cost when the pattern repeats one letter and ends in another, which alone makes up the text · Boyer–Moore returns exactly the occurrences · The full-match shift is the least period of the pattern

TheoremThe full-match shift is the least period of the pattern#✓fully proved

Let \(p = p_0 \cdots p_{m-1}\) be a nonempty pattern over the alphabet \(\{0, \dots, \sigma - 1\}\) and let \(G\) be the good-suffix table computed by the Boyer–Moore preprocessing of \(p\). Then \(1 \le G_0 \le m\), \(p_{t - G_0} = p_t\) for every \(t < m\) with \(G_0 \le t\), and \(G_0 \le e\) for every positive integer \(e\) such that \(p_{t - e} = p_t\) for every \(t < m\) with \(e \le t\). That is, \(G_0\) is the least positive period of \(p\).

So after a full match the matcher may shift by \(G_0\) without discarding overlapping occurrences.

public theorem preprocess_fullMatch {σ m : Nat} (p : Vector (Fin σ) m) (hm : 0 < m) :
    let d := (preprocess p).ret.2[0]
    0 < d ∧ d ≤ m ∧
      (∀ t : Fin m, d ≤ t.val → p[t.val - d] = p[t.val]) ∧
      ∀ e, 0 < e → (∀ t : Fin m, e ≤ t.val → p[t.val - e] = p[t.val]) → d ≤ e

Uses 2 · Used by 2

Statement usesBoyer–Moore preprocessing

Proof usesGood-suffix table of Boyer–Moore preprocessing

Used byExact Boyer–Moore cost when pattern and text repeat the same letter · Boyer–Moore returns exactly the occurrences

DefinitionBoyer–Moore matcher for all occurrences#✓fully proved

Let \(p = p_0 \cdots p_{m-1}\) and \(t = t_0 \cdots t_{n-1}\) be words over the alphabet \(\{0, \dots, \sigma - 1\}\). The matcher returns a list of offsets together with a cost. If \(m = 0\) it returns \(0, 1, \dots, n\) at cost \(n + 1\), and if \(n < m\) it returns the empty list at cost \(0\). Otherwise it charges \(m + n\) for converting \(p\) and \(t\) to arrays, computes the bad-character table \(B\) and the strong good-suffix table \(G\) of \(p\) with the Boyer–Moore preprocessing and charges the cost of that preprocessing, and then visits alignments \(s\), starting from \(s = 0\), as long as \(s + m \le n\). At each alignment it charges \(1\) and compares \(p_r\) with \(t_{s + r}\) for \(r = m - 1, m - 2, \dots, 0\), charging \(1\) per comparison and stopping at the first mismatch. If all \(m\) letters agree, it records \(s\), charges \(2\) and moves to the alignment \(s + G_0\). If the first mismatch is at position \(i\), it charges \(1\) and moves to the alignment \(s + \max(G_i, B_c - m + 1 + i)\), where \(c = t_{s + i}\) and the maximum is taken in the integers. Finally it charges \(1\) for each recorded offset and returns the recorded offsets in the order they were found.

The result is every occurrence of \(p\) in \(t\), in increasing order and including overlaps. The cost counts these selected events, not machine instructions.

public def boyerMooreMatches {σ : Nat} (pattern text : List (Fin σ)) :
    TimeM Nat (List Nat) :=
  Prod.fst <$> matchWithCounts pattern text

Uses 2 · Used by 8

Statement usesBoyer–Moore preprocessing · Good-suffix table of Boyer–Moore preprocessing

Used byBoyer–Moore agrees with the naive matcher · Boyer–Moore with the empty pattern · Boyer–Moore with a pattern longer than the text · Boyer–Moore returns offsets in strictly increasing order · Worst-case cost of Boyer–Moore matching · Exact Boyer–Moore cost when pattern and text repeat the same letter · Exact Boyer–Moore cost when the pattern repeats one letter and ends in another, which alone makes up the text · Boyer–Moore returns exactly the occurrences

TheoremBoyer–Moore with the empty pattern#✓fully proved

For every text \(t\) of length \(n\) over the alphabet \(\{0, \dots, \sigma - 1\}\), the Boyer–Moore matcher with the empty pattern and text \(t\) returns the list \(0, 1, \dots, n\) of all offsets from \(0\) to \(n\) in increasing order, at cost \(n + 1\).

@[simp] public theorem boyerMooreMatches_nil_pattern {σ : Nat} (text : List (Fin σ)) :
    boyerMooreMatches [] text = ⟨List.range (text.length + 1), text.length + 1⟩

Uses 1 · Used by 3

Statement usesBoyer–Moore matcher for all occurrences

Used byBoyer–Moore returns offsets in strictly increasing order · Worst-case cost of Boyer–Moore matching · Boyer–Moore returns exactly the occurrences

TheoremBoyer–Moore with a pattern longer than the text#✓fully proved

Let \(p\) and \(t\) be words over the alphabet \(\{0, \dots, \sigma - 1\}\). If \(t\) is strictly shorter than \(p\), then the Boyer–Moore matcher with pattern \(p\) and text \(t\) returns the empty list at cost \(0\): no preprocessing or search events are charged.

@[simp] public theorem boyerMooreMatches_of_length_lt {σ : Nat}
    (pattern text : List (Fin σ)) (h : text.length < pattern.length) :
    boyerMooreMatches pattern text = pure []

Uses 3 · Used by 3

Statement usesBoyer–Moore matcher for all occurrences

Proof usesBoyer–Moore preprocessing · Good-suffix table of Boyer–Moore preprocessing

Used byBoyer–Moore returns offsets in strictly increasing order · Worst-case cost of Boyer–Moore matching · Boyer–Moore returns exactly the occurrences

TheoremBoyer–Moore returns exactly the occurrences#✓fully proved

For all words \(p\) and \(t\) over the alphabet \(\{0, \dots, \sigma - 1\}\) and every natural number \(k\), the offset \(k\) belongs to the list returned by the Boyer–Moore matcher with pattern \(p\) and text \(t\) if and only if \(p\) occurs in \(t\) at offset \(k\), that is, \(k \le |t|\) and \(p\) is a prefix of the word obtained from \(t\) by deleting its first \(k\) letters. In particular, overlapping occurrences are all returned.

public theorem mem_boyerMooreMatches_iff {σ : Nat} (pattern text : List (Fin σ))
    (offset : Nat) : offset ∈ (boyerMooreMatches pattern text).ret ↔
    StringMatching.MatchAt pattern text offset

Uses 8 · Used by 1

Statement usesPattern match at an offset · Boyer–Moore matcher for all occurrences

Proof usesBoyer–Moore preprocessing · Bad-character table of Boyer–Moore preprocessing · The full-match shift is the least period of the pattern · Good-suffix table of Boyer–Moore preprocessing · Boyer–Moore with the empty pattern · Boyer–Moore with a pattern longer than the text

Used byBoyer–Moore agrees with the naive matcher

TheoremBoyer–Moore returns offsets in strictly increasing order#✓fully proved

For all words \(p\) and \(t\) over the alphabet \(\{0, \dots, \sigma - 1\}\), the list of offsets returned by the Boyer–Moore matcher with pattern \(p\) and text \(t\) is strictly increasing: each entry is smaller than every entry after it.

public theorem boyerMooreMatches_pairwise {σ : Nat} (pattern text : List (Fin σ)) :
    (boyerMooreMatches pattern text).ret.Pairwise (· < ·)

Uses 5 · Used by 1

Statement usesBoyer–Moore matcher for all occurrences

Proof usesBoyer–Moore preprocessing · Good-suffix table of Boyer–Moore preprocessing · Boyer–Moore with the empty pattern · Boyer–Moore with a pattern longer than the text

Used byBoyer–Moore agrees with the naive matcher

TheoremBoyer–Moore agrees with the naive matcher#✓fully proved

For all words \(p\) and \(t\) over the alphabet \(\{0, \dots, \sigma - 1\}\), the list of offsets returned by the Boyer–Moore matcher with pattern \(p\) and text \(t\) equals the list returned by the naive matcher with pattern \(p\) and text \(t\), entry by entry and in the same order. Only the returned lists are compared, not the costs.

public theorem boyerMooreMatches_eq_naiveMatches {σ : Nat} (pattern text : List (Fin σ)) :
    (boyerMooreMatches pattern text).ret = (naiveMatches pattern text).ret

Uses 7

Statement usesBoyer–Moore matcher for all occurrences · Naive string matcher

Proof usesPattern match at an offset · Boyer–Moore returns offsets in strictly increasing order · Boyer–Moore returns exactly the occurrences · Correctness of naive string matching · Naive matching reports shifts in increasing order

TheoremWorst-case cost of Boyer–Moore matching#✓fully proved

Let \(p\) and \(t\) be words over the alphabet \(\{0, \dots, \sigma - 1\}\) of lengths \(m\) and \(n\). The cost of the Boyer–Moore matcher with pattern \(p\) and text \(t\) is at most \(n + 1\) if \(m = 0\), at most \(0\) if \(n < m\), and at most \(\sigma + n + 11m - 6 + (m + 4)(n - m + 1)\) if \(1 \le m \le n\).

The cost counts the matcher's selected events, not machine instructions. The bound is quadratic and does not assert linear all-match comparison complexity or machine runtime.

public theorem boyerMooreMatches_time_le {σ : Nat} (pattern text : List (Fin σ)) :
    (boyerMooreMatches pattern text).time ≤
      if pattern.length = 0 then text.length + 1
      else if text.length < pattern.length then 0
      else σ + text.length + 11 * pattern.length - 6 +
        (pattern.length + 4) * (text.length - pattern.length + 1)

Uses 6

Statement usesBoyer–Moore matcher for all occurrences

Proof usesBoyer–Moore preprocessing · Good-suffix table of Boyer–Moore preprocessing · Cost of Boyer–Moore preprocessing · Boyer–Moore with the empty pattern · Boyer–Moore with a pattern longer than the text

TheoremExact Boyer–Moore cost when pattern and text repeat the same letter#✓fully proved

Let \(x\) be a letter of the alphabet \(\{0, \dots, \sigma - 1\}\), let \(m\) and \(n\) be natural numbers with \(0 < m \le n\), and write \(x^k\) for the word of \(k\) copies of \(x\). The cost of the Boyer–Moore matcher with pattern \(x^m\) and text \(x^n\) equals \(m + n + P + (m + 4)(n - m + 1)\), where \(P\) is the cost of the Boyer–Moore preprocessing of the pattern \(x^m\).

Of this cost, \(m(n - m + 1)\) counts character tests: every alignment is a match and compares all \(m\) pattern letters.

public theorem boyerMooreMatches_time_replicate {σ : Nat} (x : Fin σ) (m n : Nat)
    (hm : 0 < m) (hlen : m ≤ n) :
    (boyerMooreMatches (List.replicate m x) (List.replicate n x)).time =
      m + n + (preprocess (List.replicate m x).toArray.toVector).time +
        (m + 4) * (n - m + 1)

Uses 4

Statement usesBoyer–Moore preprocessing · Boyer–Moore matcher for all occurrences

Proof usesThe full-match shift is the least period of the pattern · Good-suffix table of Boyer–Moore preprocessing

TheoremExact Boyer–Moore cost when the pattern repeats one letter and ends in another, which alone makes up the text#✓fully proved

Exact Boyer–Moore cost when the pattern repeats one letter and ends in another, which alone makes up the text. Let \(a \ne b\) be letters of the alphabet \(\{0, \dots, \sigma - 1\}\) and let \(m\) and \(n\) be natural numbers with \(2 \le m \le n\). Write \(a^{m-1}b\) for the word of \(m - 1\) copies of \(a\) followed by one \(b\), and \(b^n\) for the word of \(n\) copies of \(b\). The cost of the Boyer–Moore matcher with pattern \(a^{m-1}b\) and text \(b^n\) equals \(m + n + P + 4\lfloor n/m \rfloor\), where \(P\) is the cost of the Boyer–Moore preprocessing of the pattern \(a^{m-1}b\).

On these inputs every alignment makes two character tests and is followed by a shift by \(m\).

public theorem boyerMooreMatches_time_replicate_append {σ : Nat} (a b : Fin σ)
    (m n : Nat) (hab : a ≠ b) (hm : 2 ≤ m) (hlen : m ≤ n) :
    (boyerMooreMatches (List.replicate (m - 1) a ++ [b]) (List.replicate n b)).time =
      m + n + (preprocess (List.replicate (m - 1) a ++ [b]).toArray.toVector).time +
        4 * (n / m)

Uses 4

Statement usesBoyer–Moore preprocessing · Boyer–Moore matcher for all occurrences

Proof usesBad-character table of Boyer–Moore preprocessing · Good-suffix table of Boyer–Moore preprocessing

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.