<< Back to previous view

[LOGIC-56] Unification of sets does not consider all possibilities Created: 21/Sep/12  Updated: 27/Sep/12  Resolved: 27/Sep/12

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

Type: Defect Priority: Major
Reporter: Aaron Brooks Assignee: David Nolen
Resolution: Completed Votes: 0
Labels: None


 Description   

The current unify-with-set logic will unify the first lvars it comes across, preventing backtrack unification with other lvars in the sets. See examples:

user> (run* [out]
        (fresh [a b c d]
          (== out [a b c d])
          (== #{a b} #{c d})))
([_.0 _.1 _.0 _.1])

user> (run* [out]
        (fresh [a b c d]
          (== out [a b c d])
          (== [a c] [7 9])
          (== #{a b} #{c d})))
()

I'm still thinking of a way to efficiently handle this but wanted to post it when I came across it.

 Comments   
Comment by Aaron Brooks [ 21/Sep/12 3:18 PM ]

BTW, I should note that issue was noticed by Jim Duey.

Comment by David Nolen [ 21/Sep/12 3:28 PM ]

More evidence that I probably should not have attempted unification with sets. This is why there is no support for logic vars as keys in maps - we should probably even throw in that case.

Perhaps we can support backtracking by switching complex unification of sets to a conde? Though at that point you're probably better of using lists + distincto.

Comment by Aaron Brooks [ 21/Sep/12 3:34 PM ]

Yeah, I looked at map unification and decided to punt entirely. One thing at a time.

Now is a good time to thank you, again, for core.logic. This is better to have than not.

Comment by David Nolen [ 26/Sep/12 3:22 PM ]

After some discussion with William Byrd at StrangeLoop I'm inclined to remove set unification from core.logic entirely. It turns out this is an open research problem and I find it unlikely that I'll be able to figure this one out anytime soon. Will this cause too much trouble for you all?

Note that a related change would be to throw on any maps that have logic vars as keys during unification.

Comment by Aaron Brooks [ 26/Sep/12 8:58 PM ]

This seems entirely reasonable. The complexity explodes quickly and distincto judiciously applied is far more efficient. Kill it as you wish. (Though I might suggest leaving the protocol in with no implementation so experimenters can easily extend it.)

Thanks!

Comment by David Nolen [ 27/Sep/12 9:36 AM ]

Excellent. I'll leave the protocol in, along with some fair warning about attempting it Thanks for the quick feedback.

Comment by David Nolen [ 27/Sep/12 9:39 PM ]

fixed, http://github.com/clojure/core.logic/commit/cdc4bf8563e9f566cc6e3e0e4f8a7735cd92b88e

Generated at Fri May 24 19:09:39 CDT 2013 using JIRA 4.4#649-r158309.