Stratifiability

A predicate P depends on a predicate Q if some atom A in a rule of P refers to Q.

If that atom is negated, P negatively depends on Q, otherwise it positively depends on Q.

A stratification assigns a natural number L_P (the level of P) to every predicate P such that

1. No P depends on a Q at a higher level, i.e., L_P < L_Q
2. No P negatively depends on a Q at the same level, i.e., L_P = L_Q

If a program has (at least) one stratification (“stratifiable”), it has a least fixed point.

Datamog checks whether there is a stratification:

• If there is, it applies naive evaluation to each group of predicates with the same level, starting from the lowest
• If there is not, the program is rejected