don't allow negation without a corresponding positive occurrence

BrianHicks · Dec 16, 2020 · 0fa9bec · 0fa9bec
1 parent 6ad133a
commit 0fa9bec
Show file tree

Hide file tree

Showing 4 changed files with 61 additions and 2 deletions.
diff --git a/src/Datalog/Parser.elm b/src/Datalog/Parser.elm
@@ -210,6 +210,9 @@ niceProblem problem =
         InvalidRule Rule.UnnamedHeadVariable ->
             "a rule, which may not use anonymous variables in the head"
 
+        InvalidRule Rule.VariableAppearsNegatedButNotPositive ->
+            "a rule, which may not contain atoms that appear in a negated expression without appearing in a positive one"
+
         InvalidProgram Datalog.CycleWithNegation ->
             -- TODO: wow, awkward way to phase this. Make it better!
             "a program, which may not contain cycles including negation"

diff --git a/src/Datalog/Rule.elm b/src/Datalog/Rule.elm
@@ -3,6 +3,7 @@ module Datalog.Rule exposing (Problem(..), Rule, body, fact, head, isFact, rule,
 import Datalog.Atom as Atom exposing (Atom)
 import Datalog.Negatable as Negatable exposing (Direction(..), Negatable(..))
 import Datalog.Term as Term
+import Sort.Set as Set
 
 
 type Rule
@@ -12,6 +13,7 @@ type Rule
 type Problem
     = NotRangeRestricted
     | UnnamedHeadVariable
+    | VariableAppearsNegatedButNotPositive
 
 
 rule : Atom -> List (Negatable Atom) -> Result Problem Rule
@@ -26,6 +28,9 @@ rule head_ body_ =
     else if not (isRangeRestricted candidate) then
         Err NotRangeRestricted
 
+    else if not (isNegationSafe candidate) then
+        Err VariableAppearsNegatedButNotPositive
+
     else
         Ok candidate
 
@@ -58,6 +63,36 @@ isRangeRestricted (Rule head_ body_) =
         (Atom.variables head_)
 
 
+{-| Do all the variables in negated expressions also appear in positive
+expressions?
+-}
+isNegationSafe : Rule -> Bool
+isNegationSafe (Rule _ body_) =
+    body_
+        |> List.foldl
+            (\(Negatable direction atom) occurrences_ ->
+                List.foldl
+                    (\variable occurrences ->
+                        case direction of
+                            Positive ->
+                                { occurrences | positive = Set.insert variable occurrences.positive }
+
+                            Negative ->
+                                { occurrences | negative = Set.insert variable occurrences.negative }
+                    )
+                    occurrences_
+                    (Atom.variables atom)
+            )
+            { positive = Set.empty Term.variableSorter
+            , negative = Set.empty Term.variableSorter
+            }
+        |> (\{ positive, negative } ->
+                negative
+                    |> Set.dropIf (Set.memberOf positive)
+                    |> Set.isEmpty
+           )
+
+
 head : Rule -> Atom
 head (Rule head_ _) =
     head_

diff --git a/tests/Datalog/RuleTests.elm b/tests/Datalog/RuleTests.elm
@@ -29,6 +29,21 @@ ruleTest =
                     (atom "mortal" [ anonymous ])
                     [ positive (atom "greek" [ anonymous ]) ]
                     |> Expect.equal (Err UnnamedHeadVariable)
+        , test "negative terms are allowed if they also appear in a positive form" <|
+            \_ ->
+                rule
+                    (atom "unreachable" [ variable "a", variable "b" ])
+                    [ positive (atom "node" [ variable "a" ])
+                    , positive (atom "node" [ variable "b" ])
+                    , negative (atom "reachable" [ variable "a", variable "b" ])
+                    ]
+                    |> Expect.ok
+        , test "negative terms are not allowed if they don't also appear in a positive form" <|
+            \_ ->
+                rule
+                    (atom "immortal" [ variable "whom" ])
+                    [ negative (atom "mortal" [ variable "whom" ]) ]
+                    |> Expect.equal (Err VariableAppearsNegatedButNotPositive)
         ]
 
 

diff --git a/tests/DatalogTests.elm b/tests/DatalogTests.elm
@@ -166,8 +166,14 @@ solveTest =
                             ]
             , test "does not stratify an unstratifiable program" <|
                 \_ ->
-                    [ Rule.rule (atom "p" [ variable "x" ]) [ negative (atom "q" [ variable "x" ]) ]
-                    , Rule.rule (atom "q" [ variable "x" ]) [ negative (atom "p" [ variable "x" ]) ]
+                    [ Rule.rule (atom "p" [ variable "x" ])
+                        [ positive (atom "exists" [ variable "x" ])
+                        , negative (atom "q" [ variable "x" ])
+                        ]
+                    , Rule.rule (atom "q" [ variable "x" ])
+                        [ positive (atom "exists" [ variable "x" ])
+                        , negative (atom "p" [ variable "x" ])
+                        ]
                     ]
                         |> List.map
                             (\ruleOrErr ->