Logic 81 #14

Closed
wants to merge 5 commits into
from

2 participants

@namin
Clojure member

Ready for review by @swannodette. I'll do a clean rebase / patch on JIRA once we're all happy.

@swannodette
Clojure member

I should explain a couple of things so it's clear why that original bit of code I wrote exists at all. The Scheme implementation of cKanren involves a lot of scanning of the constraint store. As an optimization I chose a different representation - the constraint store contains a map of variables to sets of constraint ids (integers) as well as a map of those ids to the actual constraints. Now finding the constraint set for a particular variable is a cheap operation.

However a complexity arises because logic vars can alias logic vars, imagine the case of (== u v) where u and v are both fresh. It easy to get into a situation where the aliasing is not reflected in the constraint store. My solution was to try and create stable "root" vars - there can only be one "root" var. Of course this means we have to do some merging of constraints and domain information if we have two fresh vars that have constraint information on them.

Ok, so what addcg does with fresh vars - it ensures they are created as roots. So to me this bug seems to be a violation of an invariant that unbound-rands should uphold. It should only return the vars which truly have no binding in the substitution map. Vars which have constraints but no binding appear as SubstValues in the substitution map with their value field, :v, set to ::unbound. So I don't think that addcg should check for clobbering, rather unbound-rands should be fixed (if it can of course).

Hopefully this makes sense. Happy to clarify further.

Clojure member

Thanks for the clarification. It would be very helpful if we could do a text chat, perhaps via Gmail (nada.amin@gmail.com)?

Clojure member

In a nutshell, my understanding of the root issue is that 'rands' does not take the substitution map into account.

Consider this program:

(run* [q]
           (fresh [x]
             (== q x)
             (predc q number? `number?)
             (== x "foo")))

First, (q . x). So x is the implicit root. But then, predc is attaching the constraint keyed by q, which is not a root!

Then unbound-rands just returns q, and this clobbers the (q . x).

In order for predc to attach the constraint correctly, it needs to walk the rands. The API issue now is that addc, updatec, remc do not take a Substitution.

Do you agree with this assessment?

Clojure member

Yes I think you are right! addc, updatec, and remc need the Substitution to know what vars a constraint actually refers to. This also opens the door for some optimizations I've been thinking about for a while - but more importantly I really do think this should address the underlying issue.

Clojure member

BTW, let me know if you would like to tackle this. More than happy to take a patch for master. Or if you'd rather focus on the alphaKanren work, I'm also more than happy to dig into this one.

@swannodette
Clojure member

This looks great! Patch welcome :)

@swannodette
Clojure member

Patch applied

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment