LogiQL 4.x Fixpoint Semantics

This blog-post describes our current semantics for LoqiQL rules, focusing on how fixpoints are handled in the presence of negation and arithmetic. We use examples and describe the semantics operationally. As usual for declarative programs, the engine might actually choose a very different way of computing the model. In this post, I use the term Stratified Partial Fixpoint Semantics as the name of the semantics used by the LogiQL 4.x engine.

Stratified Partial Fixpoint Semantics

Let us consider a simple stratified program that computes the transitive closure of a graph as well as the complement of the transitive closure. The graph is given as input via a binary relation e containing its edges.

n(x) <- e(x,_) ; e(_,x).
tc(x,y) <- e(x,y).
tc(x,y) <- e(x,z), tc(z,y).
ntc(x,y) <- n(x), n(y), !tc(x,y).

Computing the model of this program under LogiQL’s stratified fixpoint semantics yields n containing all nodes in the graph encoded by e; tc having the transitive closure of e; and ntc being the complement of tc. As you might know, the order in which the rules of a LogiQL program are given is not significant. Yet, it makes sense to imagine some sort of order between rules. Intuitively, we would expect the system to first evaluate tc before it computes the content of ntc — even if we put the fourth rule first. This is best explained via the concept of dependencies between predicates.

Predicate Dependency Graph

For a LogiQL program, we can create its predicate-dependency graph as follows: Each predicate is a node in the graph. There is an edge from a predicate R to a predicate S if R appears in the body of a rule for which S appears in the head. For our example program from above, the predicate dependency graph is the following:

In the graph, we see that to determine n we need e as input; to compute ntc, we need both n and tc. A cycle in this graph (like tc->tc) indicates a fixpoint set: To compute tc, we need e and tc itself.

In general, we are interested in the strongly-connected components of the predicate dependency graph. Consider the following program, which computes the square root of pi via two recurrence relations:

pi[]=3.0f <- !pp[]=_.
pp[]=x <- x = pi[] + sin[pi[]].
pi[]=pp[].

sqrt_pi[]=x <- x=pi[], !new_est[]=_.
new_est[]=x <- x=(sqrt_pi[] + pi[]/sqrt_pi[]) / 2.0f.
sqrt_pi[]=new_est[].

Its predicate dependency-graph is:

A strongly-connected component of a graph is a maximal subset C of nodes such that there is a path between any two nodes in C. Our most recent example has two strongly-connected components: {pi,pp} and {sqrt_pi,new_est}. The predicate dependency graph for the earlier example (complement of transitive closure) has 4 strongly-connected components — one for each node.

Condensed Dependency Graph

LogiQL’s stratified partial fixpoint semantics will compute predicates component-wise. Consider the predicate-dependency graph in which each strongly connected component is collapsed into a single node. The so obtained condensed dependency graph constraints the order in which LogiQL computes the contents of predicates. The condensed graphs for the complement of transitive closure is:

LogiQL determines the contents of predicates by choosing a node for which all predecessor nodes have been computed. Thus, in the beginning a leaf node is considered. Our only leaf node is e, which as an EDB predicate is trivially finished. Then, either the component for n or tc is computed next. In each strongly connected component predicates that appear in the body of rules have either already been computed in a lower component; or they are part of the fixpoint predicates — that is they appear in the body as well as in the head within this component. Components that do not have fixpoint-predicates are computed by simply executing the rules defining the predicates of the component. E.g., n is computed via n(x) <- e(x,_) ; e(_,x).

Fixpoint Components

In components with fixpoint predicates, we apply a partial-fixpoint semantics. Roughly speaking, this means we iterate the rules of the component until we reach a fixpoint. Let us consider our transitive closure example. The second and third rules define tc. Specifically, these rules describe how to compute a new tc’, given predicates tc and e:

tc'(x,y) <- e(x,y).
tc'(x,y) <- e(x,z), tc(z,y).

Since e is fixed, we can view the rules of a fixpoint component as a specification F of how to compute the new predicate tc’ for a given tc. We start with computing F1 = F(ø), i.e., we initialize tc to be empty. We then iterate; that is we compute F2 = F(F(ø)), F3 = F(F2), and so on until we reach a point in which F{i+1}=F{i}, e.g., the computed tc’ agrees with the previously computed tc’.

The semantics we use to compute single components is known as partial fixpoint semantics. It is partial since the fixpoint does not always exist:

Diverging Cases

Consider the following simple example:

p(1) <- !p(1).

Starting with p empty, in the next iteration p contains 1. In the next iteration, p would be empty again since the rule would fail to produce p(1), causing an endless loop switching back and forth between these two states infinitely. The LogiQL execution engine will ultimately detect cases in which an earlier state is reproduced; and abort the transaction with an error message. Note that with value-invention, for example, via constructors or arithmetic, we can construct a program that does not reach a fixpoint without visiting the same state twice:

f(1). f(x+1) <- f(x).

This rule will attempt to store all positive integers in the predicate f.

Converging Cases

Luckily, the partial fixpoint semantics always reaches a fixpoint for components without value invention when negation is either not used at all (as in our tc component) or if predicates that are used with a negation have already been computed in an earlier component. This is the case in our example for the component ntc since the only negatedly used predicate tc has already been fixed in an earlier component.

For those familiar with the Stratified Semantics. One can easily see that for stratified programs the above criterion is satisfied. In fact, it is not too hard to see that our Stratified Fixpoint Semantics agrees with the Stratified Semantics for stratified programs (for the pure Datalog subset without value invention).

Even with value invention and negation we can construct programs in which the components reach fixpoints. Consider again the example that computes the square-root of Pi. Its condensed dependency graph is the following:

That is, we would first iterate the first three rules until we reach a fixpoint, then we iterate the second group of three rules. Let’s see why the first set converges:

pi[]=3.0f <- !pp[]=_.
pp[]=x <- x = pi[] + sin[pi[]].
pi[]=pp[].

Here, both pi and pp (“Pi-prime”) is computed via the fixpoint. In the first iteration pp and pi are initialized to be empty. Thus, we obtain pi=3.0. In the second iteration, we obtain pi=3.0 as well as pp=3.1411=3+sin(3). In the third iteration the first rule does not apply anymore. We obtain pp=3.1411 and pi=3.1411. In the next iteration, we obtain a new value for pp, then a new value for pi, and so on. For pi=3.1415926535897931, pp will be the same. Thus we will reach a state in which neither pi nor pp will change — a fixpoint. 

Now, the second component is computed.

sqrt_pi[]=x <- x=pi[], !new_est[]=_.
new_est[]=x <- x=(sqrt_pi[] + pi[]/sqrt_pi[]) / 2.0f.
sqrt_pi[]=new_est[].

With empty sqrt_pi and new_est, only the first rule applies, which computes the first guess for the square root of Pi as Pi itself. Then, a refinement is computed, until a fixpoint will be reached.

Relationship to Other Semantics

Note that in the database literature, the partial fixpoint semantics is generally applied to the entire program as opposed to only connected components. Not surprisingly, this yields a very different semantics. Most notably, partial fixpoint semantics does, in general, not agree with the stratified semantics whereas our stratified partial fixpoint semantics is a conservative extension of the stratified semantics.

In a follow-up post, we will relate the Stratified Partial Fixpoint Semantics to other well-known semantics such as the stratified, well-founded, and inflationary semantics.