|
Mitchell Wand. Putting Failure in Context: Abstract Data Types of Computations and Contexts. submitted for publication, March 2003.
There are two standard models of backtracking programs: a model in which the many possible answers are represented as a stream, and a model in which the action of the backtracking program is represented by two continuations: a success continuation and a failure continuation. These two models, both intuitively plausible, have never been (to our knowledge) been formally related. We show how the two-continuation model can be derived from the stream model. We do this by treating computations and contexts as abstract data types. We start by representing computations as elements in a term algebra. We derive an operational semantics for this term algebra by representing it in an extension of call-by-value PCF. This allows us to build an algebra of contexts, in which the usual representation of contexts as terms with holes is an initial algebra. We then represent these contexts as a final algebra using two observers, one representing the action of the context on success, and one representing its action on failure. Finally, we regain a compositional semantics by representing computations by their action on contexts.
The two approaches for modelling backtracking were mentioned here in the past. Not only are they relevant for logic programming, they are also important for other situations requiring goal directed evaluation (e.g., Icon).
Note that the paper makes use of quite a few theoretical tools (operational and denotational semantics, algebraic and coalgebraic teqhniques, monads etc.), which may make it a bit difficult to read.
Posted to theory by Ehud Lamm on 4/6/03; 12:39:10 PM
|
|
Putting Failure in Context: ADTs of Computations & Contexts
