Backtracking in recursive computations

Summary A mathematical (denotational) semantics is constructed for a formalism of recursive equations with the Alternative operator. This formalism enables the combination of recursion and backtracking. The semantics is defined by applying fixpoint theory to set valued functions. We introduce the notion of strategy to produce subsets of the result. Two implementations are suggested using an auxiliary stack, that trade off recomputation time with space in the auxiliary stack. The concept of a sub-fixpoint is introduced, and the implementations are shown to be incomplete even w.r.t. sub-fixpoint values. One special strategy, the leftmost strategy, which stems from problems such as pattern matching or parsing, is discussed.