Equality-generating dependencies

Equality-generating dependencies (EGD) are an advanced feature that allows to embed constraints to be satisfied within a program.

More specifically, EGDs allow us to unify values that are bound to the variables at runtime. The variables to be equated appear in a pseudo-head (called equality atom), whereas the conditions are expressed in the body.

In general, an EGD has the form: X=Y :- body

Suppose we have X and Y in the head of an EGD as the example above then we have three different scenarios depending on what value X and Y are bound to at runtime.

  • If X (resp. Y) is bound to a marked null and Y (resp. X) is bound to a constant, the value of X (resp. Y) will be replaced by the value of Y (resp. X), in other words, X becomes a constant value

  • If X (resp. Y) is bound to a marked null and Y (resp. X) is bound to another marked null, the both values are replaced by the same marked null

  • If X (resp. Y) is bound to a constant and Y (resp. X) is bound to another constant, we throw a unifying failure, meaning that the reasoning process has failed

Let us show uses of EGDs with some examples.

Example 1
edge(1,2).
edge(2,1).
edge(1,3).
conn(X,Y,Z):- edge(X,Y).
conn(Y,X,Z):- edge(X,Y).
Z1=Z2 :- conn(X,Y,Z1),conn(Y,Z,Z2).
@output("conn").
Expected result
conn(1,2,z1)
conn(2,1,z1)
conn(1,3,z1)
conn(1,2,z1)
conn(2,1,z1)
conn(3,1,z1)
Example 2
edge(1,2).
edge(2,1).
edge(1,3).
conn(X,Y,Z):- edge(X,Y).
Z1=Z2 :- conn(X,Y,Z1),conn(Y,Z,Z2).
Z1=Z2 :- conn(X,Y,Z1),conn(X,Z,Z2).
Z1=Z2 :- conn(X,Y,Z1),conn(Z,Y,Z2).
Z1=Z2 :- conn(X,Y,Z1),conn(Z,X,Z2).
@output("conn").

The programs in the example above find the edges of the same connected component in an undirected graph. The first two TGDs label each edge with a different marked null, then the EGDs unify the marked null of the edges that share a node. The output will be:

Expected result
conn(1,2,z1), conn(2,1,z1) and conn(1,3,z1).

Harmless EGDs

VadaEngine supports reasoning with EGDs under some constraints. We say that a set of EGDs is harmless if for every TGD in the program the following conditions hold: - every variable that appears in a tainted position appears only once in the body - there are no constants in tainted positions

Where a position is tainted if:

  • the program contains an EGD where a variable X appears in the position in the body, X is harmful and appears in an equality atom in the head

  • pos is the position of the variable X in the head and X appears in a tainted position in the body (forward propagation)

  • pos is the position of the variable X in the body and X appears in a tainted position in the head (backward propagation)

These constrains are checked by VadaEngine before the reasoning starts, if they are not satified an exception will be thrown.

T-Isomorphism Termination Strategy

When reasoning with EGDs t-isomorphism termination strategy is automatically enabled to guarantee the reasoning process correctness. This allows to have t-isomorphic facts in the output.

Equality Structures

When reasoning with EGDs the unifications learned at runtime are store within a shared memory structure which we call "Equality Structure". The system supports two kind of structure.

  • Equality graph (default) : the equalites are stored in a graph-like data structure which is efficient even when very large clusters are discovered.

  • Equality Hash Table : the equalites are stored in a hash table data which is efficient when there are many clusters but its performance degrades when the sizes of the clusters become very large.