On obtaining Knuth, Morris, and Pratt''s string matcher by partial evaluation.
We present the first formal proof that partial evaluation of a quadratic string matcher can yield the precise behaviour of Knuth, Morris, and Pratt's linear string matcher.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. We are not aware, however, of any formal proof that partial evaluation of a staged string matcher precisely yields the KMP string matcher, or in fact any other specific string matcher.In this article, we present a staged string matcher and we formally prove that it performs the same sequence of comparisons between pattern and text as the KMP string matcher. To this end, we operationally specify each of the programming languages in which the matchers are written, and we formalize each sequence of comparisons with a trace semantics. We also state the (mild) conditions under which specializing the staged string matcher with respect to a pattern string provably yields a specialized string matcher whose size is proportional to the length of this pattern string and whose time complexity is proportional to the length of the text string. Finally, we show how tabulating one of the functions in this staged string matcher gives rise to the 'next' table of the original KMP algorithm.The method scales for obtaining other linear string matchers, be they known or new.
Introduction
Obtaining Knuth, Morris, and Pratt's linear string matcher out of a naive
quadratic string matcher is a traditional exercise in partial evaluation:
run match #pat , res
run PE #match , #pat ,
run match #pat, # , res
Given a static pattern, the partial evaluator should perform all backtracking
statically to produce a specialized matcher that traverses the text in linear
time.
Initially, the exercise was proposed by Futamura to illustrate Generalized
Partial Computation, a form of partial evaluation that memoizes the result of
dynamic tests when processing conditional branches [10]. 1 Subsequently, Consel
and Danvy pointed out that a binding-time improved (i.e., staged) quadratic
string matcher could also be specialized into a linear string matcher, using a
standard, Mix-style partial evaluator [7]. A number of publications followed,
showing either a range of binding-time improved string matchers or presenting
a range of partial evaluators integrating the binding-time improvement [1, 9, 11,
12, 15, 23, 24, 25].
After 15 years, however, we observe that
1. the KMP test, as it is called, appears to have had little impact, if any, on
the development of algorithms outside the field of partial evaluation, and
that
2. except for Grobauer and Lawall's recent work [13], issues such as the
precise characterization of time and space of specialized string matchers
have not been addressed.
The goal of our work is to address the second item, with the hope to contribute
to remedying the first one, in the long run.
1.1 This work
We relate the original KMP algorithm [18] to a staged quadratic string matcher
that keeps one character of negative information (essentially Consel and Danvy's
original solution [7]; there are many ways to stage a string matcher [1, 13], and
we show one in Appendix A). Our approach is semantic rather than algorithmic
or intuitive:
1 For example, the dynamic test can be a comparison between a static (i.e., known) character
in the pattern and a dynamic (i.e., unknown) character in the text. In one conditional
branch, the characters match and we statically know what the dynamic character is. In the
other branch, the characters mismatch, and we statically know what the dynamic character
is not. The former is a piece of positive information, and the latter is a piece of negative
information.
. We formalize an imperative language similar to the one in which the KMP
algorithm is traditionally specified, and we formalize the subset of Scheme
in which the staged matcher is specified.
. We then present two trace semantics that account for the sequence of
indices corresponding to the successive comparisons between characters in
the pattern and in the text, and we show that the KMP algorithm and
the staged matcher share the same trace.
. We analyze the binding times of the staged matcher using an o#-the-shelf
binding-time analysis (that of Similix [3, 4]), and we observe that the only
dynamic comparisons are the ones between the static pattern and the dynamic
text. Therefore, specializing this staged string matcher preserves its
trace, given an o#ine program specializer (such as Similix's) that (1) computes
static operations at specialization time and (2) generates a residual
program where dynamic operations do not disappear, are not duplicated,
and are executed in the same order as in the source program. We also
assess the size of residual programs: it is proportional to the size of the
corresponding static patterns. 2
This correspondence and preservation of traces shows that a staged matcher
that keeps one character of negative information corresponds to and specializes
into (the second half of) the KMP algorithm, precisely. It also has two
corollaries:
1. A staged matcher that does not keep track of negative information, as
in S-rensen, Gl-uck, and Jones's work on positive supercompilation [25],
does not give rise to the KMP algorithm. Instead, we observe that such a
staged matcher gives rise to Morris and Pratt's algorithm [5, Chapter 6],
which is also linear but slightly less e#cient.
2. A staged string matcher that keeps track of all the characters of negative
information accumulated during consecutive character mismatches, as in
Futamura's Generalized Partial Computation [9, 11], Gl-uck and Klimov's
supercompiler [12], and Jones, Gomard, and Sestoft's textbook [15, Figure
12.3] does not give rise to the KMP algorithm either. The corresponding
residual programs are slightly more e#cient than the KMP algorithm,
but their size is not linearly proportional to the length of the pattern.
(Indeed, Grobauer and Lawall have shown that the size of these residual
programs is bounded by |pat | - |#|, where pat denotes the pattern and #
denotes the alphabet [13].)
That said,
(a) there is more to linear string matching than the KMP: for example, in their
handbook on exact string matching [5], Charras and Lecroq list over
di#erent algorithms; and
We follow the tradition of counting the size of integers as units. For example, a table of
m integers has size m log n if these integers lie in the interval [0, n - 1], but we consider that
it has size m.
(b) many naive string matchers exist that can be staged to yield a variety of
linear string matchers, e.g., Boyer and Moore's [1].
We observe that over half of the algorithms listed by Charras and Lecroq can
be obtained as specialized versions of staged string matchers. Proving this
observation can be done in the same manner as in the present article for the
KMP. Furthermore, we can obtain new linear string matchers by exploring the
variety of staged string matchers.
1.2

Overview

The rest of this article is organized as follows. In Section 2, we specify an
operational semantics for the imperative language used by Knuth, Morris, and
Pratt, and in Section 3, we specify an operational semantics for a subset of
Scheme [16]. In each of these sections, we specify:
1. the abstract syntax of the language,
2. its expressible values,
3. its evaluation rules,
4. the string matcher,
5. the semantics of the string matcher, and
6. an abstract semantics of the string matcher.
The point of the abstract semantics is to account for the sequence of comparisons
between the pattern and the text in Knuth, Morris, and Pratt's algorithm
(the "imperative matcher") and in our staged string matcher (the "functional
matcher"). Lemmas 1 and 2 show that the abstract semantics faithfully account
for the comparisons between the pattern and the text in the string matchers,
and Theorem 1 establishes their correspondence:
abstract
imperative matcher
(Section 2.6)
Theorem 1
(Section
abstract
functional matcher
(Section 3.6)
concrete
imperative matcher
(Section 2.5)
(Section 2.6)
concrete
functional matcher
(Section 3.5)
(Section 3.6)
In Section 4, we show that the imperative matcher and the functional matcher
give rise to the same sequence of comparisons. In Section 5, we investigate the
result of specializing the functional matcher with respect to a pattern string using
program specialization and then using a simple form of data specialization.
Section 6 concludes.
2 The KMP, imperatively
In this section, we describe the imperative language in which the imperative
string matcher is specified. The language is canonical, with constant and mutable
identifiers and with immutable arrays. We then present the imperative
string matcher and its meaning. Finally, we specify a trace semantics of the
imperative matcher.
2.1 Abstract syntax
A program consists of statements s # Stm, expressions e # Exp, numerals
mutable identifiers x # Mid , array
identifiers a # Aid , and operators opr # Opr .
s ::= x:=e | s;s | if e then s else s fi |
while e do s od | return e
e ::= num | x | c | a[e] | e opr e | e and e
2.2 Expressible values
A value is an integer, a boolean, or a character in an alphabet:
2.3 Rules
In the following rules, e # Exp, v ,
2.3.1 Auxiliary constructs
The language includes numeric operators and a comparison operator over characters

2.3.2 Stores
A store is a total function:
2.3.3 Constants
Constants are defined with a total function:
2.3.4 Arrays
Arrays are defined with a partial function:
where N denotes the set of natural numbers including zero. Indexing arrays
starts at zero, and indexing out of bounds is undefined.
2.3.5 Relations
The (big-step) evaluation relation for expressions reads as
and the (small-step) evaluation relation for statements reads as
If r # Stm, the computation of s is in progress. If r # Unit , the computation
of s completed normally. If r # Z, the computation of s aborted with a return.
We choose a big-step evaluation relation for expressions because we are not
interested in intermediate evaluation steps. We choose a small-step evaluation
relation for statements because we want to monitor the progress of imperative
computations.
2.3.6 Expressions
(var)
(array)
2.3.7 Statements
(assign)
#while e do s od, # I #unit , #
#while e do s od, # I #s;while e do s od, #
A, C #return e, # I #n, #
2.4 The string matcher
The KMP algorithm consists of two parts: the initialization of the next table
and the actual string matching [18].
2.4.1 Initialization of the next table
The first part builds a next table for the pattern satisfying the following definition

table) The next table is an array of indices with the same
length as the pattern: next [j] is the largest i less than j such that pat [j -
no such i exists
then next [j] is -1.
The initialization of the next table is described by the pseudocode in Figure
we assume that pat, txt, lpat, and ltxt are given in an initial
store # in which pat denotes the pattern and lpat its length, and in which txt
denotes the text and ltxt its length.
while j < lpat - 1 do
while t >= 0 and pat[j] != pat[t] do
then next[j] := next[t]
else next[j] := t
od

Figure

1: Initialization of the next table
2.4.2 String matching
The second part traverses the text using the next table as described by the
program in Figure 2, which is written in the imperative language specified in
Sections 2.1, 2.2, and 2.3. In this second part, lpat and ltxt are constant
identifiers, j and k are mutable identifiers, and pat, txt and next are array
identifiers. (pat denotes the pattern and lpat its length, and txt denotes the
text and ltxt its length.)
3 We write 'pseudocode' instead of `code' because in the language of Sections 2.1, 2.2, and
2.3, arrays are immutable. We could easily extend the language to support mutable arrays,
but doing so would clutter the rest of our development with side conditions expressing that
the next table is not updated in the second part of the KMP algorithm. We have therefore
chosen to simplify the language.
while j<lpat and k<ltxt do
while j >= 0 and pat[j] != txt[k] do

Figure

2: The imperative string matcher
In the rest of this article, we only consider the second part of the KMP
algorithm and we refer to it as the imperative matcher.
2.5 Semantics of the imperative matcher
We now consider the meaning of the imperative matcher. We state without
proof that the imperative matcher terminates and accesses the pattern, the
text, and the next table within their bounds.
What we are after is the sequence of indices corresponding to the successive
comparisons between characters in the pattern and in the text. Because the
imperative language is deterministic and the KMP algorithm is a correct string
matcher, this sequence exists and is unique.
imperative comparison for the string matcher
of Section 2.4 is a derivation tree of the form
derivation tree.
Definition 3 (Index) The following function maps an imperative comparison
into the corresponding pair of indices in the pattern and the text:
index I
Definition 4 (Computation) An imperative computation is a derivation of
the imperative matcher
where the premises S 0 , S 1 , ., Sn-1 are other derivation trees, A contains the
pattern, the text, and the next table, C contains the length of the pattern and
the text, s 0 is the imperative matcher, and # 0 is the initial state mapping all
identifiers to zero.
A computation is said to be complete if r # {-1} # N.
In an imperative computation, each premise might contain imperative com-
parisons. We want to build the sequence of indices corresponding to the successive
comparisons between characters in the pattern and in the text. Applying
the index function to each of the imperative comparisons in each premise gives
such indices. We collect them in a sequence of non-empty sets of pairs of indices
as follows.
be the premises of an imperative
computation. Let c i be the set of imperative comparisons in S i , for
n. The imperative trace is the sequence
and where # is the neutral element for concatenation.
In Section 2.6, Lemma 1 shows that each of the premises in Definition 5 contains
at most one imperative comparison. Therefore, for all i, p i is either empty or a
singleton set. The imperative trace is thus a sequence of singleton sets, each of
which corresponds to the successive comparisons of characters in pat and txt .
We choose three program points: one for checking whether we are at the end
of the pattern or at the end of the text, one for comparing a character in the
pattern and a character in the text, and one for reinitializing the index in the
pattern (i.e., for 'shifting the pattern' [18, page 324]) based on the next table.
Definition 6 (Program points) The imperative program points Match I ,
Compare I
and Shift I
are defined as the following sets of configurations:
Match
Compare I
Shift I
where
while j<lpat and k<ltxt do
while j >= 0 and pat[j] != txt[k] do
do
The set of imperative program points is defined as the sum
Compare I
2.6 Abstract semantics
Definition 7 (Abstract states) The set of abstract imperative states is the
sum of the set of abstract imperative final states and the set of abstract imperative
intermediate states:
States
I
States int
I
States fin
I
States int
where match, compare and shift are injection tags.
Definition 8 (Program points and abstract states) We define the correspondence
between abstract imperative states and the union of imperative program
points and final results by the following relation # I # States int
I - (PP I #
(match, j, Match I if
(compare, j, Compare I
(shift, j,
Definition 9 (Abstract matcher) Let pat , txt # and let next be the next
table for pat . Then the abstract imperative matcher is the following total function
I # States int
I - States I :
(match, j,
(compare, j,
(compare, j,
(shift, j,
# (compare, next[j],
(match,
The function last I yields the last element of a non-empty
sequence of abstract states:
last I
I # States I
last I
Definition 11 (Abstract computations) Let pat , txt # and let # I be
the corresponding abstract imperative matcher. Then the set of abstract imperative
computations, AbsComp I # States
I
, is the least set closed under
(1) (match, 0, I and
last I (S) # I p # S - p # AbsComp I .
S is said to be complete i# last I (S) # States fin
I
(Computations are faithful) Abstract imperative computations represent
imperative computations faithfully. In other words:
1. An imperative computation starts with an initial derivation that either does
not contain any program points or (1) does not contain any program points
apart from the final configuration, (2) does not contain any comparisons,
and (3) the final configuration is a program point P # Match I such that
(match, 0, I P .
2. Whenever the last configuration of an imperative computation is an imperative
program point, P , related to an abstract state, S, by # I , there exists
an imperative program point or final result, P # , and an abstract state, S # ,
such that the following holds: (1) there is a derivation from P to P # that
does not contain other program points, (2) S # I S # , (3) S # I P # , and (4)
the derivation contains a comparison, C, if and only if
and then index I
Proof: Part 1 is straightforward to verify. For Part 2 we must divide by cases
as dictated by the abstract matcher. We show just a single case: P # Match I ,
k. The other cases are similar.
The derivation is
#while j<lpat and k<ltxt do . od, # I #unit , #
while j<lpat and k<ltxt do . od;
else return
# I #if j >= lpat then return k-j else return
A, C #if j >= lpat then return k-j else return
I #return k-j, #
(var)
Since (match, j, I k-j, we also have k-j # I n. Furthermore, we observe
that the derivation contains no other program points and no comparisons. #
Since at most one comparison exists for each step in the derivation, the
imperative trace of Definition 5 is a sequence of singleton sets. Moreover, since
the imperative matcher terminates, the abstract matcher does as well.
Definition 12 (Abstract trace) An abstract imperative trace maps a sequence
of abstract states to another sequence of abstract states:
trace I
I # States # I
trace I
The following corollary of Lemma 1 shows that abstract imperative traces
represent imperative traces.
Corollary 1 (Imperative traces are faithful) Let pat , txt # be given,
be the imperative trace for a complete imperative
computation, and let (compare, j #
be the abstract imperative trace for the corresponding complete abstract imperative
computation. Then
In words, the abstract trace faithfully represents the imperative trace.
2.7

Summary

We have formally specified an imperative string matcher implementing the KMP
algorithm, and we have given it a trace semantics accounting for the indices at
which it successively compares characters in the pattern and in the text. In the
next section, we turn to a functional string matcher and we treat it similarly.
3 The KMP, functionally
In this section, we describe the functional language in which the functional
string matcher is specified. The language is a first-order subset of Scheme (tail-
recursive equations). We then present the functional string matcher and its
meaning. Finally, we specify a trace semantics of the functional matcher.
3.1 Abstract syntax
A program consists of serious expressions e # Exp, trivial expressions t # Triv ,
operators opr # Opr , numerals num # Num, value identifiers x # Vid , function
identifiers f # Fid and sequences of value identifiers #x # Vid # .
3.2 Expressible values
A value is an integer, a boolean, a character, or a string:
3.3 Rules
3.3.1 Auxiliary constructs
The language includes numeric operators, a comparison operator over characters
and a string-indexing operator.
c is the i'th character in s.
Indexing strings starts at zero, and indexing out of bounds is undefined.
3.3.2 Environments
Expressions are evaluated in a value environment # Venv and a function
environment
3.3.3 Relations
The (big-step) evaluation relation for trivial expressions reads as
and the (small-step) evaluation relation for serious expressions reads as
#e, #F #r , #
We choose a big-step evaluation relation for trivial expressions because we
are not interested in intermediate evaluation steps. We choose a small-step evaluation
relation for serious expressions because we want to monitor the progress
of computations.
3.3.4 Programs
At the top level, a program is evaluated in an initial function environment # 0
holding the predefined functions and an initial value environment # 0 holding the
predefined values. The initial configuration of a program
is thus #e 0 , # 0 # in the function environment #:
.,
3.3.5 Trivial expressions
(var)
3.3.6 Serious expressions
3.4 The string matcher
We consider the string matcher of Figure 3 (motivated in Appendix A), which
is written in the subset of Scheme specified in Sections 3.1, 3.2, and 3.3. The
initial environment # 0 binds pat and lpat to the pattern and its length, and txt
and ltxt to the text and its length. None of pat, txt, lpat and ltxt are bound
in the program, and therefore they denote initial values throughout.
In the rest of this article, we refer to this string matcher as the functional
matcher.
3.5 Semantics of the functional matcher
We now consider the meaning of the functional matcher. What we are after
is the sequence of indices corresponding to the successive comparisons between
characters in the pattern and in the text.
functional comparison for the string matcher
of Section 3.4 is a derivation tree of the form
where T denotes another derivation tree.
(letrec ([match
(lambda (j
(if (= k ltxt)
(compare j k))))]
[compare
(lambda (j
(if (eq? (string-ref pat
(match
(if (= 0
(match
(rematch
[rematch
(lambda (j k jp kp)
(if (= kp
(if (eq? (string-ref pat jp)
(if (= jp
(match
(rematch
(compare jp k))
(if (eq? (string-ref pat jp)
(rematch
(rematch
(match

Figure

3: The functional matcher
Definition 14 (Index) The following function maps a functional comparison
into the corresponding pair of indices in the pattern and the text:
index F
Definition 15 (Computation) A functional computation is a derivation of
the functional matcher
where the premises are other derivation trees, # is the initial
function environment, e 0 is the functional matcher, and # 0 is a value environment
mapping pat, txt, lpat, and ltxt to the pattern, the text, and their lengths,
respectively, and all other value identifiers to zero.
A computation is said to be complete if r # {-1} # N.
In a functional computation, each premise might contain functional compar-
isons. We want to build the sequence of indices corresponding to the successive
comparisons between characters in the pattern and in the text. Applying the
index function to each of the functional comparisons in each premise gives such
indices. We collect them in a sequence of non-empty sets of pairs of indices as
follows.
Definition be the premises of a functional
computation. Let c i be the set of functional comparisons in E i , for
n. The functional trace is the sequence
otherwise.
In Section 3.6, Lemma 2 shows that each of the premises in Definition 16 contains
at most one functional comparison. Therefore, for all i, p i is either empty or a
singleton set. The functional trace is thus a sequence of singleton sets, each of
which corresponds to the successive comparisons of characters in pat and txt .
We choose three program points: one for checking whether we are at the end
of the pattern or at the end of the text, one for comparing a character in the
pattern and a character in the text, and one for matching the pattern, and a
prefix of a su#x of the pattern. These program points correspond to the bodies
of the match, compare and rematch functions.
Definition 17 (Program points) The functional program points Match F ,
Compare F
and Rematch F are defined as the following sets of configurations:
Match
Compare F
Rematch
where M is the body of the match function, C is the body of the compare function,
and R is the body of the rematch function.
The set of functional program points is defined as the sum
Compare F +Rematch F .
3.6 Abstract semantics
Definition (Abstract states) The set of abstract functional states is the
sum of the set of abstract functional final states and the set of abstract functional
intermediate states:
F
States int
F
States fin
F
States int
F
(rematch -N- N - N -N)
where match, compare and rematch are injection tags.
Definition 19 (Program points and abstract states) We define the correspondence
between abstract functional states and the union of functional program
points and final results by the following relation #F # States int
(match, j,
(compare, j,
(rematch, j, k, jp, kp) #F #e, # Rematch F
Definition 20 (Abstract matcher) Let pat , txt # . Then the abstract
functional matcher is the following total function #F# States int
(match, j,
(compare, j,
(compare, j,
(match,
(rematch, j, k, 0, 1) otherwise
(rematch, j, k, jp, kp) #F
(match,
(compare, jp,
(rematch, j, k, jp
Definition 21 (Last) The function last F yields the last element of a non-empty
sequence of abstract states:
last
last
Definition 22 (Abstract computations) Let pat , txt # and let #F be
the corresponding abstract functional matcher. Then the set of abstract functional
computations, AbsComp F # States
F
, is the least set closed under
(1) (match, 0,
last F (S) #F p # S - p # AbsComp F .
S is said to be complete i# last F (S) # States fin
F
(Computations are faithful) Abstract functional computations represent
functional computations faithfully. In other words:
1. A functional computation starts with an initial derivation that either does
not contain any program points or (1) does not contain any program points
apart from the final configuration, (2) does not contain any comparisons,
and (3) the final configuration is a program point P # Match F such that
(match, 0,
2. Whenever the last configuration of an functional computation is an functional
program point, P , related to an abstract state, S, by #F , there exists
a functional program point or final result, P # , and an abstract state, S # ,
such that the following holds: (1) there is a derivation from P to P # that
does not contain other program points, (2) S #F S # , (3) S #F P # , and (4)
the derivation contains a comparison, C, if and only if
and then indexF
Proof: Part 1 is straightforward to verify. For Part 2 we must divide by cases
as dictated by the abstract matcher. We show just a single case: P # Match F ,
|txt|. The other cases are similar.
The derivation is
(var)
(var)
#(compare
(app)
where C denotes the body of the compare function, as in Definition 17.
Since (match, j,
k, we also have that (compare, j, k) corresponds to the final configuration in
the derivation. Furthermore, we observe that the derivation contains no other
program points and no comparisons. #
Since at most one comparison exists for each step in the derivation, the
functional trace of Definition 16 is a sequence of singleton sets. Moreover, if one
of the matchers terminates, the other does as well.
Definition 23 (Abstract trace) An abstract functional trace maps a sequence
of abstract states to another sequence of abstract states:
trace
trace
The following corollary of Lemma 2 shows that abstract functional traces
traces.
Corollary 2 (Functional traces are faithful) Let pat , txt # be given,
be the functional trace for a complete functional
computation, and let (compare, j #
be the abstract trace for the corresponding complete abstract functional compu-
tation. Then
In words, the abstract trace faithfully represents the functional trace.
Lemma 3 (Invariants) Let pat , txt # and AbsComp F
be the corresponding
set of abstract functional computations. Then for all s 1 -s
the following conditions, whose conclusions we call invariants, are satisfied:
. If s
. If s
. If s
Proof: Let pat , txt # be given, and let S # AbsComp F
. The proof is by
structural induction on S. The base case is to show that the invariants hold
initially, and the induction cases are to show that the invariants are preserved
at match, compare and rematch.
Initialization
By definition of AbsComp F
, the initial abstract functional state in the computation
S is (match, 0, 0). As lengths of strings, |pat| and |txt| are non-negative,
and by insertion we obtain 0
and (m2) thus hold trivially in the initial abstract functional state.
Preservation at match
Let us assume that Invariants (m1) and (m2) hold at an abstract functional
state (match, j, k). We consider the three possible cases:
j. The next abstract state in
the abstract functional computation is therefore k-j and all the invariants
are preserved.
. -1. The next
abstract state is therefore -1 and all the invariants are preserved.
.
The next abstract state is therefore (compare, k). By the case
assumption Invariants
(c1) and (c2).
The invariants are thus preserved at match.
Preservation at compare
Let us assume that Invariants (c1) and (c2) hold at an abstract functional state
(compare, j, k). We consider the three possible cases:
. 1). The
next abstract state in the abstract functional computation is (match,
1). Since j, k, |pat| and |txt| are integers, j < |pat| #
hold. Since the premises are true by Invariants (c1) and (c2), Invariants
(m1) and (m2) hold.
. txt[k] #= pat[j] # 0: By definition, (compare, j, 1).
The next abstract state is (match, 1). With an argument
identical to the above we obtain Invariant (m2). By inserting the value
in Invariant (m1), as done in the initalization case, we also obtain
Invariant (m1).
. txt[k] #= pat[j]#j > 0: By definition, (compare, j,
The next abstract state is (rematch,
Due to (c1) and j > 0, (r1) holds, and (c2) is identical to
(r2).
thus (r3) holds.
which by convention
denotes the empty string. Similarly, pat[kp # - jp #
denotes the empty string, and Invariant (r4)
holds.
Finally, (r5) holds trivially, because the interval [1, kp # - jp # -
[1, 0] denotes the empty set, by convention.
The invariants are thus preserved at compare.
Preservation at rematch
Let us assume that Invariants (r1), (r2), (r3), (r4), and (r5) hold at an abstract
functional state (rematch, j, k, jp, kp). We consider the five possible cases:
. 0: By definition, (rematch, j, k, jp, kp) #F
(match, 1). The next abstract state in the abstract functional computation
is (match, 1). By Invariant (r2), we obtain
as shown
above.
. 0: By definition, (rematch, j, k, jp, kp) #F
1). The next abstract state is (rematch,
Invariants (r1) and (r2) hold for j and k, the trivial
updates, immediately give Invariants (r1) and
(r2).
kp # . And since j
Invariant (r3) is satisfied.
first look at pat[0] - pat[jp # -1], which is the empty string since
1] is the empty string, and therefore Invariant (r4) holds.
From the invariant we know that the body of (r5) holds for every
k in the interval [1, kp # - jp # - 2], since j
We then only need to show that -(pat[0] - pat[j # - k -
more specifically
1. This is easily seen
since which under the case
assumption give pat[j -
Invariant (r5) holds.
.
k). The next abstract state is therefore (compare,
(r1), (r3), and the case assumption, we have
holds. Since k
. kp <
1). The next abstract state is therefore (rematch,
which give us (r3).
we have pat[0] - pat[jp #
and we only need to show pat[jp # - This is true by
the case assumption and thus (r4) holds.
and since the interval for k is unchanged, because
holds by
assumption.
. kp < j # pat[jp] #= pat[kp]: By definition, (rematch, j, k, jp, kp) #F
(rematch, j, k, 0, kp -jp 1). The next abstract state is therefore (rematch,
By the trivial update of j and k, (r1) and (r2), as shown
above, still hold.
clearly have jp # 0, and the assumption kp > jp
gives us kp . Finally, since kp < j # kp+1 # j,
we have kp thus Invariant (r3) holds.
Again, as shown in the second case, the strings are empty by the
condition thus Invariant (r4) holds.
Similarly to the second case, we only need to show -(pat[0] - pat[j # -
more specifically
holds for
We consider the jpth and (k jp)th entries, which
are the characters pat[jp] and pat[kp], respectively, since k
kp. By the case
assumption the entries are distinct, and we conclude by showing
that the first string contains a jpth entry. The case assumption
us just that; we have 0 # jp and
thus
Invariant (r5) holds. #
The key connection between the abstract functional matcher and the abstract
imperative matcher is stated in the following remark. The remark shows
how to interpret Invariant (r5) in terms of the next table.
Remark 1 We notice that for any j and 0 # a # b, if #k # [a, b].-(pat[0] - pat[j-
then by Definition 1 next [j]
cannot occur in the interval [j - b, j - a].
Indeed, if for some k and some j, (pat[0] - pat[j - k -
and pat[j - k] #= pat[j]), then j - k is a candidate for next[j]. Therefore the
negation of the condition gives us that j - k is not a candidate for next[j].
3.7

Summary

We have formally specified a functional string matcher, and we have given it
a trace semantics accounting for the indices at which it successively compares
characters in the pattern and in the text. In the next section, we show that
for any given pattern and text, the traces of the imperative matcher and of the
functional matcher coincide.
Extensional correspondence between imperative
and functional matchers
Definition 24 (Correspondence) We define the correspondence between imperative
and functional states with the relation # States I - States F :
(match, j,
(compare, j,
(shift, j,
We define # States # I -States # F
such that for any sequences
I
F
for all
hold for empty sequences.
Synchronization is a relation sync # States
I
-States
F
defined as
trace I (S) # trace F (S # last I (S) # last F (S # )
Theorem 1 (Abstract equivalence) For any given pattern and text, there
is a unique complete abstract imperative computation S and a unique complete
abstract functional computation S # , and these two abstract computations are
synchronized, i.e., sync(S, S # ) holds.
Proof: Let pat , txt # be given, and let S # AbsComp I
. The proof is by structural induction on the abstract computation
. The base case is to prove that the abstract computations start in the
same abstract state, and are therefore initially synchronized. The induction
cases are to prove that synchronization is always preserved.
Initialization
By definition of AbsComp I
and AbsComp F
, both abstract computations S and
start in the abstract state (match, 0, 0). Since sync((match, 0, 0), (match, 0, 0))
holds, the abstract computations are initially synchronized.
Preservation from match
We are under the assumption that initial subsequences I of S and I # of S #
are synchronized, i.e., sync(I , I # ) holds, last I last F
(match, j, k). Three cases occur, that are exhaustive by the invariants of Lemma 3:
j. Similarly, by
definition, (match, j, j. By assumption, sync(I , I # ) holds, and
therefore and thus the complete
abstract computations are synchronized.
Similarly, by
definition, (match, j, I -1. As above, synchronization is preserved
since the computations end with the same integer.
. j < |pat| # k < |txt|: By definition, (match, j,
larly, by definition, (match, j,
by assumption, sync(I - (compare, j, k), I # - (compare, j, k)) also holds.
Synchronization is thus preserved in all cases.
Preservation from compare
We are under the assumption that initial subsequences I of S and I # of S # are
synchronized, i.e., sync(I , I # ) holds, last I last F
(compare, j, k). Three cases occur, that are exhaustive by the invariants of
Lemma 3:
. txt[k] #= pat[j] # 0: By definition, (compare, j, 1).
Similarly, by definition, (compare, j,
since by definition. Since sync(I , I # ) by assumption, and the
shift states are not included in the abstract trace, sync(I - (shift, j,
(match,
. txt[k] #= pat[j]#j > 0: By definition, (compare, j,
Similarly, by definition, (compare, j,
holds by assumption, and (shift, j,
. 1).
Similarly, by definition, (compare, j,
sync(I , I # ) holds by assumption, sync(I - (match, j +1, k+1), I # - (match,
Again, synchronization is preserved in all cases.
Preservation from rematch and shift
We are under the assumption that initial subsequences I of S and I # of S #
are synchronized, i.e., sync(I , I # ) holds, last I last F
(rematch, j, k, jp, kp). Since by Definition 24, (shift, j,
for all jp and kp, we only have to consider the cases where the abstract functional
computation goes to a abstract state of a form di#erent from (rematch, j, k, jp, kp).
Doing so is sound because the recursive calls in the rematch function never diverge
(the lexicographic ordering on #m - (kp - jp), m - jp# is a termination
relation for rematch until its call to match or compare). Two cases occur:
. 0: By definition, (rematch, j, k, jp, kp) #F
(match, 1). We know that Invariant (r5) holds for k in the interval
which by Remark 1 implies that next [j] /
From the
case assumption, we know that
next [j] # [-1, j - 1] we then have next Therefore, by definition
of the abstract imperative matcher, (shift, j,
sync(I , I # ) holds by assumption, sync(I -(match, 0, k+1), I # -(match, 0, k+1))
also holds.
. Due to Invariants (r1) and (r3), we have jp <
|pat|. By definition, (rematch, j, k, jp, kp) #F (compare, jp, k). We
know that the body of Invariant (r5) holds for k in the interval [1, j-jp-1],
which by Remark 1 gives us next [j] /
# [jp+1, j-1]. From (r4) we know that
and by the case assumption
we have pat[jp] #= pat[j]. Therefore, jp is a candidate for next [j]. Since
next [j] /
since next [j] is the largest value less than j
satisfying the requirements, we have next Invariant (r3) we
know that jp # 0, so by definition of the abstract imperative matcher,
(shift, j, I (compare, jp, k). Since sync(I , I # ) holds by assumption,
sync(I - (compare, jp, k), I # - (compare, jp, k)) also holds.
Since the KMP algorithm terminates, and since the abstract matchers are total
functions, complete abstract computations exist, and they are unique. #
We are now in position to state our main result, as captured by the diagram
from Section 1.2.
abstract
imperative matcher
(Section 2.6)
Theorem 1
(Section
abstract
functional matcher
(Section 3.6)
concrete
imperative matcher
(Section 2.5)
(Section 2.6)
concrete
functional matcher
(Section 3.5)
(Section 3.6)
Corollary 3 (Equivalence) Let pat , txt # be given. Then there is (1)
a corresponding complete imperative computation, C, with final configuration
#n, #, for some number, n, (2) a corresponding complete functional computa-
tion, C # , with final configuration #n #, for some number, n # , (3)
(4) the traces of C and C # are equal.
Proof: By Theorem 1, the abstract functional matcher terminates, and by
Corollary 2 so does the functional matcher. A complete functional computation
therefore exists. By Lemma 1 and Lemma 2 and their corollaries, the abstract
computations represent the computations such that the trace and the result are
represented faithfully. Finally, by Theorem 1, the abstract computations are
synchronized, which means that the abstract traces and the results are equal.
To summarize, we have shown that for any given pattern and text, the traces
of the imperative matcher and of the functional matcher coincide. In that sense,
the two matchers "do the same", albeit with a di#erent time complexity. In the
next section, we show how to eliminate the extra complexity of the functional
matcher, using partial evaluation.
5 Intensional correspondence between imperative
and functional matchers
We now turn to specializing the functional string matcher with respect to given
patterns. First we use partial evaluation (i.e., program specialization), and next
we consider a simple form of data specialization. We first show that the size
of the specialized programs is linear in the size of the pattern, and that the
specialized programs run in time linear in the size of the text. We next show
that the specialized data coincides with the next table of the KMP.
This section is more informal and makes a somewhat liberal use of partial-
evaluation terminology [21].
(define (main pat s txt d )
(let ([lpat s (string-length pat)] [ltxt d (string-length txt)])
(letrec ([match
(lambda (j s k d )
(compare j k))))]
[compare
(lambda (j s k d )
(match
(if (= 0
(match
(rematch
[rematch
(lambda (j s k d jp s kp s )
(if (= kp
(if (eq? (string-ref pat jp)
(if (= jp
(match
(rematch
(compare jp k))
(if (eq? (string-ref pat jp)
(rematch
(rematch
(match

Figure

4: The binding-time annotated functional matcher
5.1 Program specialization

Figure

4 displays a binding-time annotated version of the complete functional
matcher as derived in Appendix A. Formal parameters are tagged with "s"
(for "static") or "d" (for "dynamic") depending on whether they only denote
values that depend on data available at partial-evaluation time or whether they
denote values that may depend on data available at run time. In addition,
dynamic conditional expressions, dynamic tests, and dynamic additions and
subtractions are boxed. All the other parts in the source program are static
and will be evaluated at partial-evaluation time. All the dynamic parts will be
reconstructed, giving rise to the residual program.
A partial evaluator such as Similix [3, 4] is designed to preserve dynamic computations
and their order. In the present case, the dynamic tests are among the
dynamic computations. They are guaranteed to occur in specialized programs
in the same order as in the source program. Therefore, by construction, Similix
generates programs that traverse the text in the same order as the functional
matcher and thus the KMP algorithm.
For example, we have specialized the functional matcher with respect to
the pattern "abac" (without post-unfolding). The resulting residual program is
displayed in Figure 5, after lambda-dropping [8] and renaming (the character
following the "|", in the subscripts, is the next character in the pattern to be
matched against the text-an intuitive notation suggested by Grobauer and
Lawall [13]). The specialized string matcher traverses the text linearly and
compares characters in the text and literal characters from the pattern. In their
article [18, page 330], Knuth, Morris and Pratt display a similar program where
the next table has been "compiled" into the control flow. We come back to this
point at the end of Section 5.2.
In their revisitation of partial evaluation of pattern matching in strings [13],
Grobauer and Lawall analyzed the size and complexity of the residual code
produced by Similix, measured in terms of the number of residual tests. They
showed that the size of a residual program is linear in the length of the pattern,
and that the time complexity is linear in the length of the text. In the same
manner, we can show that Similix yields a residual program that is linear in the
length of the pattern, and whose time complexity is linear in the length of the
text.
Similix is a polyvariant program-point specializer that builds mutually recursive
specialized versions of source program points (by default: conditional
expressions with dynamic tests). Each source program point is specialized with
respect to a set of static values. The corresponding residual program point is
indexed with this set. If a source program point is met again with the same set
of static values, a residual call to the corresponding residual program point is
generated.
Proposition 1 Specializing the functional matcher of Figure 4 with respect to a
pattern yields a residual program whose size is linear in the length of the pattern.
Proof (informal): The only functions for which residual code is generated
are main, match and compare. The first one, main, is the goal function, but it
contains no memoization points, so only one residual main function is generated.
There is exactly one memoization point-a dynamic conditional expression-
in each of the functions match and compare. The only static data available at
the two memoization points are bound to j, pat, and lpat. The only piece of
static data that varies is the value of j, i.e., j, and since 0 # j < |pat| at the
memoization points (because of the invariants of Lemma 3 in Section 4, and the
fact that the memoization point in match is only reached if j #= |pat|), at most
|pat| variants of the two memoization points can be generated. The number of
(define (main-abac txt)
(let ([ltxt (string-length txt)])
(define (match |abac
(define (compare |abac
(if (eq? #\a (string-ref txt k))
(match a|bac (+ k 1))
(match |abac (+ k 1))))
(define (match a|bac
(define (compare a|bac
(if (eq? #\b (string-ref txt k))
(match ab|ac (+ k 1))
(compare |abac k)))
(define (match ab|ac
(define (compare ab|ac
(if (eq? #\a (string-ref txt k))
(match aba|c (+ k 1))
(match |abac (+ k 1))))
(define (match aba|c
(define (compare aba|c
(if (eq? #\c (string-ref txt k))
(compare a|bac k)))
(match |abac 0)))
. For all txt, evaluating (main-abac txt) yields the same result as evaluating
(main "abac" txt).
. For all k, evaluating (match |abac k) in the scope of ltxt yields the same
result as evaluating (match 0 k) in the scope of lpat and ltxt, where
lpat denotes the length of pat and ltxt denotes the length of txt.
. For all k, evaluating (match a|bac k) in the scope of ltxt yields the same
result as evaluating (match 1 in the scope of lpat and ltxt.
. For all k, evaluating (match ab|ac k) in the scope of ltxt yields the same
result as evaluating (match 2 k) in the scope of lpat and ltxt.
. For all k, evaluating (match aba|c k) in the scope of ltxt yields the same
result as evaluating (match 3 k) in the scope of lpat and ltxt.

Figure

5: Result of specializing the functional matcher wrt. "abac"
residual functions is therefore linear in the size of the pattern. In addition, the
size of each function is bounded by a small constant, as can be seen if one writes
the BNF of residual programs [20]. #
Proposition 2 Specializing the functional matcher of Figure 4 with respect to
a pattern yields a residual program whose time complexity is linear in the length
of the text.
Proof (informal): As proven by Knuth, Morris and Pratt, the KMP algorithm
performs a number of comparisons between characters in the pattern
and in the text, that is linear in the length of the text [18]. Corollary 3 shows
that the functional matcher performs the exact same sequence of comparisons
between characters in the pattern and in the text as the KMP algorithm. All
comparisons are performed in the compare function, and exactly one comparison
is performed at each call to compare. The number of calls to compare is therefore
linear in the length of the text, and since the match function either terminates
or calls compare, the number of calls to match is bounded by the number of calls
to compare. By Proposition 1, residual code is only generated for the functions
main, compare, and match. The time complexity of each of the functions main,
compare, and match is easily seen to be bounded by a small constant. Since main
is only called once and the number of calls to compare and match is linear in the
length of the text, the time complexity of the residual program is linear in the
length of the text. #
5.2 Data specialization
In Section 3.6, Remark 1 connects the rematch function in the functional matcher
and the next table of the KMP algorithm. In this section, we revisit this connection
and show how to actually derive the KMP algorithm with a next table from
the functional matcher using a simple form of data specialization [2, 6, 17, 19].
To this end, we first restate the functional matcher.
In the functional matcher, all functions are tail recursive, i.e., they iteratively
call themselves or each other. In particular, rematch completes either by calling
match or by calling compare. The two actual parameters to match are 0, a literal,
and an increment over k, which is available in the scope of match. The two
actual parameters to compare are jp, which has been computed in the course of
rematch, and k, which is available in the scope of compare.
To make it possible to tabulate the rematch function, we modify the functional
matcher so that it is no longer tail recursive. Instead of having rematch
call match or compare, tail recursively, we make it return a value on which to call
match or compare. We set this value to be that of jp (a natural number) or -1.
Correspondingly, instead of having compare call rematch tail recursively, we make
it dispatch on the result of rematch to call match or compare, tail recursively. The
result is displayed in Figure 6.
In the proof of Theorem 1, we show that when rematch terminates by calling
compare, jp is equal to next [j] in the KMP algorithm. We also show that when
(define (main pat txt)
(let ([lpat (string-length pat)] [ltxt (string-length txt)])
(letrec ([match
(lambda (j
(if (= k ltxt)
(compare j k))))]
[compare
(lambda (j
(if (eq? (string-ref pat
(match
(if (= 0
(match
(let ([next (rematch j 0 1)])
(if (= next -1)
(match
(compare next k))))))]
[rematch
(lambda (j jp kp)
(if (= kp
(if (eq? (string-ref pat jp)
(if (= jp
(rematch
(if (eq? (string-ref pat jp)
(rematch
(rematch
(match

Figure

Variation on the functional matcher
match is called from rematch, the value next [j] in the KMP algorithm is -1. We
only call rematch from compare, and only with
Therefore calling the new rematch function is equivalent to a lookup in the next
table in the KMP algorithm. In particular, tabulating the |pat| input values of
rematch corresponding to all j between 0 and |pat| - 1 yields the next table as
used in the KMP algorithm.
This simple data specialization yields a string matcher that traverses the
text linearly, matching it against the pattern, and looking up the next index
into the pattern in the next table in case of mismatch. In other words, data
specialization of the functional matcher yields the KMP algorithm.
In particular, specializing the string matcher of Figure 6 (or its tabulated
version) with respect to a pattern would compile the corresponding next table
into the control flow of the residual program. The result would coincide with
the compiled code in Knuth, Morris and Pratt's article [18, page 330].
6 Conclusion and issues
We have presented the first formal proof that partial evaluation can precisely
yield the KMP, both extensionally (trace semantics, synchronization) and intensionally
(size of specialized programs, relation to the next table, actual derivation
of the KMP algorithm). We have shown that the key to obtaining the
KMP out of a naive, quadratic string matcher is not only to keep backtracking
under static control, but also to maintain exactly one character of negative in-
formation, as in Consel and Danvy's original solution. Together with Grobauer
and Lawall's complexity proofs about the size and time complexity of residual
programs, the buildup of Corollary 3 paves the way to relating the e#ect of
staged string matchers with independently known string matchers, e.g., Boyer
and Moore's [1].
Our work has led us to consider a family of KMP algorithms in relation with
the following family of staged string matchers:
. A staged string matcher that does not keep track of negative information
gives rise not to Knuth, Morris, and Pratt's next table, but to their f
function [18, page 327], i.e., to Morris and Pratt's algorithm [5, Chapter 6].
Tabulating this function yields an array of the same size as the pattern.
. A staged string matcher that keeps track of one character of negative
information corresponds to Knuth, Morris, and Pratt's algorithm and next
table.
. A staged string matcher that keeps track of a limited number of characters
of negative information gives rise to a KMP-like algorithm. The
corresponding residual programs are more e#cient, but they are also bigger

. A staged string matcher that keeps track of all the characters of negative
information also gives rise to a KMP-like algorithm. The corresponding
residual programs are even more e#cient, but they are also even bigger.
Grobauer and Lawall have shown that the size of these residual programs
is bounded by |pat | - |#|, where |#| is the size of the alphabet [13].
It is however our conjecture that for string matchers that keep track of
two or more characters of negative information, a tighter upper bound on
the size is twice the length of the pattern, i.e., 2|pat |. This conjecture
holds for short patterns.
Let us conclude on two points: obtaining e#cient string matchers by partial
evaluation of a naive string matcher and obtaining them e#ciently.
The essence of obtaining e#cient string matchers by partial evaluation of
a naive string matcher is to ensure that backtracking in the naive matcher is
static. One can then either stage the naive matcher and use a simple partial
evaluator, or keep the naive matcher unstaged and use a sophisticated partial
evaluator. What matters is that backtracking is carried out at specialization
time and that dynamic computations are preserved in specialized programs.
The size of residual programs provides a lower bound to the time complexity
of specialization. For example, looking at the KMP, the size of a residual
program is proportional to the size of the pattern if only positive information
is kept. At best, a general-purpose partial evaluator could thus proceed in time
linear in |pat |, i.e., O(|pat |), as in the first pass of the KMP algorithm. How-
ever, evaluating the static parts of the source program at specialization time,
as driven by the static control flow of the source program, does not seem like
an optimal strategy, even discounting the complexity of binding-time analysis.
For example, the data specialization in Section 5.2 works in time quadratic in
|pat |, i.e., O(|pat | 2 ), to construct the next table. On the other hand, such an
e#cient treatment could be one of the bullets in a partial evaluator's gun [22,
Section 11], i.e., a treatment that is not generally applicable but has a dramatic
e#ect occasionally. For example, proving the conjecture above could lead to
such a bullet.

Acknowledgments

We are grateful to Torben Amtoft, Julia Lawall, Karoline
Malmkj-r, Jan Midtgaard, Mikkel Nygaard, and the anonymous reviewers for
a variety of comments. Special thanks to Andrzej Filinski for further comments
that led us to reshape this article.
This work is supported by the ESPRIT Working Group APPSEM (http://
www.md.chalmers.se/Cs/Research/Semantics/APPSEM/).
A Staging a quadratic string matcher

Figure

7 displays a naive, quadratic string matcher that successively checks
whether the pattern pat is a prefix of one of the successive su#xes of the text
txt. The main function initializes the indices j and k with which to access pat
and txt. The match function checks whether the matching is finished (either
with a success or with a failure), or whether one more comparison is needed.
The compare function carries out this comparison. Either it continues to match
the rest of pat with the rest of the current su#x of txt or it starts to match pat
and the next su#x of txt.

Figure

8 displays a staged version of the quadratic string matcher. Instead of
matching pat and the next su#x of txt, this version uses a rematch function and
a recompare function to first match pat and a prefix of a su#x of pat, which we
know to be equal to the corresponding segment in txt. Eventually, the rematch
function resumes matching the rest of the pattern and the rest of txt. As a
result, the staged string matcher does not backtrack on txt.
In partial-evaluation jargon, the string matcher of Figure 8 uses positive information
about the text (see Footnote 1 page 4). A piece of negative information
is also available, namely the latest character having provoked a mismatch.

Figure

9 displays a staged version of the quadratic string matcher that exploits
this negative information. Rather than blindly resuming the compare function,
the rematch function first checks whether the character having caused the latest
mismatch could cause a new mismatch, thereby avoiding one access to the text.
To simplify the formal development, we inline recompare in rematch and
lambda-lift rematch to the same lexical level as match and compare [8, 14]. The
resulting string matcher is displayed in Figure 10 and in Section 3.4.
There are of course many ways to stage a string matcher. The one we have
chosen is easy to derive and easy to reason about.



--R

The abstraction and instantiation of string-matching programs
Mixed computation and translation: Linearisation and decomposition of compilers.
Similix 5.1 manual.
Automatic autoprojection of recursive equations with global variables and abstract data types.
Exact string matching algorithms.
Sandrine Chiroko
Partial evaluation of pattern matching in strings.





Transforming recursive equations into programs with block structure.
Program transformation system based on generalized partial computation.
Generalized partial computation.


Essence of generalized partial computation.
Occam's razor in metacomputation: the notion of a perfect process tree.
Partial evaluation of pattern matching in strings
Lambda lifting: Transforming programs to recursive equations.
Partial Evaluation and Automatic Program Generation.
Revised 5 report on the algorithmic language Scheme.
Data specialization.
Fast pattern matching in strings.
Program and data specialization: Principles
Abstract Interpretation of Partial-Evaluation Algo- rithms

A transformation-based optimiser for Haskell
Christian Queinnec and Jean-Marie Ge#roy
Partial evaluation of pattern matching in constraint logic programming languages.
A positive su- percompiler
--TR
Lambda lifting: transforming programs to recursive equations
Partial evaluation of pattern matching in strings
Partial evaluation of pattern matching in constraint logic programming languages
Automatic autoprojection of recursive equations with global variable and abstract data types
Essence of generalized partial computation
Partial evaluation and automatic program generation
Abstract interpretation of partial evaluation algorithms
Data specialization
A transformation-based optimiser for Haskell
Lambda-dropping
Glossary for Partial Evaluation and Related Topics
Program transformation system based on generalized partial computation
Revised Report on the Algorithmic Language Scheme
Combining Program and Data Specialization
Occam''s Razor in Metacompuation
Partial evaluation of pattern matching in strings, revisited

--CTR
Mads Sig Ager , Olivier Danvy , Henning Korsholm Rohde, Fast partial evaluation of pattern matching in strings, ACM SIGPLAN Notices, v.38 n.10, p.3-9, October
Yoshihiko Futamura , Zenjiro Konishi , Robert Glck, Automatic generation of efficient string matching algorithms by generalized partial computation, Proceedings of the ASIAN symposium on Partial evaluation and semantics-based program manipulation, p.1-8, September 12-14, 2002, Aizu, Japan
Olivier Danvy , Henning Korsholm Rohde, On obtaining the Boyer-Moore string-matching algorithm by partial evaluation, Information Processing Letters, v.99 n.4, p.158-162, 31 August 2006
Mads Sig Ager , Olivier Danvy , Henning Korsholm Rohde, Fast partial evaluation of pattern matching in strings, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.696-714, July 2006
Germn Vidal, Cost-Augmented Partial Evaluation of Functional Logic Programs, Higher-Order and Symbolic Computation, v.17 n.1-2, p.7-46, March-June 2004
trace semantics;data specialization;program specialization;Knuth-Morris-Pratt string matching