Negation Bug?

[cwarden]

This program results in an unexpected derived fact of implicitDep(2, 1).

Decl task(TaskId, UserTaskIndex)
   bound [/any, /number].

Decl directDep(TaskId, DependsOn).
Decl transDep(TaskId, DependsOn).
Decl implicitDep(TaskId, DependsOn).

transDep(Task, DependsOn) :- directDep(Task, DependsOn).
transDep(Task, DependsOn) :- directDep(Task, Z), transDep(Z, DependsOn).

# Implicit dependency on the previous task for this user
implicitDep(Task, DependsOn) :- task(Task, Later),
   task(DependsOn, Earlier),
   !directDep(DependsOn, _),
   !transDep(DependsOn, Task),
   Later > Earlier.

task(1, 1).
task(2, 2).
task(3, 3).
task(4, 4).
directDep(1, 4).

$ mg -load planner/datalog/dependencies-bug.mg -exec implicitDep
loaded planner/datalog/dependencies-bug.mg.
implicitDep(2,1)
implicitDep(3,1)
implicitDep(3,2)
implicitDep(4,2)
implicitDep(4,3)
#PASS

The clause, !directDep(DependsOn, _) should prevent the implicitDep(2,1) fact from being created since the fact directDep(1, 4) exists.

The equivalent souffle program results in the expected output:

.decl task(TaskId: symbol, UserTaskIndex: number)
.decl directDep(TaskId: symbol, DependsOn: symbol)
.decl transDep(TaskId: symbol, DependsOn: symbol)
.decl implicitDep(TaskId: symbol, DependsOn: symbol)

transDep(Task, DependsOn) :- directDep(Task, DependsOn).
transDep(Task, DependsOn) :-
    directDep(Task, Z),
    transDep(Z, DependsOn).

implicitDep(Task, DependsOn) :-
    task(Task, Later),
    task(DependsOn, Earlier),
    !directDep(DependsOn, _),
    !transDep(DependsOn, Task),
    Later > Earlier.

task("1", 1).
task("2", 2).
task("3", 3).
task("4", 4).
directDep("1", "4").

.output implicitDep (IO=stdout)

$ souffle planner/datalog/dependencies.dl
---------------
implicitDep
===============
4       2
4       3
3       2
===============

[cwarden]

Adding another relation to replace !directDep(DependsOn, _) works:

hasDirectDep(Task) :- directDep(Task, _).

# Implicit dependency on the previous task for this user
implicitDep(Task, DependsOn) :- task(Task, Later),
   task(DependsOn, Earlier),
   !hasDirectDep(DependsOn),
   !transDep(DependsOn, Task),
   Later > Earlier.

[burakemir]

It is not a bug, but a frequent pitfall.

The meaning of ... !directDep(DependsOn, Z) ... for fresh Z on the right-hand side is
"there exists a Z such that not(directDep(DependsOn, Z))"

What you want seems to be "not (there exists Z such directDep(DependsOn, Z))"

Adding a separate relation is necessary. The canonical example for this pitfall (from https://cse.buffalo.edu/~chomicki/636/a1.pdf pp.17) is

bachelor(X) :- man(X), !married(X,Y).   # Wrong!

It should instead be:

bachelor(X) :- man(X), !has_spouse(X).
has_spouse(X) :- married(X, Y).

Now, I recognize that this is a debatable convention, and one very frequently wants "!exists[table(Bound, _)]". It is possible that souffle interprets negation that way, I couldn't find much documentation about this at a quick glance.

I find it better to stick the logical reading, but I have been thinking about making this use case more convenient through custom synax, for example: !exists[implicitDep(Bound, _)] or !exists Z [implicitDep(Bound, Z)].

The implementation would then automatically create that auxiliary predicate tmp(Bound...) with that right hand side, and replace the !exists(...) with !tmp(Bound).

[cwarden]

Interesting. I hadn't considered that the meaning was ambiguous.
I'm happy to make make my rule more explicit.

That said, it does seem peculiar that these aren't equivalent:

bachelor(X) :- man(X), !has_spouse(X).
has_spouse(X) :- married(X, _).

bachelor(X) :- man(X), !married(X, _).

It's easy for me to see how !married(X, Z) would be interpreted as "there is some Z to whom X is not married", but I'm having trouble interpretting !married(X, _) as anything other than "X is not married to anyone".

Does it require custom syntax rather than treating !married(X, _) differently than !married(X, Z)?

[burakemir]

It depends what you mean by "require".

There is already Mangle code which assumes the current semantics.
_ is uniformly treated as if one used a fresh variable. So changing the meaning could be very surprising.
It would IMHO also be very surprising to treat _ as different from spelling out a fresh variable.

If one were to start Mangle from scratch, then one could choose to interpret a negated atom that contains fresh variables differently.
It seems better to be explicit with the quantification that is happening for a negated subgoal.