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.

Great post! This clears up some questions that I’ve wondering about since the “Fun With LogiQL 4.x Fixpoint Semantics” post. I’m still having some trouble coming up with an example where stratified partial fixedpoint semantics differ from (what I think is) partial fixedpoint semantics.

Looking forward to the next post!