On Specialization of a Program Model of Naive Pattern Matching in Strings (Extended Abstract)

TL;DR

This paper proves that the naive pattern matching program can be automatically specialized into the KMP algorithm for any pattern using a specific relation, achieving linear-time search, but current automation tools are insufficient to reproduce the proof.

Contribution

It demonstrates the automatic specialization of naive pattern matching to KMP algorithm for any pattern using the Higman-Kruskal relation, advancing program specialization techniques.

Findings

Residual program finds first pattern occurrence in linear time

Automated specialization can produce KMP for static patterns

Current automation tools cannot fully reproduce the proof

Abstract

We have proved that for any pattern p the tail recursive program model of naive pattern matching may be automatically specialized w.r.t. the pattern p to a specialized version of the so-called KMP-algorithm, using the Higman-Kruskal relation that controls the unfolding/folding. Given an input string, the corresponding residual program finds the first occurrence of p in the string in linear time on the string length. The current state of the automated program specialization art based on unfolding/folding is too weak in order to be able to reproduce the proof, done by hands, of the uniform property above, while it known before that program specialization is sometimes able to produce the KMP-algorithm for a few concrete static patterns.