Stratification

[julianhyde]

Ensure that Morel has analogous behavior to Datalog in the presence of negation.

Consider the following invalid Souffle (Datalog) program:

.decl edge(from: symbol, to: symbol)
.decl blocked(from: symbol, to: symbol)
.decl reachable(from: symbol, to: symbol)

edge("a", "b").
edge("b", "c").
edge("c", "a").  // Cycle in graph

// Edge is blocked if it's part of a reachable cycle
blocked(X, Y) :- edge(X, Y), reachable(X, X).

// Reachable, but not through blocked edges
reachable(X, Y) :- edge(X, Y), !blocked(X, Y).
reachable(X, Z) :- reachable(X, Y), edge(Y, Z), !blocked(Y, Z).

Souffle gives a compile-time error "Strongly connected component { p, q } is not stratified" because:

• blocked depends on reachable
• reachable depends on !blocked (negatively)

So there is a cycle: reachable → blocked → (neg) reachable

You can make the program valid by ensuring negation only references lower strata:

.decl edge(from: symbol, to: symbol)
.decl blocked_edge(from: symbol, to: symbol)  // Stratum 0 (base facts)
.decl reachable(from: symbol, to: symbol)     // Stratum 1

edge("a", "b").
edge("b", "c").
edge("c", "a").

// Manually specify blocked edges (no dependency on reachable)
blocked_edge("c", "a").  // Block the cycle-closing edge

// Reachable, avoiding blocked edges
reachable(X, Y) :- edge(X, Y), !blocked_edge(X, Y).
reachable(X, Z) :- reachable(X, Y), edge(Y, Z), !blocked_edge(Y, Z).

.output reachable

Alternatively, use two-Phase Computation.

// Phase 1 (Stratum 0): Compute all paths
.decl edge(from: symbol, to: symbol)
.decl path(from: symbol, to: symbol)

edge("a", "b").
edge("b", "c").

path(X, Y) :- edge(X, Y).
path(X, Z) :- path(X, Y), edge(Y, Z).

// Phase 2 (Stratum 1): Use negation on computed paths
.decl unreachable(from: symbol, to: symbol)
.decl node(n: symbol)

node(X) :- edge(X, _).
node(Y) :- edge(_, Y).

unreachable(X, Y) :- node(X), node(Y), X != Y, !path(X, Y).

.output unreachable

Morel behavior could be like this:

(* reachable_blocked.mor *)

(* Base data *)
val edge = [
  {from = "a", to = "b"},
  {from = "b", to = "c"},
  {from = "c", to = "a"}
]

(* INVALID: Circular dependency through negation *)
val reachable =
  (from e in edge
   where not (exists b in blocked where b = e))
  union
  (from r in reachable, e in edge
   where r.to = e.from andalso
         not (exists b in blocked where b = e)
   select {r.from, e.to})

val blocked =
  from e in edge
  where (exists r in reachable 
                where r.from = e.to andalso r.to = e.to)

gives the following compiler error:

Error: Cycle through negation detected

Inferred stratification:
  edge: stratum 0
  reachable: stratum ? (depends on ¬blocked)
  blocked: stratum ? (depends on reachable)

Cycle:
  reachable --[negation]--> blocked --[positive]--> reachable

This program cannot be stratified.

Suggestion: Compute in phases or make 'blocked' base data.

However, I'm not convinced that a Morel user would expect the compiler to detect cycles.