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

<p>Robert Giegerich, Carsten Meyer, Peter Steffen:
<a href="https://doi.org/10.1016/j.scico.2003.12.005" rel="nofollow noreferrer">A discipline of dynamic programming over sequence data</a>. Sci. Comput. Program. 51(3): 215-263 (2004)</p>

<p>Robert Giegerich, Hélène Touzet:
<a href="https://doi.org/10.3390/a7010062" rel="nofollow noreferrer">Modeling Dynamic Programming Problems over Sequences and Trees with Inverse Coupled Rewrite Systems</a>. Algorithms 7(1): 62-144 (2014)</p>

<p>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. </p>

<p>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.</p>

CC BY-SA 4.0
2020-02-12T19:48:04.357Z
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
Siddharth Bhat
CC BY-SA 4.0
2020-02-13T06:53:13.637Z
@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.
CC BY-SA 4.0
2020-02-12T19:40:10.820Z
2020-02-12T19:40:10.820Z
Christian Komusiewicz
<p>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. </p>

<p>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.</p>

<p>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.</p>

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

CC BY-SA 4.0
2020-02-12T10:58:03.800Z
Orthogonal to your question, but Strother Moore agrees with you, and verified his algorithm in a fheorem prover, see his paper [A Mechanically Checked Proof of the
Correctness of the Boyer-Moore Fast
String Searching Algorithm](https://www.cs.utexas.edu/~moore/publications/moore-martinez-09.pdf).
Martin Berger
<string-matching><string-search><analysis-of-algorithms>
Proof techniques for string algorithms?
Siddharth Bhat
# Proof techniques for string algorithms?

(Asked by: username_0 on 2020-02-12)

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?

**Tags:** string-matching, string-search, analysis-of-algorithms
> **Comments:**
> **username_1**: Orthogonal to your question, but Strother Moore agrees with you, and verified his algorithm in a fheorem prover, see his paper [A Mechanically Checked Proof of the Correctness of the Boyer-Moore Fast String Searching Algorithm](https://www.cs.utexas.edu/~moore/publications/moore-martinez-09.pdf).  

---

## 1 answers

### Answer by username_2 on 2020-02-12. Score: 2 | Accepted answer

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](https://doi.org/10.1016/j.scico.2003.12.005). 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](https://doi.org/10.3390/a7010062). 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.

> **Comments:**
> **username_0**: 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  
> **username_3**: @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.  

---

