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 = 3.0f. Pi[i+1] = Pi[i] + sin[Pi[i]] <- i < 5.
┌─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 = 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=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]
- It would be great to have support for cases.
- 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 🙂
- 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.
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