Question about inlining ?

[rhendrix42]

Hi, Consider the following datalog file

datalog 1

.decl Jkc(U:float, V:float, W:float, X:float)
.input Jkc

.decl klG(U:float, V:float) inline
klG(oTZ^s,Vds-2) :- Jkc(Vds,s,oTZ,Vds), Vds <= Vds, oTZ <= s, oTZ < Vds.

.decl Vne(U:float, V:float)
Vne(a,b) :- klG(a,b), klG(a,c).

.output Vne

If i modify Vne(a,b) :- klG(a,b), klG(a,c). to Vne(a,b) :- klG(a,b). to get a new data log file

datalog 2

.decl Jkc(U:float, V:float, W:float, X:float)
.input Jkc

.decl klG(U:float, V:float) inline
klG(oTZ^s,Vds-2) :- Jkc(Vds,s,oTZ,Vds), Vds <= Vds, oTZ <= s, oTZ < Vds.

.decl Vne(U:float, V:float)
Vne(a,b) :- klG(a,b).

.output Vne

I would expect that the result would not change since Vne(a,b) :- klG(a,b), klG(a,c). should be equivalent to Vne(a,b) :- klG(a,b)..

But it get -nan 8.24 for datalog 2 and an empty result for datalog 1.

If i remove inline from the klG clause, i get the same result for both files. Is this expected ? I would assume that inlining should not change the computation what am I doing wrong ?

Jkc.facts

I am using the commit : a9ac3cbf2aad1b3bf8dfd335192e7a9328ec4b4d

[b-scholz]

You can double-check the generated Datalog code of souffle using the flag --show=transformed-datalog.

Inlining is a pure syntactical process.

The first Datalog program is transformed into

.decl Jkc(U:float, V:float, W:float, X:float) 
.decl Vne(U:float, V:float) 
Vne((<inlined_oTZ_1>^<inlined_s_1>),(<inlined_Vds_0>-2)) :- 
   Jkc(<inlined_Vds_0>,<inlined_s_0>,<inlined_oTZ_0>,<inlined_Vds_0>),
   <inlined_Vds_0> <= <inlined_Vds_0>,
   <inlined_oTZ_0> <= <inlined_s_0>,
   <inlined_oTZ_0> < <inlined_Vds_0>,
   (<inlined_oTZ_0>^<inlined_s_0>) = (<inlined_oTZ_1>^<inlined_s_1>),
   Jkc(<inlined_Vds_1>,<inlined_s_1>,<inlined_oTZ_1>,<inlined_Vds_1>),
   <inlined_Vds_1> <= <inlined_Vds_1>,
   <inlined_oTZ_1> <= <inlined_s_1>,
   <inlined_oTZ_1> < <inlined_Vds_1>.
.input Jkc

.output Vne

The second Datalog program is transformed into

.decl Jkc(U:float, V:float, W:float, X:float) 
.decl Vne(U:float, V:float) 
Vne((<inlined_oTZ_0>^<inlined_s_0>),(<inlined_Vds_0>-2)) :- 
   Jkc(<inlined_Vds_0>,<inlined_s_0>,<inlined_oTZ_0>,<inlined_Vds_0>),
   <inlined_Vds_0> <= <inlined_Vds_0>,
   <inlined_oTZ_0> <= <inlined_s_0>,
   <inlined_oTZ_0> < <inlined_Vds_0>.
.input Jkc

.output Vne

[rhendrix42]

But inlining should not change the results, right ? Running datalog1 with and without inlining gives different results

[b-scholz]

Note that operations on floating-point numbers do not follow always maths laws because they are an approximation of real numbers.

I have not checked in detail but the issue is most likely the constraint (<inlined_oTZ_0>^<inlined_s_0>) = (<inlined_oTZ_1>^<inlined_s_1>)
in the expanded version versus a simple equivalence (based on bits) in the join.

[b-scholz]

Basically, you would need eps-environments for checking equivalences, e.g., a == b <=> |a-b| < eps where eps is a constant depending on your needs.

In the case of recursive procedures, you would need to look carefully into the numerical stability of your fixpoint as well.

For example, instead of writing

.decl A,B(x:number, y:number) 
A(x,z) :- B(x,y), B(y,z). 

it is more stable to write

A(x,z) :- B(x,y1), B(y2,z), |y1-y2| < 1e-12. 

which reminds me that we don't have an fabs functor at the moment.

[rhendrix42]

oh I see ! Alright that's very helpful! Thanks :)

[rhendrix42]

Hi @b-scholz , After looking into this some more, I am wondering if this issue is related to issue #1467 . I have a similar example here where we inline the relation B.

.decl A(U:float, V:float)
.decl B(U:float, V:float) inline  // VS no inline
.decl O(U:float)
.output O

A(-5.431, -12.744).

B(w^(x^y),x^y) :- A(x,y), A(z,w).
O(m) :- B(m,m).

Without inlining i get -nan and with linlining I get an empty result.

Transformed datalog without inlining:

A(-5.431,-12.744).

B((w**(x**y)),(x**y)) :- 
   A(x,y),
   A(_,w).

O(m) :- 
   B(m,m).

Transformed datalog with inlining:

A(-5.431,-12.744).

O((<inlined_x_0>**<inlined_y_0>)) :- 
   A(<inlined_x_0>,<inlined_y_0>),
   A(_,<inlined_w_0>),
   (<inlined_w_0>**(<inlined_x_0>**<inlined_y_0>)) = (<inlined_x_0>**<inlined_y_0>).

In issue # 1467 , there is an explicit equality in the program whereas here the equality seems to be introduced by inlining. Could it be that by fixing issue 1467 by not resolving aliases on floats (as suggested by @mmcgr in this comment) this issue would be resolved as well?