Support negated conjunctions using new variable bindings

[mrrodriguez]

On the Clojurians #clara Slack channel user enn reported an session compilation error that didn't make sense in something like the following

Example 1:

(mk-session
 [(dsl/parse-query []
                   [[:not [:and
                           [:x (= ?z (:z this))]
                           [:y (= ?z (:z this))]]]])])

;;;; With error:
ExceptionInfo Using variable that is not previously bound. This can happen when an expression uses a previously unbound variable, or if a variable is referenced in a nested part of a parent expression, such as (or (= ?my-expression my-field) ...). 
Note that variables used in negations are not bound for subsequent
                                    rules since the negation can never match.
Production: 
{:lhs [[:not [:and {:type :x, :constraints [(= ?z (:z this))]} {:type :y, :constraints [(= ?z (:z this))]}]]], :params #{}}
Unbound variables: #{?z}  clojure.core/ex-info (core.clj:4593)

On the surface it seemed that this was somehow due to the "negated conjuction" handling done within the compiler, however, the issue is a bit more shallow than that.

Consider this

Example 2:

(mk-session
 [(dsl/parse-query []
                   [[:not [:x (= ?z (:z this))]]])])

This has the same exception in the compilation about the variable ?z being "unbound".

Contrast that with

Example 3:

(mk-session
 [(dsl/parse-query []
                   [[:y ( = ?z (:z this))]
                    [:not [:x (= ?z (:z this))]]])])

This compiles successfully since ?z is bound in a condition before the negated condition.

---

I haven't looked closely at the compiler to identify the specific place that relates to this issue, but I think the general idea is that the compiler does not support negated conditions that introduce new variable bindings within a LHS.

In a case like (Example 2) [:not [:x (= ?z (:z this))]] it doesn't really make a lot of sense to introduce a new variable binding since it cannot be made visible outside of the :not - because negation means "no match" of course.

However, in the case of a negated conjunction it can make sense to want to join multiple conditions together when performing the negated conjuctive condition. This can be seen in my first example here.

I think the behavior of Example 1 is surprising to find that it doesn't work.

[rbrush]

I suspect the compiler check for the non-sensical condition of a binding within a single negation is being overly sensitive and catching something that it shouldn't. I agree that I'd expect at least the first example to work, and can't think of any structural reason why it isn't doable.

[WilliamParker]

Agreed that something like

[[:not [:and
         [:x (= ?z (:z this))]
          [:y (= ?z (:z this))]]]])])

ought to work. I wonder if this is actually a functional issue or just an error detection issue.

More broadly, I think some thought and reflection on how we handle complex negations is in order. #343 and #304 are other outstanding issues in this area.

[WilliamParker]

It looks like to-dnf is the culprit here.

clara.test-rules> (com/to-dnf [:not [:and {:type :x, :constraints '[(= ?z (:z this))]} 
                                     {:type :y, :constraints '[(= ?z (:z this))]}]])
(:or [:not {:type :x, :constraints [(= ?z (:z this))]}] [:not {:type :y, :constraints [(= ?z (:z this))]}])

The not-and is turned into an or of not conditions; see to-dnf's implementation of this. However, the laws of Boolean algebra don't actually fully apply here since the meaning of each of the terms A and B in [:not [:and [A] [B]]] is dependent on the other term.

[rbrush]

I'd expect the extract-negation transformation (which runs before the conversion to DNF) to pull this out into a separate rule that can handle this flow and inserts a NegationResult. So I wonder if we can tweak the logic in in extract-negation to catch this as well.

[mrrodriguez]

@rbrush @WilliamParker
I'm revising what I said here. I was thinking along the wrong track. Luckily, the discussion on #373 made me realize this.

It does look like analysis happening prior to extraction is an issue. The sorting of conditions is another topic that can factor in, but that's what the other issue is for.

Sorry for my confusion causing any more confusion here. :P