Subset assertions and negation as failure
Mauricio Osorio, Bharat Jayaraman · 1993
Subset assertions provide a declarative and natural means for expressing solutions to many problems involving sets. This paper is motivated by the use of subset assertions for formulating transitive closures and solving containment constraints in applications of graph traversal and program analysis. In these applications, circular containment constraints may arise, for which we propose an operational strategy based upon memoization and reexecution of function calls. We provide formal declarative and operational semantics for this class of subset assertions. One of the main technical results of this paper is a succinct translation of subset assertions into normal program clauses [L87] such that the stratified semantics of the resulting normal programs coincides with the declarative semantics of subset assertions. This translation is interesting because the operational semantics of subset assertions appears to be very different from that of normal programs---due to the setof-like capabil...