Partial Evaluation of Pattern Matching in Strings, revisited

Resumé

Specializing string matchers is a canonical example of partial evaluation.
A naive implementation of a string matcher repeatedly matches a
pattern against every substring of the data string; this operation should
intuitively benefit from specializing the matcher with respect to the pattern.
In practice, however, producing an efficient implementation by
performing this specialization using standard partial-evaluation techniques
has been found to require non-trivial binding-time improvements. Starting
with a naive matcher, we thus present a derivation of a binding-time
improved string matcher. We prove its correctness and show that specialization
with respect to a pattern yields a matcher with code size linear
in the length of the pattern and running time linear in the length of its
input. We then consider several variants of matchers that specialize well,
amongst them the first such matcher presented in the literature, and we
demonstrate how variants can be derived from each other systematically.