Allow nested negation and universal quantification in rules

[james-whiteside]

Problem to Solve

TypeQL does not currently support nested negation (not { not { <pattern> }; };) in rule conditions. This makes some logical expressions impossible to construct. Taking the following rule:

rule group-maximisation-violation-detection:
    when {
        $g1 isa user-group;
        $g2 isa user-group;
        not {
            (permitted-subject: $g1, permitted-access: $a) isa permission;
            not { (subject: $g2, access: $a) isa permission; };
            not { (group: $g1, member: $s) isa group-membership; };
            (group: $g2, member: $s) isa group-membership;
        } ;
    } then {
        (group: $g1, group: $g2) isa group-maximisation-violation;
    };

and applying De Morgan's laws to cancel out the nested negation gives:

rule group-maximisation-violation-detection:
    when {
        $g1 isa user-group;
        $g2 isa user-group;
        {
            not { (permitted-subject: $g1, permitted-access: $a) isa permission; };
        } or {
            (subject: $g2, access: $a) isa permission;
        } or {
            (group: $g1, member: $s) isa group-membership;
        } or {
            not { (group: $g2, member: $s) isa group-membership; };
        };
    } then {
        (group: $g1, group: $g2) isa group-maximisation-violation;
    };

which does not achieve the same result. The second version of the rule will insert a group-maximisation-violation relation between every possible pair of groups in the database as long as at least one $a or $s exists, which is not the case for the first one. This is because applying De Morgan's laws requires proper treatment of qualifiers. Stating the first version of the rule mathematically gives:

g : user-group
a : access
s : subject
p : permission
m : group-membership
v : group-maximisation-violation

∃(g1, g2) . ( ¬∃(a, s) . ( p(g1, a) ∧ ¬p(g2, a) ∧ ¬m(g2, s) ∧ m(g1, s) ) ) → v(g1, g2)

Now applying De Morgan's laws gives:

∃(g1, g2) . ( ∀(a, s) . ( ¬p(g1, a) ∨ p(g2, a) ∨ m(g2, s) ∨ ¬m(g1, s) ) ) → v(g1, g2)

The existential qualifier ∃ is implicit in TypeQL (elegantly allowing the implicit binding of $a and $s), but as there is no universal quantifier ∀, the second version of the rule cannot be constructed. This means that, as nested negations are currently not permitted, it is impossible to create this logical expression in a single rule's conditions.

As a minimum to solve this issue, nested negations would need to be permitted, but it would be very powerful to introduce notation for universal quantification. By De Morgan's laws, universal quantification is never necessary as it can always be replaced with nested negation. This is the approach that Prolog uses, and nested negation is an encouraged design pattern in the language. While the addition of a universal quantifier would not increase TypeDB's expressivity, it would significantly improve readability and reduce rule complexity.

Current Workaround

Use multiple rules with one level of negation per rule.

Proposed Solution

Permit nested negation (short-term), and introduce a universal quantifier (long-term).

[james-whiteside]

@cxdorn

[james-whiteside]

From "Logic for Mathematicians" by A.G. Hamilton, sec. 3.2, p. 51:

We have seen that the existential quantifier can be defined in terms of the universal quantifier, so we need have only one of them.

[cxdorn]

(I realize my earlier thumbs up reaction wasn't very helpful, but I actually wasn't sure whether there was a question implied here!)

With regards to the question: can we do everything with 'exists' that we can do with 'forall'?

• Propositionally (i.e. for truth values) yes. $\forall x. \phi(x)$ and $\neg \exists x. \neg \phi(x)$ are equi-derivable in predicate logic (if you assume the axiom of excluded middle $\neg \neg \phi(x) \Rightarrow \phi(x)$, which holds in the 'negation as failure' semantics we are using).
• Type-theoretically (i.e. for data instances) no. The way we interpret an existence statement in TypeQL is as a query for all data instances of that statement. If we write $\exists (y : T). \psi(y)$ we want to find all $y$ of type $T$ with property $\psi(y)$. Similarly, a 'forall' statement can query for data instances. For instance, for the query $\forall (x : S). \{y : T; \phi(x,y) \}$ (by which I mean $\forall (x : S). \exists (y : T). \phi(x,y)$ ), if we'd really list all data instances to that statement, we would want to find all functions of data instances $f : S \to T$ such that $\phi(x, f(x))$ holds true. Whereas for the query $\neg \exists (x : S). \neg \exists (y : T). \phi(x,y)$ we'd not return any witnesses, but just a truth value, namely, whether or not the statement $\exists (x : S). \neg \exists (y : T). \phi(x,y)$ has a witness.

But function spaces are generally way too big, so I don't think we'd ever want to implement forall in a data instance sense.