Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10328939 | Electronic Notes in Theoretical Computer Science | 2005 | 21 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Marija Kulaš,