<< Back to previous view

[LOGIC-172] nafc doesn't work with more complex goals Created: 31/Jul/15  Updated: 31/Jul/15

Status: Open
Project: core.logic
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Defect Priority: Major
Reporter: Tassilo Horn Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: bug
Environment:

core.logic 0.8.10, clojure 1.7.0



 Description   

The negation as failure constraint nafc is supposed to succeed if and only if the goal provided by a relation and its args fails. The test cases just cover very simple cases like (nafc == q 'b) which is essentially equivalent to (!= q 'b) (at least to my understanding). But with a slightly more complex case, it doesn't seem to work anymore.

Example:

(run* [q]
  (fresh [a b]
    (== q (list a b))
    (fd/in a b (fd/interval 1 3)) ;; fd is an alias for clojure.core.logic.fd
    (fd/< a b)
    (nafc membero 2 q)))
;=> ((1 2) (2 3) (1 3))

The constraint specifies that the number 2 must NOT be contained in the list q but still it is. I expected to get the single answer (1 3) here.



 Comments   
Comment by Tassilo Horn [ 31/Jul/15 2:40 AM ]

It seems that this problem could be specific to clojure.core.logic.fd. At least this example works:

(defn answero [x]
  (conde
   [(== x :yes)]
   [(== x :no)]
   [(== x :maybe)]
   [(== x :dont-know)]))

(run* [q]
  (fresh [a b]
    (== q (list a b))
    (everyg answero q)
    (nafc membero :maybe q)
    (nafc membero :dont-know q)))
;=> ((:yes :yes) (:yes :no) (:no :yes) (:no :no))
Comment by Nicolás Berger [ 31/Jul/15 11:01 AM ]

This is not a bug. It's expected behavior because not all arguments to the nafc goal are ground.

From `nafc` docstring:

EXPERIMENTAL: negation as failure constraint. All arguments to the goal c must be ground. If some argument is not ground the execution of this constraint will be delayed.

In the example using fd, q is not ground (because a and b are not ground), so it's almost the same as if the nafc wasn't there.

Comment by Tassilo Horn [ 31/Jul/15 1:40 PM ]

My interpretation of the docstring is that the check will be delayed until the point in time where the variables become ground. And eventually q is ground in my first example. I mean, otherwise nafc would be pretty useless.





[LOGIC-171] The docstring of condu is incorrect or at least confusing Created: 28/Jul/15  Updated: 28/Jul/15

Status: Open
Project: core.logic
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Enhancement Priority: Major
Reporter: Tassilo Horn Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: docs, docstring


 Description   

The docstring of condu reads

Committed choice. Once the head (first goal) of a clause has succeeded, remaining goals of the clause will only be run once. Non-relational.

The sentence with respect to the once-semantics isn't correct. The head (first goal) can succeed at most once whereas the remaining goals of the clause committed to can succeed an unbounded number of times. The following example demonstrates that.

(defn y-or-n [x]
  (conde
   [(== x :y)]
   [(== x :n)]))

(run* [x y]
  (condu
   [(y-or-n x) (== y 1)] ;; (y-or-n x) succeeds once because it's the head goal
   [(== x :y) (== y 2)]))
;;=> ([:y 1])

(run* [x y]
  (condu
   [(== y 1) (y-or-n x)] ;; (y-or-n x) succeeds twice because it's not the head goal
   [(== x :y) (== y 2)]))
;;=> ([:y 1] [:n 1])

The current behavior shown in the example is in compliance with miniKanren on Scheme, so it's just the docstring which isn't right. The implementation is correct.






Generated at Mon Aug 03 01:37:01 CDT 2015 using JIRA 4.4#649-r158309.