Logical negation

Besides conjunctions of multiple rule clauses (logical AND) and disjunctions of multiple rules with the same name (logical OR), Eclair also supports negation in rules (logical NOT). This makes it possible to write queries where you can search if a certain fact is not found.

Here’s an example that uses negation to find all recipes that are safe for people who are lactose intolerant (can’t contain any dairy products):

@def dairy_product(ingredient: string).
@def recipe_ingredients(recipe: string, ingredient: string).
@def lactose_safe_recipe(recipe: string).

lactose_safe_recipe(recipe) :-
  recipe_ingredients(recipe, ingredient),
  !dairy_product(ingredient).

Restrictions

Negated rule clauses comes with a few restrictions, to guarantee that the program is valid and will terminate. These are mostly related to the way programs are evaluated.

A first limitation is that negated rule clauses do not ground any of their arguments. This is due to how variables are initialized in the final executable code generated by the compiler: if a variable is ungrounded, it could potentially take on infinitely many values, which is not allowed in Datalog. The fix for ungrounded variables is easy though: ground the variable in another rule clause:

@def a(u32) output.
@def b(u32) input.
@def c(u32) input.
@def d(u32) input.

// This rule will not compile:
a(x, y) :-
  b(x),
  !c(y). // <-- y is not grounded

// This will:
a(x, y) :-
  b(x),
  d(y),  // <-- d grounds y, fixing the error
  !c(y).

NOTE: Wildcards are allowed in negated rule clauses (since they do not need to be grounded).

A second restriction regarding negation is that you can’t create “cyclic negations” in rules. Cyclic negations can occur both for the case for rules with direct cycles, and for multiple mutually recursive rules that contain cycles referring to negated rule clauses.

An example of a direct cyclic negation is the following:

a(x) :-
  // ...
  !a(x).

It is not possible to evaluate the above code because to evaluate a, we would already need to know all results of a. (In other words, it is not possible to stratisfy this program.)

An example of mutually recursive rules that contain cyclic negation can be found below:

a(x) :-
  !b(x).

b(x) :-
  !a(x).

The problem with the previous example is that to evaluate a, we would need to have fully evaluated b, and b can’t be computed until all results for a have been calculated. This is again not a stratisfiable program.