We present techniques for incremental computing by introducing
adaptive functional programming. As an {\em adaptive} program
executes, the underlying system represents the data and control
dependences in the execution in the form of a {\em dynamic dependence
graph}. When the input to the program changes, a change propagation
algorithm updates the output and the dynamic dependence graph by
propagating changes through the graph and re-executing code where
necessary. Adaptive programs adapt their output to any change in the
input, small or large.
We show that adaptivity techniques are practical by giving an
efficient implementation as a small ML library. The library consists
of three operations for making a program adaptive, plus two operations
for making changes to the input and adapting the output to these
changes. We give a general bound on the time it takes to adapt the
output, and based on this, show that an adaptive Quicksort adapts its
output in logarithmic time when its input is extended by one key.
To show the safety and correctness of the mechanism we give a formal
definition of \AFL{}, a call-by-value functional language extended
with adaptivity primitives. The modal type system of \AFL{} enforces
correct usage of the adaptivity mechanism, which can only be checked
at run time in the ML library. Based on the \AFL{} dynamic semantics,
we formalize the \ncpa{} and prove its correctness.