String matching with finite automata

DefinitionTransition table of the string-matching automaton#✓fully proved

Let \(P\) be a pattern of length \(m\) over the alphabet \(\{0, \dots, A-1\}\) and write \(P_k\) for its prefix of length \(k\). This timed computation returns a table of \((m+1)A\) entries in \(\{0, \dots, m\}\), stored row by row: for each state \(q \le m\) and symbol \(a < A\), the entry at index \(qA + a\) is found by trying \(k = \min(m, q+1)\) and then each smaller value in turn, and is the first \(k\) for which \(P_k\) is a suffix of the word \(P_q a\) (the candidate \(k = 0\) is always accepted). The cost counts one unit for each candidate \(k\) tried, one for each symbol comparison executed when comparing \(P_k\) with the last \(k\) symbols of \(P_q a\) (left to right, stopping at the first mismatch), one for each move to a smaller candidate, and one for each table entry written.

def computeTransition {A : Nat} (pattern : List (Fin A)) :
    TimeM Nat (Vector (Fin (pattern.length + 1)) ((pattern.length + 1) * A)) :=
  Vector.ofFnM fun i => do
    let q ← typedTransitionCell pattern (rowOfIndex i) (columnOfIndex i)
    TimeM.tick 1
    pure q

Sources

• CLRS fourth edition section 32.3, decreasing-candidate row-major construction.

Used by 6

Used byCorrectness of the string-matching transition table · Cost bound for the string-matching transition table · Finite-automaton string matcher · Correctness of the finite-automaton matcher · Exact cost of the finite-automaton matcher · String-matching automaton

TheoremCorrectness of the string-matching transition table#✓fully proved

Let \(P\) be a pattern of length \(m\) over the alphabet \(\{0, \dots, A-1\}\) and write \(P_k\) for its prefix of length \(k\). For every state \(q \le m\) and symbol \(a < A\), the entry at index \(qA + a\) of the transition table of \(P\) is the greatest \(k \le m\) such that \(P_k\) is a suffix of the word \(P_q a\).

theorem computeTransition_spec {A : Nat} (pattern : List (Fin A))
    (q : Fin (pattern.length + 1)) (a : Fin A) :
    IsGreatest {k : Nat | k ≤ pattern.length ∧ pattern.take k <:+ pattern.take q.val ++ [a]}
      ((computeTransition pattern).ret.get ⟨q.val * A + a.val, by
        calc
          q.val * A + a.val < q.val * A + A := Nat.add_lt_add_left a.isLt _
          _ = (q.val + 1) * A := (Nat.succ_mul q.val A).symm
          _ ≤ (pattern.length + 1) * A :=
            Nat.mul_le_mul_right A (Nat.succ_le_of_lt q.isLt)⟩).val

Uses 1 · Used by 2

Statement usesTransition table of the string-matching automaton

Used byCorrectness of the finite-automaton matcher · The string-matching automaton tracks the longest matched prefix

TheoremCost bound for the string-matching transition table#✓fully proved

For every pattern of length \(m\) over the alphabet \(\{0, \dots, A-1\}\), the cost of computing its transition table is at most \(2A(m+1)^3\).

The cost counts executed candidates, symbol comparisons, failed decrements and table writes.

theorem computeTransition_time_le {A : Nat} (pattern : List (Fin A)) :
    (computeTransition pattern).time ≤ 2 * A * (pattern.length + 1) ^ 3

Uses 1

Statement usesTransition table of the string-matching automaton

DefinitionString-matching automaton#✓fully proved

For a pattern \(P\) of length \(m\) over the alphabet \(\{0, \dots, A-1\}\), the string-matching automaton of \(P\) is the deterministic finite automaton with states \(\{0, \dots, m\}\), input symbols \(\{0, \dots, A-1\}\), start state \(0\), accepting set \(\{m\}\), and transition from state \(q\) on symbol \(a\) given by the entry at index \(qA + a\) of the transition table of \(P\).

def patternAutomaton {A : Nat} (pattern : List (Fin A)) :
    Cslib.Automata.DA.FinAcc (Fin (pattern.length + 1)) (Fin A) :=
  let table := (computeTransition pattern).ret
  { start := 0
    tr := fun q a => table.get (flatIndex q a)
    accept := {q | q.val = pattern.length} }

Uses 1 · Used by 2

Statement usesTransition table of the string-matching automaton

Used byCorrectness of the finite-automaton matcher · The string-matching automaton tracks the longest matched prefix

TheoremThe string-matching automaton tracks the longest matched prefix#✓fully proved

Let \(P\) be a pattern of length \(m\) over the alphabet \(\{0, \dots, A-1\}\) and write \(P_k\) for its prefix of length \(k\). For every word \(w\) over this alphabet, the state that the string-matching automaton of \(P\) reaches from its start state after reading \(w\) is the greatest \(k \le m\) such that \(P_k\) is a suffix of \(w\).

theorem patternAutomaton_state {A : Nat} (pattern word : List (Fin A)) :
    IsGreatest {k : Nat | k ≤ pattern.length ∧ pattern.take k <:+ word}
      ((patternAutomaton pattern).mtr (patternAutomaton pattern).start word).val

Uses 2 · Used by 1

Statement usesString-matching automaton

Proof usesCorrectness of the string-matching transition table

Used byCorrectness of the finite-automaton matcher

DefinitionFinite-automaton string matcher#✓fully proved

Let \(P\) be a pattern of length \(m\) and \(T\) a text over the alphabet \(\{0, \dots, A-1\}\). This timed computation first computes the transition table of \(P\), then runs through \(T\) starting in state \(0\): on reading the \(i\)-th symbol \(a\) of \(T\) in state \(q\) it moves to the state given by the table entry at index \(qA + a\), and if that state is \(m\) it reports the shift \(i - m\). If \(m = 0\), the shift \(0\) is also reported before the scan. It returns the reported shifts in the order found. The cost is that of computing the table, plus two units for each symbol of \(T\) (a table lookup and an acceptance test), plus one unit for each reported shift.

The table is computed once, before the single pass over the text, and the scan does not reset after a match, so overlapping occurrences are reported.

def finiteAutomatonMatches {A : Nat} (pattern text : List (Fin A)) : TimeM Nat (List Nat) := do
  let table ← computeTransition pattern
  if pattern.length = 0 then do
    TimeM.tick 1
    scan table 0 0 (pure [0]) text
  else scan table 0 0 (pure []) text

Uses 1 · Used by 2

Statement usesTransition table of the string-matching automaton

Used byCorrectness of the finite-automaton matcher · Exact cost of the finite-automaton matcher

TheoremExact cost of the finite-automaton matcher#✓fully proved

For every pattern \(P\) and text \(T\) over the alphabet \(\{0, \dots, A-1\}\), where \(T\) has length \(n\), the cost of the finite-automaton matcher on \(P\) and \(T\) equals the cost of computing the transition table of \(P\), plus \(2n\), plus the number of shifts the matcher returns.

theorem finiteAutomatonMatches_time {A : Nat} (pattern text : List (Fin A)) :
    (finiteAutomatonMatches pattern text).time =
      (computeTransition pattern).time + 2 * text.length +
        (finiteAutomatonMatches pattern text).ret.length

Uses 2

Statement usesTransition table of the string-matching automaton · Finite-automaton string matcher

TheoremCorrectness of the finite-automaton matcher#✓fully proved

For every pattern \(P\) and text \(T\) over the alphabet \(\{0, \dots, A-1\}\), the list of shifts returned by the finite-automaton matcher equals the list returned by the naive string matcher.

So it is the complete increasing list of zero-based shifts at which \(P\) occurs in \(T\), including overlapping occurrences and, for the empty pattern, every boundary.

theorem finiteAutomatonMatches_ret {A : Nat} (pattern text : List (Fin A)) :
    (finiteAutomatonMatches pattern text).ret = (TimeM.naiveMatches pattern text).ret

Uses 9

Statement usesFinite-automaton string matcher · Naive string matcher

Proof usesPattern match at an offset · Transition table of the string-matching automaton · Correctness of the string-matching transition table · String-matching automaton · The string-matching automaton tracks the longest matched prefix · Correctness of naive string matching · Naive matching reports shifts in increasing order

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.