A semantics-based determinacy analysis for prolog with cut

Abstract

At PEPM’91 Sahlin presented a determinacy analysis for Prolog with cut. The analysis was, however, not justified in any kind of semantics for Prolog, so correctness was argued with respect to an intuitive idea of the behaviour of Prolog programs. We now start with a denotational semantics of Prolog and derive a variant of Sahlins analysis as an abstraction of this. We observe that we avoid some problems Sahlin had, and in addition get rid of some redundant domain elements, which our semantics show can not be distinguished by any context. To obtain better precision in the abstract interpretation we do fixed-point iteration in two steps: First we find the least equivalence class using a powedomain ordering, then we find the least fixed-point within that equivalence class using the subset ordering. We believe this method is original.