SOS 2004 Preliminary Version Toward the concept of backtracking computation

This article proposes a new mathematical definition of the execution of pure Prolog, in the form of axioms in a structural operational semantics. The main advantage of the model is its ease in representing backtracking, due to the functionality of the transition relation and its converse. Thus, forward and backward derivation steps are possible. A novel concept of stages is introduced, as a refinement of final states, which captures the evolution of a backtracking computation. An advantage over the traditional stack-of-stacks approaches is a modularity property. Finally, the model combines the intuition of the traditional ‘Byrd box ’ metaphor with a compact representation of execution state, making it feasible to formulate and prove theorems about the model. In this paper we introduce the model and state some useful properties. Key words: backtracking, Prolog, operational semantics 1 Motivation, aims and results In this paper, we introduce S1:PP, a new operational semantics for pure Prolog, and establish some useful properties, aiming toward an algebraic definition of the concept of Prolog computation. On the way, we obtain some new concepts useful for characterizing backtracking, but possibly also useful for objects which evolve over time. Such an object is in logic programming the goal, in its dynamic sense (‘this unique, run-time invocation of a Prolog procedure’), as opposed to its static or syntactic sense (‘this goal formula’). The goal is a basic concept of logic programming, but nevertheless one which proved hard to grasp in a formal way, even in the case of pure Prolog. The problem is the possible evolution of ‘the ’ goal through slightly different identities, in case of a non-deterministic procedure.