BRICS RS-02-32 Ager et al.: On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation BRICS

Basic Research in Computer Science

On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation

Mads Sig Ager Olivier Danvy Henning Korsholm Rohde BRICS Report Series RS-02-32 ISSN 0909-0878 July 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Mads Sig Ager & Olivier Danvy &

Henning Korsholm Rohde. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/32/

On Obtaining

Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation ^{∗}

Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde

BRICS ^{†} Department of Computer Science University of Aarhus ^{‡}

July 2002

Abstract

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, à 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.

∗Extended version of an article to appear in the proceedings of the first ACM SIG-PLAN ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (ASIA-PEPM’02), September 12-14, 2002, Aizu, Japan.

† Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

‡ Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark E-mail: {mads,danvy,hense}@brics.dk

Contents

1 Introduction 4 1.1 This work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2 The KMP, imperatively 7 2.1 Abstract syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Expressible values . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3 Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.3.1 Auxiliary constructs . . . . . . . . . . . . . . . . . . . . . 8 2.3.2 Stores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.3 Constants . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.4 Arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.5 Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.6 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3.7 Statements . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.4 The string matcher . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.4.1 Initialization of the next table . . . . . . . . . . . . . . . . 10 2.4.2 String matching . . . . . . . . . . . . . . . . . . . . . . . 10

2.5 Semantics of the imperative matcher . . . . . . . . . . . . . . . . 11 2.6 Abstract semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3 The KMP, functionally 16 3.1 Abstract syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.2 Expressible values . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.3 Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3.3.1 Auxiliary constructs . . . . . . . . . . . . . . . . . . . . . 16 3.3.2 Environments . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3.3 Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3.4 Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3.5 Trivial expressions . . . . . . . . . . . . . . . . . . . . . . 18 3.3.6 Serious expressions . . . . . . . . . . . . . . . . . . . . . . 18

3.4 The string matcher . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.5 Semantics of the functional matcher . . . . . . . . . . . . . . . . 18 3.6 Abstract semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

4 Extensional correspondence between imperative and functional matchers 28

5 Intensional correspondence between imperative and functional matchers 31 5.1 Program specialization . . . . . . . . . . . . . . . . . . . . . . . . 32 5.2 Data specialization . . . . . . . . . . . . . . . . . . . . . . . . . . 35 6 Conclusion and issues 37

A Staging a quadratic string matcher 38

List of Figures

1 Initialization of the next table . . . . . . . . . . . . . . . . . . . . 10 2 The imperative string matcher . . . . . . . . . . . . . . . . . . . 11 3 The functional matcher . . . . . . . . . . . . . . . . . . . . . . . 19 4 The binding-time annotated functional matcher . . . . . . . . . . 32 5 Result of specializing the functional matcher wrt. "abac" . . . . . 34 6 Variation on the functional matcher . . . . . . . . . . . . . . . . 36 7 The naive, quadratic functional matcher . . . . . . . . . . . . . . 40 8 The functional matcher with positive information . . . . . . . . . 40 9 The functional matcher with positive information and one char-

acter of negative information . . . . . . . . . . . . . . . . . . . . 41 10 The functional matcher with positive information and one char-

acter of negative information (final version) . . . . . . . . . . . . 42

1 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, txt⟩ = res
run PE ⟨match, ⟨pat, ⟩⟩ = match_{⟨pat, ⟩}
run match_{⟨pat, ⟩} ⟨ , txt⟩ = 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 off-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 offline 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ück, 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 efficient.

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ück 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 efficient 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 30 different algorithms; and (b) many naive string matchers exist that can be staged to yield a variety of

2We 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.

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 4)

[figure]

[figure]

abstract functional matcher (Section 3.6)

[figure]

[figure]

concrete imperative matcher (Section 2.5)

Lemma 1 (Section 2.6)

[figure]

concrete functional matcher (Section 3.5)

Lemma 2 (Section 3.6)

[figure]

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 num ∈ Num, constant identifiers c ∈ Cid, 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
opr ::= + | - | >= | < | !=

2.2 Expressible values

A value is an integer, a boolean, or a character in an alphabet:

Val = ℤ + 𝔹 + Σ

2.3 Rules

In the following rules, e ∈ Exp, v, v_{1}, v_{2} ∈ Val, s, s_{1}, s_{2} ∈ Stm, c ∈ Cid, x ∈ Mid, num ∈ Num, opr ∈ Opr, n ∈ ℤ, and Unit = {unit}.

2.3.1 Auxiliary constructs

The language includes numeric operators and a comparison operator over characters:

number(num) = n, if num denotes n
operate(+, n_{1}, n_{2}) = n_{1} + n_{2}
operate(-, n_{1}, n_{2}) = n_{1} − n_{2}
operate(>=, n_{1}, n_{2}) = n_{1} ≥ n_{2}
operate(<, n_{1}, n_{2}) = n_{1} < n_{2}
operate(!=, c_{1}, c_{2}) = c_{1} ≠ c_{2}

2.3.2 Stores

A store is a total function:

σ : Mid → ℤ

2.3.3 Constants

Constants are defined with a total function:

C : Cid → ℤ

2.3.4 Arrays

Arrays are defined with a partial function:

A : Aid × ℕ → ℤ ∪ Σ

where ℕ 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

A, C, σ ⊢ e →_{I} v

and the (small-step) evaluation relation for statements reads as

A, C ⊢ ⟨s, σ⟩ →_{I} ⟨r, σ′⟩

where e ∈ Exp, v ∈ Val, s ∈ Stm, and r ∈ Stm + Unit + ℤ. If r ∈ Stm, the computation of s is in progress. If r ∈ Unit, the computation of s completed normally. If r ∈ ℤ, 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

\frac{n = number(num)}{A, C, σ ⊢ num →_{I} n}(num)

\frac{n = σ(x)}{A, C, σ ⊢ x →_{I} n}(var)

\frac{n = C(c)}{A, C, σ ⊢ c →_{I} n}(const)

\frac{A, C, σ ⊢ e →_{I} n v = A(a, n)}{A, C, σ ⊢ a[e] →_{I} v}(array)

\frac{A, C, σ ⊢ e_{1} →_{I} v_{1} A, C, σ ⊢ e_{2} →_{I} v_{2} v = operate(opr, v_{1}, v_{2})}{A, C, σ ⊢ e_{1} opr e_{2} →_{I} v} (opr)

\frac{A, C, σ ⊢ e_{1} →_{I} false}{A, C, σ ⊢ e_{1} and e_{2} →_{I} false} (and_{1})

\frac{A, C, σ ⊢ e_{1} →_{I} true A, C, σ ⊢ e_{2} →_{I} b}{A, C, σ ⊢ e_{1} and e_{2} →_{I} b}(and_{2})

2.3.7 Statements

\frac{A, C, σ ⊢ e →_{I} n σ′ = σ[x ↦ n]}{A, C ⊢ ⟨x:=e, σ⟩ →_{I} ⟨unit, σ′⟩}(assign)

\frac{A, C ⊢ ⟨s_{1}, σ⟩ →_{I} ⟨s′_{1}, σ′⟩}{A, C ⊢ ⟨s_{1};s_{2}, σ⟩ →_{I} ⟨s′_{1};s_{2}, σ′⟩}(seq_{1})

\frac{A, C ⊢ ⟨s_{1}, σ⟩ →_{I} ⟨unit, σ′⟩}{A, C ⊢ ⟨s_{1};s_{2}, σ⟩ →_{I} ⟨s_{2}, σ′⟩}(seq_{2})

\frac{A, C ⊢ ⟨s_{1}, σ⟩ →_{I} ⟨n, σ′⟩}{A, C ⊢ ⟨s_{1};s_{2}, σ⟩ →_{I} ⟨n, σ′⟩}(seq_{3})

\frac{A, C, σ ⊢ e →_{I} true}{A, C ⊢ ⟨if e then s_{1} else s_{2} fi, σ⟩ →_{I} ⟨s_{1}, σ⟩}(if_{1})

\frac{A, C, σ ⊢ e →_{I} false}{A, C ⊢ ⟨if e then s_{1} else s_{2} fi, σ⟩ →_{I} ⟨s_{2}, σ⟩}(if_{2})

\frac{A, C, σ ⊢ e →_{I} false}{A, C ⊢ ⟨while e do s od, σ⟩ →_{I} ⟨unit, σ⟩}(while_{1})

\frac{A, C, σ ⊢ e →_{I} true}{A, C ⊢ ⟨while e do s od, σ⟩ →_{I} ⟨s;while e do s od, σ⟩}(while_{2})

\frac{A, C, σ ⊢ e →_{I} n}{A, C ⊢ ⟨return e, σ⟩ →_{I} ⟨n, σ⟩}(ret)

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.

Definition 1 (Next 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 − i] ⋯ pat[j − 1] = pat[0] ⋯ pat[i − 1] and pat[j] ≠ pat[i]. If no such i exists then next[j] is −1.

The initialization of the next table is described by the pseudocode in Figure 1,^{3} where 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.

                     j := 0; t := -1; next[0] := -1;
                     while j < lpat - 1 do
                       while t >= 0 and pat[j] != pat[t] do
                         t := next[t]
                       od;
                       t := t+1; j := j+1;
                       if pat[j] = pat[t]
                       then next[j] := next[t]
                       else next[j] := t
                       fi
                     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.

                j := 0; k := 0;
                while j<lpat and k<ltxt do
                  while j >= 0 and pat[j] != txt[k] do
                    j := next[j]
                  od;
                  k := k+1;
                  j := j+1
                od;
                if j >= lpat then return k-j else return -1 fi

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.

Definition 2 (Comparison) An imperative comparison for the string matcher of Section 2.4 is a derivation tree of the form

\frac{E}{A, C, σ ⊢ pat[j] != txt[k] →_{I} b}(opr)

where E denotes another 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} (\frac{E}{A, C, σ ⊢ pat[j] != txt[k] →_{I} b}(opr)) = (σ(j), σ(k))

Definition 4 (Computation) An imperative computation is a derivation of the imperative matcher

\frac{S_{0}}{A, C ⊢ ⟨s_{0}, σ_{0}⟩ →_{I} ⟨s_{1}, σ_{1}⟩},

\frac{S_{1}}{A, C ⊢ ⟨s_{1}, σ_{1}⟩ →_{I} ⟨s_{2}, σ_{2}⟩},

⋮

\frac{S_{n−1}}{A, C ⊢ ⟨s_{n−1}, σ_{n−1}⟩ →_{I} ⟨r, σ_{n}⟩}

where the premises S_{0}, S_{1}, ..., S_{n−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} ∪ ℕ.

In an imperative computation, each premise might contain imperative comparisons. 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.

Definition 5 (Trace) Let S_{0}, S_{1}, ..., S_{n−1} be the premises of an imperative computation. Let c_{i} be the set of imperative comparisons in S_{i}, for 0 ≤ i < n. Let p_{i} = {index_{I}(c)|c ∈ c_{i}}, for 0 ≤ i < n. The imperative trace is the sequence π(p_{0}) · π(p_{1}) ⋯ π(p_{n−1}), where

π(p) = \{ \begin{matrix}ε & if p = ∅ \\ p & otherwise \end{matrix}

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_{I} = {⟨P, σ⟩ | σ(j) ≥ 0}
Compare_{I} = {⟨W;P, σ⟩ | σ(j) ≥ 0}
Shift_{I} = {⟨j := next[j];W;P, σ⟩}

where

     P = while j<lpat and k<ltxt do
            while j >= 0 and pat[j] != txt[k] do
              j := next[j]
            od;
            k := k+1;
            j := j+1
          od;
          if j >= lpat then return k-j else return -1 fi
     W = while j >= 0 and pat[j] != txt[k] do
              j := next[j]
           od;
           k := k+1;
           j := j+1

The set of imperative program points is defined as the sum

PP_{I} = Match_{I} + Compare_{I} + Shift_{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_{I}^{fin} + States_{I}^{int}
States_{I}^{fin} = {−1} + ℕ
States_{I}^{int} = {match, compare, shift} × ℕ × ℕ

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_{I}^{int} × (PP_{I} ∪ {⟨n, σ⟩|n ∈ ℕ} ∪ {⟨−1, σ⟩}):

(match, j, k) ≃_{I} ⟨s, σ⟩ ∈ Match_{I}  if σ(j) = j ∧ σ(k) = k
(compare, j, k) ≃_{I} ⟨s, σ⟩ ∈ Compare_{I} if σ(j) = j ∧ σ(k) = k
(shift, j, k) ≃_{I} ⟨s, σ⟩ ∈ Shift_{I}  if σ(j) = j ∧ σ(k) = k
n ≃_{I} ⟨n′, σ⟩  if n = n′
−1 ≃_{I} ⟨−1, σ⟩

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_{I}^{int} × States_{I}:

(match, j, k) ⇝_{I} \begin{cases}(compare, j, k) & if j < |pat| ∧ k < |txt| \\ k − j & if j ≥ |pat| \\ −1 & otherwise \end{cases}

(compare, j, k) ⇝_{I} \begin{cases}(shift, j, k) & if txt[k] ≠ pat[j] \\ (match, j + 1, k + 1) & otherwise \end{cases}

(shift, j, k) ⇝_{I} \begin{cases}(compare, next[j], k) & if next[j] ≠ −1 \\ (match, 0, k + 1) & otherwise \end{cases}

Definition 10 (Last) The function last_{I} yields the last element of a nonempty sequence of abstract states:

last_{I} : States_{I}^{+} → States_{I}
last_{I}(s_{1} · s_{2} ⋯ s_{n}) = s_{n}

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, 0) ∈ AbsComp_{I} and
(2) S ∈ AbsComp_{I} ∧ last_{I}(S) ⇝_{I} p ⇒ S · p ∈ AbsComp_{I}.

S is said to be complete iff last_{I}(S) ∈ States_{I}^{fin}.

Lemma 1 (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, 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 S = (compare, j, k), and then index_{I}(C) = (j, k).

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}, S = (match, j, k), S ≃_{I} P and j ≥ k. The other cases are similar.

The derivation is

 \frac{\frac{\frac{\frac{\frac{n_{1} = σ(j)}{A, C, σ ⊢ j →_{I} n_{1}} (var) \frac{n_{2} = C(lpat)}{A, C, σ ⊢ lpat →_{I} n_{2}} (const) operate(<, n_{1}, n_{2}) = false}{A, C, σ ⊢ j<lpat →_{I} false}(opr)}{A, C, σ ⊢ j<lpat and k<ltxt →_{I} false}(and_{1})}{A, C ⊢ ⟨while j<lpat and k<ltxt do ... od, σ⟩ →_{I} ⟨unit, σ⟩}(while_{1})}{A, C ⊢ ⟨(\begin{matrix}while j<lpat & and k<ltxt do ... od; \\ if j >= lpat & then return k-j \\ & else return -1 fi \end{matrix}), σ⟩ →_{I} ⟨if j >= lpat then return k-j else return -1 fi, σ⟩}(seq_{2})

\frac{\frac{\frac{n_{1} = σ(j)}{A, C, σ ⊢ j →_{I} n_{1}} (var) \frac{n_{2} = C(lpat)}{A, C, σ ⊢ lpat →_{I} n_{2}} (const) operate(>=, n_{1}, n_{2}) = true}{A, C, σ ⊢ j >= lpat →_{I} true}(opr)}{A, C ⊢ ⟨if j >= lpat then return k-j else return -1 fi, σ⟩ →_{I} ⟨return k-j, σ⟩} (if_{1})

\frac{\frac{\frac{n_{1} = σ(k)}{A, C, σ ⊢ k →_{I} n_{1}} (var) \frac{n_{2} = σ(j)}{A, C, σ ⊢ j →_{I} n_{2}} (var) n = operate(-, n_{1}, n_{2})}{A, C, σ ⊢ k-j →_{I} n}(opr)}{A, C ⊢ ⟨return k-j, σ⟩ →_{I} ⟨n, σ⟩}(ret)

Since (match, j, k) ⇝_{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} : States_{I}^{+} → States_{I}^{∗}
trace_{I}(s_{1} · s_{2} ⋯ s_{n}) = π(s_{1}) · π(s_{2}) ⋯ π(s_{n})

where π(s_{i}) = s_{i} if s_{i} = (compare, j, k) and π(s_{i}) = ε otherwise.

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, let {(j_{1}, k_{1})} · {(j_{2}, k_{2})} ⋯ {(j_{n}, k_{n})} be the imperative trace for a complete imperative computation, and let (compare, j′_{1}, k′_{1})·(compare, j′_{2}, k′_{2}) ⋯ (compare, j′_{m}, k′_{m}) be the abstract imperative trace for the corresponding complete abstract imperative computation. Then n = m and j_{i} = j′_{i} and k_{i} = k′_{i} for 0 < i ≤ n.

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 (tailrecursive 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^{∗}.

           p ::= (letrec([f_{1} (λ(x⃗_{1}) e_{1})] ... [f_{n} (λ(x⃗_{n}) e_{n})]) e)

e ::= t | (if t e_{1} e_{2}) | (f t_{1} ... t_{m})
t ::= num | x | (opr t_{1} t_{2})

         opr ::= + | - | = | eq? | string-ref

3.2 Expressible values

A value is an integer, a boolean, a character, or a string:

Val = ℤ + 𝔹 + Σ + Σ^{∗}

3.3 Rules

3.3.1 Auxiliary constructs

The language includes numeric operators, a comparison operator over characters and a string-indexing operator.

number(num) = n, if num denotes n
operate(+, n_{1}, n_{2}) = n_{1} + n_{2}
operate(-, n_{1}, n_{2}) = n_{1} − n_{2}
operate(=, n_{1}, n_{2}) = n_{1} = n_{2}
operate(eq?, c_{1}, c_{2}) = c_{1} = c_{2}
operate(string-ref, s, i) = c, if 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 θ ∈ Fenv:

ρ : Vid → ℤ + Σ^{∗}
θ : Fid → Vid^{∗} × Exp

3.3.3 Relations

The (big-step) evaluation relation for trivial expressions reads as

ρ ⊢ t →_{F} v

and the (small-step) evaluation relation for serious expressions reads as

θ ⊢ ⟨e, ρ⟩ →_{F} ⟨r, ρ′⟩

where ρ, ρ′ ∈ Venv, t ∈ Triv, v ∈ Val, θ ∈ Fenv, e ∈ Exp, and r ∈ Exp + Val.

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

             (letrec([x_{1} (λ(x⃗_{1}) e_{1})] ... [x_{n} (λ(x⃗_{n}) e_{n})]) e_{0})

is thus ⟨e_{0}, ρ_{0}⟩ in the function environment θ:

θ = θ_{0}[\begin{matrix}x_{1} ↦ ⟨x⃗_{1}, e_{1}⟩, \\ ..., \\ x_{n} ↦ ⟨x⃗_{n}, e_{n}⟩ \end{matrix}]

3.3.5 Trivial expressions

\frac{n = number(num)}{ρ ⊢ num →_{F} n}(num)

\frac{v = ρ(x)}{ρ ⊢ x →_{F} v} (var)

\frac{ρ ⊢ t_{1} →_{F} v_{1} ρ ⊢ t_{2} →_{F} v_{2} v = operate(opr, v_{1}, v_{2})}{ρ ⊢ (opr t_{1} t_{2}) →_{F} v}(opr)

3.3.6 Serious expressions

\frac{ρ ⊢ t →_{F} true}{θ ⊢ ⟨(if t e_{1} e_{2}), ρ⟩ →_{F} ⟨e_{1}, ρ⟩}(if_{1})

\frac{ρ ⊢ t →_{F} false}{θ ⊢ ⟨(if t e_{1} e_{2}), ρ⟩ →_{F} ⟨e_{2}, ρ⟩}(if_{2})

\frac{⟨x_{1} ... x_{m}, e⟩ = θ(f ) ρ ⊢ t_{1} →_{F} v_{1} ... ρ ⊢ t_{m} →_{F} v_{m}}{θ ⊢ ⟨(f t_{1} ... t_{m}), ρ⟩ →_{F} ⟨e, ρ[x_{1} ↦ v_{1}, ..., x_{m} ↦ v_{m}]⟩}(app)

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.

Definition 13 (Comparison) A functional comparison for the string matcher of Section 3.4 is a derivation tree of the form

                \frac{T}{ρ ⊢ (eq? (string-ref pat j) (string-ref txt k)) →_{F} b}(opr)

where T denotes another derivation tree.

(letrec ([match
(lambda (j k)
(if (= j lpat)
(- k j)
(if (= k ltxt)
-1
(compare j k))))]
[compare
(lambda (j k)
(if (eq? (string-ref pat j)
 (string-ref txt k))
(match (+ j 1) (+ k 1))
(if (= 0 j)
(match 0 (+ k 1))
(rematch j k 0 1))))]
[rematch
(lambda (j k jp kp)
(if (= kp j)
(if (eq? (string-ref pat jp)
     (string-ref pat kp))
(if (= jp 0)
    (match 0 (+ k 1))
    (rematch j k 0 (+ (- kp jp) 1)))
(compare jp k))
(if (eq? (string-ref pat jp)
     (string-ref pat kp))
(rematch j k (+ jp 1) (+ kp 1))
(rematch j k 0 (+ (- kp jp) 1)))))])
(match 0 0))

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} (\frac{T}{ρ ⊢ (eq? (string-ref pat j) (string-ref txt k)) →_{F} b}(opr)) = (ρ(j), ρ(k))

Definition 15 (Computation) A functional computation is a derivation of the functional matcher

\frac{E_{0}}{θ ⊢ ⟨e_{0}, ρ_{0}⟩ →_{F} ⟨e_{1}, ρ_{1}⟩},

\frac{E_{1}}{θ ⊢ ⟨e_{1}, ρ_{1}⟩ →_{F} ⟨e_{2}, ρ_{2}⟩},

⋮

\frac{E_{n−1}}{θ ⊢ ⟨e_{n−1}, ρ_{n−1}⟩ →_{F} ⟨r, ρ_{n}⟩}

where the premises E_{0}, E_{1}, ..., E_{n−1} 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} ∪ ℕ.

In a functional computation, each premise might contain functional comparisons. 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 16 (Trace) Let E_{0}, E_{1}, ..., E_{n−1} be the premises of a functional computation. Let c_{i} be the set of functional comparisons in E_{i}, for 0 ≤ i < n. Let p_{i} = {index_{F} (c)|c ∈ c_{i}} for 0 ≤ i < n. The functional trace is the sequence π(p_{0}) · π(p_{1}) ⋯ π(p_{n−1}), where

π(p) = \{ \begin{matrix}ε & if p = ∅ \\ p & otherwise. \end{matrix}

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 suffix 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_{F} = {⟨M, ρ⟩}
Compare_{F} = {⟨C, ρ⟩}
Rematch_{F} = {⟨R, ρ⟩}

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

PP_{F} = Match_{F} + Compare_{F} + Rematch_{F} .

3.6 Abstract semantics

Definition 18 (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:

States_{F} = States_{F}^{fin} + States_{F}^{int}
States_{F}^{fin} = {−1} + ℕ
States_{F}^{int} = ({match, compare} × ℕ × ℕ) +
(rematch × ℕ × ℕ × ℕ × ℕ)

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_{F}^{int} × (PP_{F} ∪ {⟨n, ρ⟩|n ∈ ℕ} ∪ {⟨−1, ρ⟩}):

(match, j, k) ≃_{F} ⟨e, ρ⟩ ∈ Match_{F}

if ρ(j) = j ∧ ρ(k) = k

(compare, j, k) ≃_{F} ⟨e, ρ⟩ ∈ Compare_{F}

if ρ(j) = j ∧ ρ(k) = k

(rematch, j, k, jp, kp) ≃_{F} ⟨e, ρ⟩ ∈ Rematch_{F}

if ρ(j) = j ∧ ρ(k) = k ∧ ρ(jp) = jp ∧ ρ(kp) = kp

n ≃_{F} ⟨n′, ρ⟩ if n = n′
−1 ≃_{F} ⟨−1, ρ⟩

Definition 20 (Abstract matcher) Let pat, txt ∈ Σ^{∗}. Then the abstract functional matcher is the following total function ⇝_{F} ⊆ States_{F}^{int} × States_{F}:

(match, j, k) ⇝_{F}

(compare, j, k) if j ≠ |pat| ∧ k ≠ |txt|
k − j  if j = |pat|
−1  otherwise

(compare, j, k) ⇝_{F}

(match, j + 1, k + 1) if txt[k] = pat[j]
(match, 0, k + 1)  if txt[k] ≠ pat[j] ∧ j = 0
(rematch, j, k, 0, 1) otherwise

(rematch, j, k, jp, kp) ⇝_{F}

(match, 0, k + 1)

if kp = j ∧ pat[jp] = pat[kp]
∧ jp = 0

(rematch, j, k, 0, kp − jp + 1)

if kp = j ∧ pat[jp] = pat[kp]
∧ jp ≠ 0
(compare, jp, k)  if kp = j ∧ pat[jp] ≠ pat[kp]
(rematch, j, k, jp + 1, kp + 1) if kp ≠ j ∧ pat[jp] = pat[kp]
(rematch, j, k, 0, kp − jp + 1) otherwise

Definition 21 (Last) The function last_{F} yields the last element of a nonempty sequence of abstract states:

last_{F} : States_{F}^{+} → States_{F} ,
last_{F} (s_{1} · s_{2} ⋯ s_{n}) = s_{n}

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, 0) ∈ AbsComp_{F}
(2) S ∈ AbsComp_{F} ∧ last_{F} (S) ⇝_{F} p ⇒ S · p ∈ AbsComp_{F} .

S is said to be complete iff last_{F} (S) ∈ States_{F}^{fin}.

Lemma 2 (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, 0) ≃_{F} P.

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 S = (compare, j, k), and then index_{F} (C) = (j, k).

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}, S = (match, j, k), S ≃_{F} P, j ≠ |pat|, and k ≠ |txt|. The other cases are similar.

The derivation is

\frac{\frac{\frac{n_{1} = ρ(j)}{ρ ⊢ j →_{F} n_{1}} (var) \frac{n_{2} = ρ(lpat)}{ρ ⊢ lpat →_{F} n_{2}} (var) operate(=, n_{1}, n_{2}) = false}{ρ ⊢ (= j lpat) →_{F} false}(opr)}{θ ⊢ ⟨(\begin{matrix}(if & (= j lpat) \\ & (- k j) \\ & (if (= k ltxt) -1 (compare j k))) \end{matrix}), ρ⟩ →_{F} ⟨(if (= k ltxt) -1 (compare j k)), ρ⟩}(if_{2})

\frac{\frac{\frac{n_{1} = ρ(k)}{ρ ⊢ k →_{F} n_{1}} (var) \frac{n_{2} = ρ(ltxt)}{ρ ⊢ ltxt →_{F} n_{2}} (var) operate(=, n_{1}, n_{2}) = false}{ρ ⊢ (= k ltxt) →_{F} false}(opr)}{θ ⊢ ⟨(if (= k ltxt) -1 (compare j k)), ρ⟩ →_{F} ⟨(compare j k), ρ⟩}(if_{2})

\frac{\frac{n_{1} = ρ(j)}{ρ ⊢ j →_{F} n_{1}} (var) \frac{n_{2} = ρ(k)}{ρ ⊢ k →_{F} n_{2}} (var) θ(compare) = ⟨j · k, C⟩}{θ ⊢ ⟨(compare j k), ρ⟩ →_{F} ⟨C, ρ[j ↦ n_{1}, k ↦ n_{2}]⟩}(app)

where C denotes the body of the compare function, as in Definition 17.

Since (match, j, k) ⇝_{F} (compare, j, k), n_{1} = ρ(j) = j and n_{2} = ρ(k) = 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_{F} : States_{F}^{+} → States_{F}^{∗}
trace_{F} (s_{1} · s_{2} ⋯ s_{n}) = π(s_{1}) · π(s_{2}) ⋯ π(s_{n})

where π(s_{i}) = s_{i} if s_{i} = (compare, j, k) and π(s_{i}) = ε otherwise.

The following corollary of Lemma 2 shows that abstract functional traces represent functional traces.

Corollary 2 (Functional traces are faithful) Let pat, txt ∈ Σ^{∗} be given, let {(j_{1}, k_{1})}·{(j_{2}, k_{2})} ⋯ {(j_{n}, k_{n})} be the functional trace for a complete functional computation, and let (compare, j′_{1}, k′_{1})·(compare, j′_{2}, k′_{2}) ⋯ (compare, j′_{m}, k′_{m}) be the abstract trace for the corresponding complete abstract functional computation. Then n = m and j_{i} = j′_{i} and k_{i} = k′_{i} for 0 < i ≤ n.

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_{2} ⋯ s_{n} ∈ AbsComp_{F}, the following conditions, whose conclusions we call invariants, are satisfied:

• If s_{i} = (match, j, k) then

(m1) 0 ≤ j ≤ |pat|
(m2) k ≤ |txt|

• If s_{i} = (compare, j, k) then

(c1) 0 ≤ j < |pat|
(c2) k < |txt|

• If s_{i} = (rematch, j, k, jp, kp) then

(r1) 0 < j < |pat|
(r2) k < |txt|
(r3) 0 ≤ jp < kp ≤ j
(r4) pat[0] ⋯ pat[jp − 1] = pat[kp − jp] ⋯ pat [kp − 1]
(r5) ∀\underline{k} ∈ [1, kp − jp − 1].

¬(\begin{matrix}pat[0] ⋯ pat[j − \underline{k} − 1] = pat[\underline{k}] ⋯ pat[j − 1] ∧ \\ pat[j − \underline{k}] ≠ pat[j]) \end{matrix}

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 ≤ j = 0 ≤ |pat| and k = 0 ≤ |txt|. Invariants (m1) 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 = |pat|: By definition, (match, j, k) ⇝_{F} k − j. The next abstract state in the abstract functional computation is therefore k−j and all the invariants are preserved.

• 0 ≤ j < |pat| ∧ k = |txt|: By definition, (match, j, k) ⇝_{F} −1. The next abstract state is therefore −1 and all the invariants are preserved.

• 0 ≤ j < |pat| ∧ k < |txt|: By definition, (match, j, k) ⇝_{F} (compare, j, k). The next abstract state is therefore (compare, j′ = j, k′ = k). By the case assumption 0 ≤ j′ = j < |pat| and k′ = k < |txt|, which satisfy 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:

• txt[k] = pat[j]: By definition, (compare, j, k) ⇝_{F} (match, j + 1, k + 1). The next abstract state in the abstract functional computation is (match, j′ = j + 1, k′ = k + 1). Since j, k, |pat| and |txt| are integers, j < |pat| ⇒ j′ = j +1 ≤ |pat|, k < |txt| ⇒ k′ = k +1 ≤ |txt|, and 0 ≤ j ⇒ 0 ≤ j +1 = j′ all hold. Since the premises are true by Invariants (c1) and (c2), Invariants (m1) and (m2) hold.

• txt[k] ≠ pat[j] ∧ j = 0: By definition, (compare, j, k) ⇝_{F} (match, 0, k + 1). The next abstract state is (match, j′ = 0, k′ = k + 1). With an argument identical to the above we obtain Invariant (m2). By inserting the value for j′ in Invariant (m1), as done in the initalization case, we also obtain Invariant (m1).

• txt[k] ≠ pat[j]∧j > 0: By definition, (compare, j, k) ⇝_{F} (rematch, j, k, 0, 1). The next abstract state is (rematch, j′ = j, k′ = k, jp′ = 0, kp′ = 1)

(r1), (r2) : Due to (c1) and j > 0, (r1) holds, and (c2) is identical to (r2).

(r3) : By insertion, 0 ≤ 0 = jp′ < kp′ = 1 ≤ j = j′, and thus (r3) holds. (r4) : Since jp′ − 1 = −1, we obtain pat[0] ⋯ pat[−1], which by conven-

tion denotes the empty string. Similarly, pat[kp′ − jp′] ⋯ pat [kp′ − 1] = pat[1] ⋯ pat[0] denotes the empty string, and Invariant (r4) holds.

(r5) : Finally, (r5) holds trivially, because the interval [1, kp′ − jp′ − 1] = [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:

• kp = j ∧pat[jp] = pat[kp]∧jp = 0: By definition, (rematch, j, k, jp, kp) ⇝_{F} (match, 0, k + 1). The next abstract state in the abstract functional computation is (match, j′ = 0, k′ = k + 1). By Invariant (r2), we obtain k′ = k + 1 ≤ |txt|, so (m2) holds. Since j′ = 0, (m1) also holds, as shown above.

• kp = j ∧pat[jp] = pat[kp]∧jp > 0: By definition, (rematch, j, k, jp, kp) ⇝_{F} (rematch, j, k, 0, kp − jp + 1). The next abstract state is (rematch, j′ = j, k′ = k, jp′ = 0, kp′ = kp − jp + 1).

(r1), (r2) : Since Invariants (r1) and (r2) hold for j and k, the trivial updates, j′ = j and k′ = k, immediately give Invariants (r1) and (r2).

(r3) : Since kp > jp ⇒ kp′ = kp − jp + 1 > 1, we have 0 ≤ jp′ = 0 < 1 < kp′. And since j′ = j = kp and jp ≥ 1, we obtain kp′ = kp − jp + 1 ≤ kp = j′ and Invariant (r3) is satisfied.

(r4) : We first look at pat[0] ⋯ pat[jp′−1], which is the empty string since jp′−1 = −1. Similarly, pat[kp′−jp′] ⋯ pat [kp′−1] = pat[kp′] ⋯ pat [kp′− 1] is the empty string, and therefore Invariant (r4) holds.

(r5) : From the invariant we know that the body of (r5) holds for every \underline{k} in the interval [1, kp′ − jp′ − 2], since j′ = j and kp′ − jp′ − 1 = kp − jp. We then only need to show that ¬(pat[0] ⋯ pat[j′ − \underline{k} − 1] = pat[\underline{k}] ⋯ pat[j′ − 1] ∧ pat[j′ − \underline{k}] ≠ pat[j′]), or more specifically ¬(pat[j − \underline{k}] ≠ pat[j]), holds for \underline{k} = kp′ − jp′ − 1. This is easily seen since j′ −\underline{k} = j −(kp −jp) = jp and j′ −\underline{k} = jp, which under the case assumption give pat[j − \underline{k}] = pat[jp] = pat[kp] = pat[j′]. Therefore Invariant (r5) holds.

• kp = j∧pat[jp] ≠ pat[kp]: By definition, (rematch, j, k, jp, kp) ⇝_{F} (compare, jp, k). The next abstract state is therefore (compare, j′ = jp, k′ = k). By (r1), (r3), and the case assumption, we have 0 ≤ j′ < j < m and therefore (c1) holds. Since k′ = k < |txt|, (c2) also holds.

• kp < j∧pat[jp] = pat[kp]: By definition, (rematch, j, k, jp, kp) ⇝_{F} (rematch, j, k, jp + 1, kp + 1). The next abstract state is therefore (rematch, j′ = j, k′ = k, jp′ = jp + 1, kp′ = kp + 1).

(r1), (r2) : (r1) and (r2) hold, since j′ = j and k′ = k.

(r3) : We have kp′ = kp+1 ≤ j′ since kp < j′, jp′ = jp+1 < kp+1 = kp′, and 0 ≤ jp + 1 = jp′ because 0 ≤ jp, which give us (r3).

(r4) : By (r4), we have pat[0] ⋯ pat[jp′−2] = pat[kp′ −jp′] ⋯ pat[kp′−2], and we only need to show pat[jp′ − 1] = pat[kp′ − 1]. This is true by the case assumption and thus (r4) holds.

(r5) : Since j′ = j, and since the interval for \underline{k} is unchanged, because kp′ − jp′ − 1 = (kp + 1) − (jp + 1) − 1 = kp − jp − 1, (r5) 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, j′ = j, k′ = k, jp′ = 0, kp′ = kp − jp + 1).

(r1), (r2) : By the trivial update of j and k, (r1) and (r2), as shown above, still hold.

(r3) : Since jp′ = 0 we clearly have jp′ ≥ 0, and the assumption kp > jp gives us kp′ = kp−jp+1 > 0 = jp′. Finally, since kp < j ⇒ kp+1 ≤ j, we have kp′ = kp −jp +1 ≤ kp +1 ≤ j′ and thus Invariant (r3) holds.

(r4) : Again, as shown in the second case, the strings are empty by the condition jp′ = 0 and thus Invariant (r4) holds.

(r5) : Similarly to the second case, we only need to show ¬(pat[0] ⋯ pat[j′− \underline{k} − 1] = pat[\underline{k}] ⋯ pat[j′ − 1] ∧ pat[j′ − \underline{k}] ≠ pat[j′]), or more specifically ¬(pat[0] ⋯ pat[j′ − \underline{k} − 1] = pat[\underline{k}] ⋯ pat[j′ − 1]), holds for \underline{k} = kp′ − jp′ − 1. We consider the jpth and (\underline{k} + jp)th entries, which are the characters pat[jp] and pat[kp], respectively, since \underline{k} + jp = (kp′ − jp′ − 1) + jp = ((kp − jp + 1) − 1) + jp = 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 kp < j and 0 ≤ jp < kp give us just that; we have 0 ≤ jp and j′ − \underline{k} − 1 = j′ − (kp − jp) − 1 = j − kp + jp − 1 ≥ 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 ∀\underline{k} ∈ [a, b].¬(pat[0] ⋯ pat[j− \underline{k} − 1] = pat[\underline{k}] ⋯ pat[j − 1] ∧ pat[j − \underline{k}] ≠ pat[j]), then by Definition 1 next[j] cannot occur in the interval [j − b, j − a].

Indeed, if for some \underline{k} and some j, (pat[0] ⋯ pat[j − \underline{k} − 1] = pat[\underline{k}] ⋯ pat[j − 1] and pat[j − \underline{k}] ≠ pat[j]), then j − \underline{k} is a candidate for next[j]. Therefore the negation of the condition gives us that j − \underline{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.

4 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, k) ≃ (match, j′, k′)  if j = j′ ∧ k = k′
(compare, j, k) ≃ (compare, j′, k′)  if j = j′ ∧ k = k′
(shift, j, k) ≃ (rematch, j′, k′, jp, kp) if j = j′ ∧ k = k′
n ≃ n′,  if n = n′
−1 ≃ −1

We define ≃^{∗}⊆ States_{I}^{∗} ×States_{F}^{∗} such that for any sequences S = s_{1} ·s_{2} ⋯ s_{p} ∈ States_{I}^{+} and S′ = s′_{1} · s′_{2} ⋯ s′_{q} ∈ States_{F}^{+}, S ≃^{∗} S′ iff p = q and s_{i} ≃ s′_{i} for all 0 < i ≤ p. We make ≃^{∗} hold for empty sequences.

Definition 25 (Synchronization) Synchronization is a relation sync ⊆ States_{I}^{+} ×States_{F}^{+} defined as

sync(S, S′) iff 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} and S′ ∈ AbsComp_{F}. The proof is by structural induction on the abstract computation S′. 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.

By definition of AbsComp_{I} and AbsComp_{F}, both abstract computations S and S′ 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}(I) = (match, j, k), and last_{F} (I′) = (match, j, k). Three cases occur, that are exhaustive by the invariants of Lemma 3:

• j = |pat| ∧ k ≤ |txt|: By definition, (match, j, k) ⇝_{F} k − j. Similarly, by definition, (match, j, k) ⇝_{I} k − j. By assumption, sync(I, I′) holds, and therefore sync(I · (k − j), I′ · (k − j)) also holds, and thus the complete abstract computations S = I ·(k−j) and S′ = I′ ·(k−j) are synchronized.

• j < |pat| ∧ k = |txt|: By definition, (match, j, k) ⇝_{F} −1. Similarly, by definition, (match, j, k) ⇝_{I} −1. As above, synchronization is preserved since the computations end with the same integer.

• j < |pat| ∧ k < |txt|: By definition, (match, j, k) ⇝_{F} (compare, j, k). Similarly, by definition, (match, j, k) ⇝_{I} (compare, j, k). Since sync(I, I′) holds 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}(I) = (compare, j, k), and last_{F} (I′) = (compare, j, k). Three cases occur, that are exhaustive by the invariants of Lemma 3:

• txt[k] ≠ pat[j] ∧ j = 0: By definition, (compare, j, k) ⇝_{F} (match, 0, k + 1). Similarly, by definition, (compare, j, k) ⇝_{I} (shift, j, k) ⇝_{I} (match, 0, k +1) since next[j] = −1 by definition. Since sync(I, I′) by assumption, and the shift states are not included in the abstract trace, sync(I · (shift, j, k) · (match, 0, k + 1), I′ · (match, 0, k + 1)) holds.

• txt[k] ≠ pat[j]∧j > 0: By definition, (compare, j, k) ⇝_{F} (rematch, j, k, 0, 1). Similarly, by definition, (compare, j, k) ⇝_{I} (shift, j, k). Since sync(I, I′) holds by assumption, and (shift, j, k) ≃ (rematch, j, k, 0, 1), sync(I·(shift, j, k), I′ · (rematch, j, k, 0, 1)) also holds.

• txt[k] = pat[j]: By definition, (compare, j, k) ⇝_{F} (match, j + 1, k + 1). Similarly, by definition, (compare, j, k) ⇝_{I} (match, j + 1, k + 1). Since sync(I, I′) holds by assumption, sync(I ·(match, j +1, k +1), I′ ·(match, j + 1, k + 1)) also holds.

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}(I) = (shift, j, k), and last_{F} (I′) = (rematch, j, k, jp, kp). Since by Definition 24, (shift, j, k) ≃ (rematch, j, k, jp, kp) 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 different 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:

• kp = j ∧pat[jp] = pat[kp]∧jp = 0: By definition, (rematch, j, k, jp, kp) ⇝_{F} (match, 0, k + 1). We know that Invariant (r5) holds for \underline{k} in the interval [1, j − 1], which by Remark 1 implies that next[j] ∉ [1, j − 1]. From the case assumption, we know that pat[0] = pat[kp], so next[j] ≠ 0. Since next[j] ∈ [−1, j − 1] we then have next[j] = −1. Therefore, by definition of the abstract imperative matcher, (shift, j, k) ⇝_{I} (match, 0, k+1). Since sync(I, I′) holds by assumption, sync(I·(match, 0, k+1), I′·(match, 0, k+1)) also holds.

• kp = j ∧ pat[jp] ≠ pat[kp]: Due to Invariants (r1) and (r3), we have jp < j < |pat|. By definition, (rematch, j, k, jp, kp) ⇝_{F} (compare, jp, k). We know that the body of Invariant (r5) holds for \underline{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 pat[0] ⋯ pat[jp − 1] = pat[j − jp] ⋯ pat[j − 1], and by the case assumption we have pat[jp] ≠ pat[j]. Therefore, jp is a candidate for next[j]. Since next[j] ∉ [jp + 1, j − 1] and since next[j] is the largest value less than j − 1 satisfying the requirements, we have next[j] = jp. By Invariant (r3) we know that jp ≥ 0, so by definition of the abstract imperative matcher, (shift, j, k) ⇝_{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 4)

[figure]

[figure]

abstract functional matcher (Section 3.6)

[figure]

[figure]

concrete imperative matcher (Section 2.5)

Lemma 1 (Section 2.6)

[figure]

concrete functional matcher (Section 3.5)

Lemma 2 (Section 3.6)

[figure]

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 computation, C′, with final configuration ⟨n′, ρ⟩, for some number, n′, (3) n = n′, and (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 different 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 partialevaluation 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})
                      (if (= j lpat)
                          ( -  k j)
                          ( if  ( =  k ltxt)
                              -1
                              (compare j k))))]
                   [compare
                    (lambda (j^{s}  k^{d})
                      ( if  ( eq?  (string-ref pat j)
                                  (string-ref txt k))
                          (match (+ j 1) ( +  k 1))
                          (if (= 0 j)
                              (match 0 ( +  k 1))
                              (rematch j k 0 1))))]
                   [rematch
                    (lambda (j^{s}  k^{d}  jp^{s}  kp^{s})
                      (if (= kp j)
                          (if (eq? (string-ref pat jp)
                                   (string-ref pat kp))
                              (if (= jp 0)
                                  (match 0 ( +  k 1))
                                  (rematch j k 0 (+ (- kp jp) 1)))
                              (compare jp k))
                          (if (eq? (string-ref pat jp)
                                   (string-ref pat kp))
                              (rematch j k (+ jp 1) (+ kp 1))
                              (rematch j k 0 (+ (- kp jp) 1)))))])
            (match 0 0))))

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}  k)
      (if (= k ltxt) -1 (compare_{|abac}  k)))
    (define (compare_{|abac}  k)
      (if (eq? #\a (string-ref txt k))
          (match_{a|bac}  (+ k 1))

          (match_{|abac}  (+ k 1))))

    (define (match_{a|bac}  k)
      (if (= k ltxt) -1 (compare_{a|bac}  k)))
    (define (compare_{a|bac}  k)
      (if (eq? #\b (string-ref txt k))
          (match_{ab|ac}  (+ k 1))

          (compare_{|abac}  k)))

    (define (match_{ab|ac}  k)
      (if (= k ltxt) -1 (compare_{ab|ac}  k)))
    (define (compare_{ab|ac}  k)
      (if (eq? #\a (string-ref txt k))
          (match_{aba|c}  (+ k 1))

          (match_{|abac}  (+ k 1))))

    (define (match_{aba|c}  k)
      (if (= k ltxt) -1 (compare_{aba|c}  k)))
    (define (compare_{aba|c}  k)
      (if (eq? #\c (string-ref txt k))
          (- (+ k 1) 4)
          (compare_{a|bac}  k)))
    (match_{|abac}  0)))

• For all txt, evaluating (main-abac txt) yields the same result as evalu-

  ating (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 k) 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 k)
                      (if (= j lpat)
                          (- k j)
                          (if (= k ltxt)
                              -1
                              (compare j k))))]
                   [compare
                    (lambda (j k)
                      (if (eq? (string-ref pat j)
                               (string-ref txt k))
                          (match (+ j 1) (+ k 1))
                          (if (= 0 j)
                              (match 0 (+ k 1))
                              (let ([next (rematch j 0 1)])
                                (if (= next -1)
                                    (match 0 (+ k 1))
                                    (compare next k))))))]
                   [rematch
                    (lambda (j jp kp)
                      (if (= kp j)
                          (if (eq? (string-ref pat jp)
                                   (string-ref pat kp))
                              (if (= jp 0)
                                  -1
                                  (rematch j 0 (+ (- kp jp) 1)))
                              jp)
                          (if (eq? (string-ref pat jp)
                                   (string-ref pat kp))
                              (rematch j (+ jp 1) (+ kp 1))
                              (rematch j 0 (+ (- kp jp) 1)))))])
            (match 0 0))))

Figure 6: 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 0 ≤ j < |pat|, jp = 0, and kp = 1. 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 information, 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 effect 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 efficient, 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 efficient, 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 efficient string matchers by partial evaluation of a naive string matcher and obtaining them efficiently.

The essence of obtaining efficient 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. However, 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 efficient 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 effect 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 suffixes 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 suffix of txt or it starts to match pat and the next suffix of txt.

Figure 8 displays a staged version of the quadratic string matcher. Instead of matching pat and the next suffix of txt, this version uses a rematch function and a recompare function to first match pat and a prefix of a suffix 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.

References

[1] Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The abstraction and instantiation of string-matching programs. Technical Report BRICS RS-01-12, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, April 2001. To appear in Neil Jones’s Festschrift.

[2] Guntis J. Barzdins and Mikhail A. Bulyonkov. Mixed computation and translation: Linearisation and decomposition of compilers. Preprint 791, Computing Centre of Siberian Division of USSR Academy of Sciences, Novosibirsk, Siberia, 1988.

[3] Anders Bondorf. Similix 5.1 manual. Technical report, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, May 1993. Included in the Similix 5.1 distribution.

[4] Anders Bondorf and Olivier Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming, 16:151–195, 1991.

[5] Christian Charras and Thierry Lecroq. Exact string matching algorithms.

http://www-igm.univ-mlv.fr/~lecroq/string/, 1997.

[6] Sandrine Chirokoff, Charles Consel, and Renaud Marlet. Combining program and data specialization. Higher-Order and Symbolic Computation, 12(4):309–335, 1999.

[7] Charles Consel and Olivier Danvy. Partial evaluation of pattern matching in strings. Information Processing Letters, 30(2):79–86, January 1989.

(define (main pat txt)
(let ([lpat (string-length pat)] [ltxt (string-length txt)])
(letrec ([match
(lambda (j k)
(if (= j lpat)
(- k j)
(if (= k ltxt)
    -1
    (compare j k))))]
[compare
(lambda (j k)
(if (eq? (string-ref pat j) (string-ref txt k))
(match (+ j 1) (+ k 1))
(match 0 (+ (- k j) 1))))])
(match 0 0))))

Figure 7: The naive, quadratic functional matcher

(define (main pat txt)
(let ([lpat (string-length pat)] [ltxt (string-length txt)])
(letrec ([match
(lambda (j k)
(if (= j lpat)
(- k j)
(if (= k ltxt)
    -1
    (compare j k))))]
[compare
(lambda (j k)
(if (eq? (string-ref pat j)
     (string-ref txt k))
(match (+ j 1) (+ k 1))
(if (= 0 j)
    (match 0 (+ k 1))
    (letrec ([rematch
              (lambda (jp jk)
                (if (= jk j)
                    (compare jp k)
                    (recompare jp jk)))]
             [recompare
              (lambda (jp jk)
                (if (eq? (string-ref pat jp)
                         (string-ref pat jk))
                    (rematch (+ jp 1) (+ jk 1))
                    (rematch 0 (+ (- jk jp) 1))))])
      (rematch 0 1)))))])
(match 0 0))))

Figure 8: The functional matcher with positive information

(define (main pat txt)
(let ([lpat (string-length pat)] [ltxt (string-length txt)])
(letrec ([match
(lambda (j k)
(if (= j lpat)
(- k j)
(if (= k ltxt)
    -1
    (compare j k))))]
[compare
(lambda (j k)
(if (eq? (string-ref pat j) (string-ref txt k))
(match (+ j 1) (+ k 1))
(if (= 0 j)
    (match 0 (+ k 1))
    (letrec
       ([rematch
         (lambda (jp kp)
           (if (= kp j)
               (if (eq? (string-ref pat jp)
                        (string-ref pat kp))
                   (if (= jp 0)
                       (match 0 (+ k 1))
                   (rematch 0 (+ (- kp jp) 1)))
               (compare jp k))
           (recompare jp kp)))]
        [recompare
         (lambda (jp kp)
           (if (eq? (string-ref pat jp)
                    (string-ref pat kp))
               (rematch (+ jp 1) (+ kp 1))
               (rematch 0 (+ (- kp jp) 1))))])
       (rematch 0 1)))))])
(match 0 0))))

Figure 9: The functional matcher with positive information and one character of negative information

[8] Olivier Danvy and Ulrik P. Schultz. Lambda-dropping: Transforming recursive equations into programs with block structure. Theoretical Computer Science, 248(1-2):243–287, 2000.

[9] Yoshihiko Futamura, Zenjiro Konishi, and Robert Glück. Program transformation system based on generalized partial computation. New Generation Computing, 20(1):75–99, 2002.

[10] Yoshihiko Futamura and Kenroku Nogi. Generalized partial computation. In Dines Bjørner, Andrei P. Ershov, and Neil D. Jones, editors, Partial

(define (main pat txt)
(let ([lpat (string-length pat)] [ltxt (string-length txt)])
  (letrec ([match
            (lambda (j k)
              (if (= j lpat)
                  (- k j)
                  (if (= k ltxt)
                      -1
                      (compare j k))))]
           [compare
            (lambda (j k)
              (if (eq? (string-ref pat j) (string-ref txt k))
                  (match (+ j 1) (+ k 1))
                  (if (= 0 j)
                      (match 0 (+ k 1))
                      (rematch j k 0 1))))]
           [rematch
            (lambda (j k jp kp)
              (if (= kp j)
                  (if (eq? (string-ref pat jp) (string-ref pat kp))
                      (if (= jp 0)
                          (match 0 (+ k 1))
                          (rematch j k 0 (+ (- kp jp) 1)))
                      (compare jp k))
                  (if (eq? (string-ref pat jp) (string-ref pat kp))
                      (rematch j k (+ jp 1) (+ kp 1))
                      (rematch j k 0 (+ (- kp jp) 1)))))])
    (match 0 0))))

Figure 10: The functional matcher with positive information and one character of negative information (final version)

Evaluation and Mixed Computation, pages 133–151. North-Holland, 1988.

[11] Yoshihiko Futamura, Kenroku Nogi, and Akihiko Takano. Essence of generalized partial computation. Theoretical Computer Science, 90(1):61–79, 1991.

[12] Robert Glück and Andrei Klimov. Occam’s razor in metacomputation: the notion of a perfect process tree. In Patrick Cousot, Moreno Falaschi, Gilberto Filé, and Antoine Rauzy, editors, Proceedings of the Third International Workshop on Static Analysis WSA’93, number 724 in Lecture Notes in Computer Science, pages 112–123, Padova, Italy, September 1993. Springer-Verlag.

[13] Bernd Grobauer and Julia L. Lawall. Partial evaluation of pattern matching in strings, revisited. Nordic Journal of Computing, 8(4):437–462, 2002.

[14] Thomas Johnsson. Lambda lifting: Transforming programs to recursive equations. In Jean-Pierre Jouannaud, editor, Functional Programming Languages and Computer Architecture, number 201 in Lecture Notes in Computer Science, pages 190–203, Nancy, France, September 1985. Springer-Verlag.

[15] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, London, UK, 1993. Available online at

http://www.dina.kvl.dk/~sestoft/pebook/.

[16] Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised^{5} report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1):7–105, 1998.

[17] Todd B. Knoblock and Erik Ruf. Data specialization. In Proceedings of the ACM SIGPLAN’96 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 31, No 5, pages 215–225. ACM Press, June 1996.

[18] Donald E. Knuth, James H. Morris, and Vaughan R. Pratt. Fast pattern matching in strings. SIAM Journal on Computing, 6(2):323–350, 1977.

[19] Karoline Malmkjær. Program and data specialization: Principles, applications, and self-application. Master’s thesis, DIKU, Computer Science Department, University of Copenhagen, August 1989.

[20] Karoline Malmkjær. Abstract Interpretation of Partial-Evaluation Algorithms. PhD thesis, Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas, March 1993.

[21] Torben Æ. Mogensen. Glossary for partial evaluation and related topics. Higher-Order and Symbolic Computation, 13(4):355–368, 2000.

[22] Simon Peyton Jones and André Santos. A transformation-based optimiser for Haskell. Science of Computer Programming, 32(1-3):3–47, 1998.

[23] Christian Queinnec and Jean-Marie Geffroy. Partial evaluation applied to pattern matching with intelligent backtrack. In Proceedings of the Second International Workshop on Static Analysis WSA’92, volume 81-82 of Bigre Journal, pages 109–117, Bordeaux, France, September 1992. IRISA, Rennes, France.

[24] Donald A. Smith. Partial evaluation of pattern matching in constraint logic programming languages. In Paul Hudak and Neil D. Jones, editors, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, SIGPLAN Notices, Vol. 26, No 9, pages 62–71, New Haven, Connecticut, June 1991. ACM Press.

[25] Morten Heine Sørensen, Robert Glück, and Neil D. Jones. A positive supercompiler. Journal of Functional Programming, 6(6):811–838, 1996.

Recent BRICS Report Series Publications

RS-02-32 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation. July 2002. 43 pp. To appear in Chin, editor, ACM SIGPLAN ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ASIA-PEPM ’02 Proceedings, 2002.

RS-02-31 Ulrich Kohlenbach and Paulo B. Oliva. Proof Mining: A Systematic Way of Analysing Proofs in Mathematics. June 2002. 47 pp.

RS-02-30 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. June 2002.

RS-02-29 Christian N. S. Pedersen and Tejs Scharling. Comparative Methods for Gene Structure Prediction in Homologous Sequences. June 2002. 20 pp.

RS-02-28 Ulrich Kohlenbach and Laurenţiu Leuştean. Mann Iterates of Directionally Nonexpansive Mappings in Hyperbolic Spaces. June 2002. 33 pp.

RS-02-27 Anna Östlin and Rasmus Pagh. Simulating Uniform Hashing in Constant Time and Optimal Space. 2002. 11 pp.

RS-02-26 Margarita Korovina. Fixed Points on Abstract Structures without the Equality Test. June 2002.

RS-02-25 Hans Hüttel. Deciding Framed Bisimilarity. May 2002. 20 pp.

RS-02-24 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Static Analysis for Dynamic XML. May 2002. 13 pp.

RS-02-23 Antonio Di Nola and Laurenţiu Leuştean. Compact Representations of BL-Algebras. May 2002. 25 pp.

RS-02-22 Mogens Nielsen, Catuscia Palamidessi, and Frank D. Valencia. On the Expressive Power of Concurrent Constraint Programming Languages. May 2002. 34 pp.

RS-02-21 ZoltánÉsik and Werner Kuich. Formal Tree Series. April 2002. 66 pp.