core.logic

unifier is not commutative

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
  • Environment:
    clojure 1.3.0, core.logic 0.6.7

Description

I am not sure if this is actually a bug

user=> (require '[clojure.core.logic :as logic])
nil
user=> (logic/unifier (logic/unifier '{:a ?x} '{:a ?y}) '{:a 5})
nil
user=> (logic/unifier (logic/unifier '{:a ?x} '{:a 5}) '{:a ?y})
{:a 5}

For comparison: here is the result of core.unify (and what I expected)

user=> (require '[clojure.core.unify :as unify])
nil
user=> (unify/unifier (unify/unifier '{:a ?x} '{:a ?y}) '{:a 5})
{:a 5}
user=> (unify/unifier (unify/unifier '{:a ?x} '{:a 5}) '{:a ?y})
{:a 5}

Activity

Hide
Jens Bendisposto added a comment -

Obviously i meant associative, not commutative.

Show
Jens Bendisposto added a comment - Obviously i meant associative, not commutative.
Hide
David Nolen added a comment -

Thanks for pointing this out. Yes the unifier isn't doing the right thing here. Will look into a fix.

Show
David Nolen added a comment - Thanks for pointing this out. Yes the unifier isn't doing the right thing here. Will look into a fix.
Hide
Brian Goslinga added a comment -

The issue occurs because (unifier '{:a ?x} '{:a ?y}) is {:a _.0}, and since _.0 is a symbol, it does not unify with 5.

Changing the definition of solve to use walk* instead of -reify fixes the issue, but is a breaking change (and breaks tests that depend on the reification lvars).

unifier could use an alternative implementation of solve, but that probably isn't ideal and would still be a breaking change (although less of one perhaps).

Show
Brian Goslinga added a comment - The issue occurs because (unifier '{:a ?x} '{:a ?y}) is {:a _.0}, and since _.0 is a symbol, it does not unify with 5. Changing the definition of solve to use walk* instead of -reify fixes the issue, but is a breaking change (and breaks tests that depend on the reification lvars). unifier could use an alternative implementation of solve, but that probably isn't ideal and would still be a breaking change (although less of one perhaps).

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved: