Nicolas Feltman
PhD Student in the Computer Science Department- CMU
Creating Data Structures from Algorithms by Stage-splitting a Modal Language
Abstract:
Many algorithms
operate by first building a searchable index structure over some data
and then repeatedly performing queries on that index. It is often
observed that the form and invariants of such intermediate data
structures (e.g. a list sorted by quicksort) mirror the design of a
divide-and-conquer algorithm (quickselect). Our goal is to
automatically derive the former from the latter. We accomplish
this by writing the divide-and-conquer algorithm in a two-stage lambda
calculus (corresponding to non-branching temporal logic) and running a
stage-splitting algorithm to factor this one two-stage program into two
one-stage programs. We also discuss possible applications of our
lambda calculus in the design of domain-specific languages, wherein the
stage-splitting algorithm becomes part of the compilation process.