core.logic

Unification of sets does not consider all possibilities

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • Priority: Major Major
  • Resolution: Completed
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • 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.

Activity

Hide
Aaron Brooks added a comment -

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

Show
Aaron Brooks added a comment - BTW, I should note that issue was noticed by Jim Duey.
Hide
David Nolen added a comment -

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.

Show
David Nolen added a comment - 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.
Hide
Aaron Brooks added a comment -

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.

Show
Aaron Brooks added a comment - 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.
Hide
David Nolen added a comment -

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.

Show
David Nolen added a comment - 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.
Hide
Aaron Brooks added a comment -

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!

Show
Aaron Brooks added a comment - 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!
Hide
David Nolen added a comment -

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

Show
David Nolen added a comment - Excellent. I'll leave the protocol in, along with some fair warning about attempting it Thanks for the quick feedback.

People

Vote (0)
Watch (1)

Dates

  • Created:
    Updated:
    Resolved: