Henning Korsholm Rohde:
Formal Aspects of Partial Evaluation.
PhD thesis, BRICS, University of Aarhus, Denmark (December
2005). Available as technical report BRICS-DS-05-9.
Thesis advisors: Olivier Danvy and Andrzej Filinski.
Thesis committee: Yoshihiko Futamura, Mogens Nielsen, and
Peter Sestoft.
Defended on December 19, 2005. [slides]
Abstract
We present a systematic approach for analyzing the
information-propagation aspect of advanced program transformations through
their application to string matching.
Our results are based on
a combination of formal
and experimental analysis.
In the formal line,
we consider fundamental partial-evaluation techniques.
Foremost, we
establish correctness
of a normalization-by-evaluation construction for the untyped
lambda-beta-calculus, as well as
provide the first formalization and correctness proof of a
polyvariant specialization algorithm. These core results are necessary for
reasoning robustly about the outcomes of such transformations.
Notably, we establish the first correctness proof of the `folklore'
result that a polyvariant specializer can transform an
inefficient binding-time-improved string matcher into the search phase
of the Knuth-Morris-Pratt algorithm.
More importantly, the proof itself exposes the sequence of dynamic
character accesses (and in turn comparisons) as an accurate
characterization of the "behavior" of string matchers.
For the Knuth-Morris-Pratt example, we show that further rewriting of
the binding-time-improved string matcher and adding efficient static
memoization enables efficient polyvariant specialization.
In the experimental line,
we show that the behavior of string matchers
turns out to accurately reflect the information propagated by advanced program
transformations.
We present a
comprehensive framework that lets us obtain the search
phases of numerous string-matching algorithms from the literature,
using polyvariant specialization.
Notably, we establish and exploit the insight that the Boyer-Moore
algorithm's highly efficient bad-character-shift heuristic can
be captured by a select application of bounded static variation.
Generalizing the so-called "KMP-test", our framework thus constitutes a
platform for measuring and experimenting with information
propagation in program transformations.
|
|
[dvi,ps,pdf]
|