Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. On Obtaining Knuth, Morris, and Pratt's String Matcher by Partial Evaluation. ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ASIA-PEPM '02. July 2002.
Obtaining a KMP-like string matcher is a canonical example of partial
evaluation: starting from the naive, quadratic program checking whether
a pattern occurs in a text, one ensures that backtracking can be performed
at partial-evaluation time (a binding-time shift that yields a staged string
matcher); specializing the resulting staged program yields residual programs that do not back up on the text, a la KMP.
The authors formally prove that the staged string matcher performs the same sequence of comparisons as the KMP string matcher.
The authors make extensive use of operational semantics, both big-step (for expressions) and small-step (for statements).
Posted to general by Ehud Lamm on 12/12/02; 2:40:15 AM