# Proof techniques for string algorithms?

I'm currently reading through the tome "Algorithms on Strings, Trees, and Sequences" by Dan Gusfield, and I find the proofs to be extremely case analysis heavy and full of finicky +-1s. This seems very error prone to program.

I was hoping for a more "conceptual" way to build string algorithms, where we first construct a toolkit of basic objects that we then use. I was hoping that prefixes, suffixes, and the Z algorithm would be those. But they seem too level to construct something like Boyer-Moore or Aho-Corasick.

As an analogy for some kind of abstract algebraic flavoured approach, like using matroids for greedy algorithms to capture the "hard" part of the analysis.

So my question is, are there nice algebraic structures that govern string algorithms which can be used to present and implement them more elegantly?

There is some work on developing an algebraic or grammar-based view of string algorithms, for example

Robert Giegerich, Carsten Meyer, Peter Steffen: A discipline of dynamic programming over sequence data. Sci. Comput. Program. 51(3): 215-263 (2004)

Robert Giegerich, Hélène Touzet: Modeling Dynamic Programming Problems over Sequences and Trees with Inverse Coupled Rewrite Systems. Algorithms 7(1): 62-144 (2014)

These approaches deal with string problems that are solved by dynamic programming such as the computation of edit distance or local alignments or comparison of RNA secondary structures. These problems are more difficult in terms of the running time of the best algorithms than the exact pattern matching problem that is solved by Boyer-Moore.

A more conceptual or programmer-friendly approach for exact pattern matching would be to use the right data structures such as suffix arrays or suffix trees. Many pattern matching algorithms become simpler when these data structures are used as a black box or augmented in some relatively easy way.

• Thanks for the references! While I agree that once one has a suffix tree, it's nice to work with, analysing the algorithm that builds the suffix tree(say, Ukkonen's) still relies on low-level reasoning I was hoping to "algebrise" away Feb 12, 2020 at 19:48
• @SiddharthBhat, if you're asking specifically about how to obtain a verifiably correct implementation of a suffix tree algorithm, I suggest asking about that separately, since that's a much more focused question. Finding a way to algebrise the derivation of the algorithm might be one way to achieve that, but there might be other ways as well.
– D.W.
Feb 13, 2020 at 6:53