Fork me on GitHub
#core-logic
<
2017-12-06
>
noprompt22:12:19

is there a rationale for why lvars as map keys do not unify?

(run* [q]
  (fresh [a b]
    (== {a b} {:a 2})
    (== q (list a b))))
;; => ()

noprompt22:12:46

in my spare time i’ve been working on a term rewriting engine and was also confronted with the problem of unifying maps. i was able to find a solution that achieves this. i was surprised to find that core.logic doesn’t support this, however, i wouldn’t be surprised if i may have overlooked something in my own algorithm.

hiredman22:12:27

there is no one way to do it

hiredman22:12:11

(== {a b c d} {:a 1 😛 2})

hiredman22:12:17

(== {a b c d} {:a 1 :b 2})

noprompt22:12:09

the algorithm i wrote unifies ground entries, then entries with ground values, then entries with ground keys, then entries where both the key and value are variable.

hiredman22:12:35

there is no single unification for that

noprompt22:12:42

your example can be unified in multiple ways, the values can be streamed to a, b, c, and d in those cases.

noprompt22:12:57

actually, that’s not true.

noprompt22:12:14

the fact there exists a solution refutes that argument.

noprompt22:12:09

so maybe my understanding here is misguided.

noprompt22:12:27

can you explain your emphasis on “single”?

hiredman22:12:08

lists are defined inductively via cons, so there is a one order they can be walked for unification, and that orders arises from the definition

hiredman22:12:20

maps are not inductively defined, so there is no single iteration order, so there is no fixed thing to wire in to the unifier

hiredman22:12:09

you can do it, but you will have to make some choices to do it that preclude being general, which is what a library like core.logic is trying to do

noprompt22:12:18

i see. can you elaborate more on why the inductive property is important?

noprompt22:12:12

wrt core.logic?

noprompt23:12:00

i’m guessing the solution here would be to use another goal in favor of == which does stream the substitutions.

hiredman23:12:30

because unification has to traverse datastructures, if a datastructure is defined inductively, that is an order the structure can be traversed

hiredman23:12:46

I bet you could make it work if you either only used one concrete map type, or sorted it before unifying

noprompt23:12:05

the strategy i mentioned above works pretty well. although, again, my setting is term rewriting which expects the left-hand side of the equation to be ground.

hiredman23:12:43

sure, if your model is less general then you can do more

noprompt23:12:07

so, in the context of core logic, would the solution then be two stream the solutions via a custom goal?

noprompt23:12:07

i understand the rationale above now.