Computable Set Theory and Logic Programming
Agostino Dovier · 2014
Interpretation An Abstract Interpreter is a static analysis tool used to extract information on properties of the program to be analyzed. Its main goal is to rewrite the original program substituting the actual operations (which implicitly work on the Herbrand universe) with their abstract equivalents on the abstract domain. In particular, the various operations performed during standard resolution (e.g., unification, application of substitutions) need to be properly abstracted. In the Ms system [32], for instance, each clause for a predicate p in the original program is rewritten according to a suitable translation scheme and stored with a modified head p$cl. Moreover, an additional clause with head p$pred is introduced as a driver for the execution of a p-based goal, with the task of allowing the test of all the different possible paths (i.e., all the matching clauses) explicitly, without using a failure-driven loop. The result of the analysis of the different paths is obtained by taking the least upper bound of the results obtained from every individual path—i.e. the value of the studied property for a predicate is obtained by taking the ‘upper bound’ among the values obtained from the different clauses defining the predicate. In the Ms system the explicit iteration over the different clauses defining a predicate requires a considerably complex mechanism. 7.2. NON-WELL-FOUNDED SETS 229 The same process can be described in a one-line {log} clause using intensional sets: p$pred(InMode,OutMode)← lub({Out | p$cl(I, InMode,Out) ∧ 1 ≤ I ≤ m},OutMode). where I is the index of the considered clause, sfm is the number of clauses defining p, InMode is the input value for the considered property (e.g., the set of modes previously computed), and OutMode will be instantiated to the output value for the considered property. Considering that the description of the property is extracted from the source program itself, and as such it can contain variables, the collection of the intensional set in the p$pred clause requires the use of constructive negation (i.e., it does not belong to the cases covered by the use of negation as failure). 7.2 Non-well-founded sets One of the most common exploitations of hypersets is as a means to model deterministic finite state automata (cf., e.g., [14]). As we will now see, the hyperset universe and unification algorithms are sufficiently powerful to offer algorithmic support to such modeling task. A deterministic finite automaton (DFA for short) consists of a set Q = {Q0, . . . , Qn} of states, a set S = {s1, . . . , sk} of symbols, and a transition function d : Q×S → Q∪{⊥}. One of the states—say Q0—is called initial state, and there is a set F ⊆ Q of accepting states (for a complete definition of DFAs see, for instance, [52]). Given a DFA A, one may define a corresponding Herbrand system E in the signature Σ = {∅, {· | ·},⊥, δ, δ′}, where ⊥ is a constant symbol and δ, δ′ are functional symbols of arity k, as follows: E = A . = {Q0, . . . , Qn}∧ ∧ Qi in Q\F Qi . = δ(d(Qi, s1), . . . , d(Qi, sk))∧ ∧ Qi in F Qi . = δ(d(Qi, s1), . . . , d(Qi, sk)) 230 CHAPTER 7. PROGRAMMING . . . WITH SETS This can easily be re-expressed as an equivalent flat system, or, if one prefers, as a graph bearing the same information. Other techniques to simulate DFAs by hypersets have been proposed in the literature. For example, in [14], one such technique is presented, and it is shown that the notion of bisimulability between graphs ≈ (cf. Def. 3.24) corresponds exactly to equivalence between automata. Given two DFAs A and B, it is easy to determine whether or not they accept the same language, as is shown by the following simple example. Consider the two DFAs q0 q1 q2 q′ 0 q′ 1 b b a b ? a