Stratified Negation

As an example of stratified negation, consider the situation in which we have a set of terms and a nondeterministic reduction operation over them. Then given a term, we want to reduce it until further operations don't simplify it any more. We will allow there to be cycles in the reduction operation and assume that terms that reduce to each other are equivalently fully reduced.

This situation can be abstractly modeled by considering the terms to be nodes of a directed graph with an edge from N1 to N2 if the term at N1 directly reduces to the term at N2. Now consider the strongly connected components (SCCs) of this graph, i.e. two nodes are in the same SCC if each can be reached from the other. We will call an SCC a final SCC if the only nodes reachable from nodes in that SCC are others in that SCC. Now given a node, we want to find all nodes reachable from that node that are in final SCCs.

So first we define reachable:

:- table reachable/2.
reachable(X,Y) :- reduce(X,Y).
reachable(X,Y) :- reachable(X,Z), reduce(Z,Y).

Next we can define reducible to be true of nodes that can be further reduced, i.e., those nodes from which we can reach other nodes that cannot reach back:

reducible(X) :- reachable(X,Y), tnot(reachable(Y,X)).

tnot is the negation operator for tabled goals. It checks to see that the call doesn't flounder, giving an error message if it does. It can be applied only to a single goal, and that goal must be a tabled predicate. With this predicate we can next define the predicate fullyReduce that is true of pairs of nodes such that the first can be reduced to the second and the second is not further reducible:

:- table reducible/1.
fullyReduce(X,Y) :- reachable(X,Y),tnot(reducible(Y)).

Note that we must table reducible because tnot can only be applied to predicates that are tabled.

So with these definitions and the following graph for reduce:

reduce(a,b).
reduce(b,c).
reduce(c,d).
reduce(d,e).
reduce(e,c).
reduce(a,f).
reduce(f,g).
reduce(g,f).
reduce(g,k).
reduce(f,h).
reduce(h,i).
reduce(i,h).

we can ask queries such as:

| ?- fullyReduce(a,X).

X = c;

X = h;

X = d;

X = k;

X = i;

X = e;

no
| ?-

which returns all nodes in final SCCs reachable from node a.

However, we may now wish to generate just one representative from each final SCC, say the smallest. We can do that with the following program:

fullyReduceRep(X,Y) :- fullyReduce(X,Y), tnot(smallerequiv(Y)).

smallerequiv(X) :- reachable(X,Y), Y@<X, reachable(Y,X).

Now we get:

| ?- fullyReduceRep(a,X).

X = c;

X = h;

X = k;

no
| ?-

Note that this is an example of a stratified program. The predicate reachable is in the lowest stratum; then reducible is defined in terms of the negation of reachable so it is in the next stratum; then fullyReduce is defined in terms of the negation of reducible, so it is in the third stratum. smallerequiv is in the first stratum with reachable; and fullyReduceRep is in the same stratum as fullyReduce.

*********************************

Issues of safety.