Fun With LogiQL 4.x Fixpoint Semantics

In LogicBlox 4.x, rules are run until they reach a fixpoint, even if negation is involved. This allows interesting formulations for various algorithms. The following show-cases some tricks involving fixpoint computations.

Fixpoints with Explicit Iteration Numbers in Logic

Let’s start with computing pi via a fixpoint relation, stopping after 6 steps:

Pi[0] = 3.0f.
Pi[i+1] = Pi[i] + sin[Pi[i]] <- i < 5.

Output:

┌─Pi
│ 0,3.0
│ 1,3.1411200080598674
│ 2,3.1415926535721956
│ 3,3.1415926535897931
│ 4,3.1415926535897931
│ 5,3.1415926535897931
└─Pi [end]

Sometimes, we would like to stop when an iteration does not change the value by more than a certain epsilon:

Pi[0] = 3.0f.
Pi[i+1]=next <- next = Pi[i] + sin[Pi[i]], abs[next-Pi[i]]>0.001f.

Or, when the result does not change anymore:

Pi[0]=3.0f.
Pi[i+1]=next <- next=Pi[i]+sin[Pi[i]], next != Pi[i].

The latter yields an output of:

┌─Pi
│ 0,3.0
│ 1,3.1411200080598674
│ 2,3.1415926535721956
│ 3,3.1415926535897931
└─Pi [end]

Fixpoints Without Explicit Iteration Numbers in Logic

If we are not interested in the steps the computation takes until it converges, we can also leave off the index value. We would make Pi a scalar predicate. Then, the runtime would perform the fixpoint iteration and stop once a fixpoint has been reached:

Pi[] = 3.0f <- !Pi[]=_.
Pi[] = Pi[] + sin[Pi[]].

This will compute Pi as:

┌─Pi
│ 3.1415926535897931
└─Pi [end]

The first line is used to initialize Pi to 3.0 if Pi is not set. The second line performs the fixpoint computation. The runtime will stop iterating once a fixpoint has been reached – that is there are no changes from one iteration to the next. It is important to reproduce the same result in two immediately following iterations. The following program does not converge:

Pi[]=3.0f <- !Pi[]=_.
Pi[]=newpi <- newpi = Pi[] + sin[Pi[]], newpi != Pi[].

Witnessed by the following error message from the runtime:

Error: Fixpoint iteration does not converge: e.g. iteration #7881 has the same s
tate as iteration #7876 (cycles in 5 steps).

What happened here? The program computes successive values of Pi until it reaches the point in which newpi = Pi. Here, no value for Pi is computed; and thus being different from the previous iteration where Pi had the correct value. In the next iteration,  the initialization rule will be applicable again, resulting into the infinite loop.

So, what do we do if we actually want to stop iterating at a certain condition? – We just need to make sure the same value is reproduced. Lets say we want to stop if our change is smaller than 0.01:

Pi[]=3.0f <- !Pi[]=_.
Pi[]=newpi <- newpi= Pi[] + sin[Pi[]], abs[newpi - Pi[]] > 0.01f.
Pi[]=Pi[] <- newpi= Pi[] + sin[Pi[]],!(abs[newpi - Pi[]] > 0.01f).

Here, the second rule will only compute a new value for Pi[] if the new and old value differ by more than 0.01f. The third rule is used to obtain a fixpoint: If the condition from the second rule is false, then set the new value of Pi to its old value. In deed, we obtain:

┌─Pi
│ 3.1411200080598674
└─Pi [end]

In future versions of logiQL, we are planning to support a cases construct. Cases allows to provide alternatives with a first-match semantics:

Pi[]=x <- cases (x)
          of x = Pi[] + sin[Pi[]], abs[x-Pi[]] > 0.01f
          else x = Pi[]
          else x = 3.0f.

Here, the first case would match only if some earlier value of Pi has already been computed, and the new value is further than 0.01f away from the previous value. That is the first clause corresponds to our iteration case. The first clause will stop being satisfiable once Pi and the next value are close enough. Then, the second clause x=Pi will set the new Pi to the old Pi, effectively causing the fixpoint. The last clause is needed to get everything started: The first two clauses only match if Pi is defined and so, at the very beginning of the computation the third clause initializes Pi to 3.0f.

Greatest Common Divisor

To compute the greatest common divisor, we can directly implement Euclid’s algorithm:

g(a,0) <- g(a,0).
g(b, int:mod[a, b]) <- g(a,b).
g(a[],b[]) <- !g(_,_).
a[]=350. b[]=5390.
gcd[]=a <- g(a,0).

The first two lines are almost verbatim from wikipedia for Euclid’s algorithm. The third line initializes g with a and b; the third line provides our sample input the last line copies the final result. When running this we obtain:

┌─gcd
│ 70
└─gcd [end]

 

LogiQL Wishlist

  1. It would be great to have support for cases.
  2. It would be great if we could omit [] for scalar predicates. Obviously, it will be harder to distinguish them from variables in the rule, but we could pick the predicate if it exists. This would then feel like variables whose value persists 🙂
  3. This is likely controversial, but I would prefer foo(x)=y for the functional syntax. One way would be to switch ( ) and [ ] around. This would make our functions look more like functions. And, tables are sorta rectangular shape — so we can have [ ] here. Another option is to allow foo(x)=y  for a functional predicate.

Remarks:

All tests require that you switch off the compiler-error for negation through recursion. A runnable version for the Pi program is as follows:

create --unique
transaction
addBlock <doc>
Pi[] = 3.0f <- !Pi[]=_.
Pi[] = Pi[] + sin[Pi[]].

lang:compiler:disableError:NEGATION_RECURSION[]=true.
lang:compiler:disableWarning:NEGATION_RECURSION[]=true.
</doc>
print --atend Pi
commit
close --destroy
14 Comments
  1. Zef Hemel 7 years ago

    Cool stuff Daniel!

  2. Nikolaos Vasiloglou 7 years ago

    Danniel

    this is really great news for expressing machine learning algorithms. I will write some examples with machine learning and send them to post. George already expressed pagerank with this new framework.

  3. George Kastrinis 7 years ago

    Great post Daniel! Are all those made possible in the new runtime, or were they supported in 3.x as well?

  4. Author
    Daniel Zinn 7 years ago

    These are only supported in 4.x. And, since we are just starting to try out this feature, there might be issues 🙂

  5. Molham Aref 7 years ago

    Nice post Daniel. This capability in the LB4 will make LogiQL so much more expressive and useful. As they say in France: chapeaux to the RT team. (I’m not worried that we will have to work out some bugs and tune performance — that’s perfectly normal and nothing to be shy about)

    My comments on your wish list:
    — It would be great to have support for cases. [MA] Agreed.

    — It would be great if we could omit [] for scalar predicates. Obviously, it will be harder to distinguish them from variables in the rule, but we could pick the predicate if it exists. This would then feel like variables whose value persists [MA] I don’t believe we will need for [] on singletons (these are not scalars) once we have a point-free syntax. The reason I am opposed to hacking around them now is that we don’t understand how our point-free notation will work and whether or not we will want to mix and match point-free and point-wise styles. I know that this is a pet peeve for several people. Please direct the evil-eye to me while we work the design out 🙂

    — This is likely controversial, but I would prefer foo(x)=y for the functional syntax. One way would be to switch ( ) and [ ] around. This would make our functions look more like functions. And, tables are sorta rectangular shape — so we can have [ ] here. Another option is to allow foo(x)=y for a functional predicate. [MA] You are right, this is controversial and I hate it :-).

  6. Author
    Daniel Zinn 7 years ago

    I also found a motivating example for why it might be good to spend a few cycles on research about a well-founded semantics inspired semantics (cf. the email I wrote a while ago).

    Unfortunately, using this method is not very robust with the current semantics. Consider:

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

    This program does not reach a fixpoint (it would with the proposed well-founded changes). To find out why it is not terminating is left as an exercise to the reader 😉

    • George Kastrinis 7 years ago

      Let me try this Daniel.

      You start with an initial value = 3.0 in f since there isn’t any previous value. This will in turn compute an initial value for Pi using the 3rd rule (3.something).

      In the next iteration there is a value for f so the 1st rule cannot apply. Only the 2nd. The second rule relies on the existence of a value for f, which has now lost its “support” from the 1st rule.

      So in this iteration you have no value computed for f, and in turn no value computed for Pi.

      In the next iteration you are in the same state as in the first one (f and Pi empty) and you will again compute the initial values, thus a cycle.

      Am I close?

      PS. What’s the “Pi[] = Pi[] + sin[Pi[]].” notation? Is it a version of a left arrow rule?

  7. Author
    Daniel Zinn 7 years ago

    That’s it George.


    Pi[] = Pi[] + sin[Pi[]].

    is syntactic sugar for:

    Pi[]=b <-
    /* a::float[64],c::float[64] */
    float64:add[c,a]=b,
    Pi[]=c,
    float64:sin[c]=a.

    You can see how logiQL desugars by putting the logic in a file and running
    bloxcompiler compileFile x.logic

    Daniel

  8. Author
    Daniel Zinn 7 years ago

    Hey George,

    there is a simple pattern we can use to deal with “next-value-computations” that take longer than 1 fixpoint iteration. The general idea is to have the initial value be provided for a fixed number n of rounds. A round counter is not that hard to implement, we just need to make sure its fixpoint is entangled with the fixpoint we want to compute.

    I wrote a sample program: https://dl.dropboxusercontent.com/u/5310859/delay_init.lb

  9. George Kastrinis 7 years ago

    I am a bit confused with the example. When would you need to spend some amount of rounds computing the same value?

    PS. What does “–atend” do?

  10. Author
    Daniel Zinn 7 years ago

    If you have a fixpoint calculation for some predicate P, and P_{n+1} is not computed from P_n in the same rule. I would expect that in any slightly realistic/complex example this can occur. The trick is to keep the initialization value until the first value is computed.

    When we support the cases construct, this should not be necessary anymore since the cases construct would do exactly what we need: it uses the initialization value until the first value has been computed; and in iterations in which a successive value is computed, it keeps the previous value persistent.

    –atend directs dlbatch to print the content of the relations at the end of a transaction.

  11. George Kastrinis 7 years ago

    Hey Daniel,

    In the examples that I tried, I often needed to write rules of the following form (because there is also some other rule with negation):

    distance(n, d) <- distance(n, d).

    Is there a way, maybe with the "cases" feature you suggest, to skip writing manually this type of rules (would you call them frame rules?)?

  12. Ghassen Louhaichi 7 years ago

    Hey Daniel,

    Is there a way that we could iterate in a parameterized way? So instead of having Pi[] we would have something like F[param] and we could iterate on that.

    If this is possible without any violation we could just easily implement mathematical functions like “arcsin” or “arccos”.

  13. Author
    Daniel Zinn 7 years ago

    Hi Ghassen,

    you can have predicates taking part in fixpoint computations that are not scalars, e.g. f[x]=y, if this is what you mean.

    You can likely implement mathematical functions like arcsin or arccos – but you really want to use built-ins for these mostly for performance reasons.

    Cheers,
    Daniel

Leave a reply

© Copyright 2020. Infor. All rights reserved.

Log in with your credentials

Forgot your details?