Nominal unification inspired by alphaKanren #12

Closed
wants to merge 64 commits into
from

2 participants

@namin
Clojure member

Review by @swannodette.

@swannodette
Clojure member

This is truly, truly fantastic. However official Clojure projects can't just merge pull requests. I need a ticket+patch in JIRA - http://dev.clojure.org/jira/browse/LOGIC. If it's not too much bother could you please submit a Clojure Contributor Agreement (CA) - http://clojure.org/contributing. If you're willing to become a contributor, I'm more than happy to go ahead and apply the patch ASAP while the CA slowly finds its way to North Carolina via snail mail :)

Again, thank you very much for this addition.

@namin
Clojure member

Sure. I'll do the ticket / patch on JIRA as well as sign the agreement tomorrow.

Also please let me know if you have suggestions.

Thanks. :-)

@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/main/clojure/clojure/core/logic.clj
@@ -2982,7 +2991,8 @@
(defn reify-constraints [v r cs]
(let [rcs (->> (vals (:cm cs))
(filter reifiable?)
- (map #(reifyc % v r)))]
+ (map #(reifyc % v r))
+ (filter #(not (nil? %))))]
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

I'm curious about this, why do we need to check for nil?

@namin
Clojure member
namin added a line comment Dec 16, 2012

In reifyc for the nom-hash constraint, I just reify the constraint if it's relevant to the end result. This is consistent with alphaKanren.

For example,

(run* [q]
  (nom-fresh [c d]
     (typo [] ['lam (nom-tie c ['lam (nom-tie d ['var c])])] q)))

would otherwise return

(([-> _0 [-> _1 _0]] :- lvar:x5037#lvar:xc5049 nom:b5036#lvar:gc5025 nom:b5036#_0 nom:b5036#[nom:b5026 lvar:trand5024]))

instead of just

((-> _0 (-> _1 _0)))

Because the constraints are on vars and noms that are not in the final result, they're just noisy and not interesting to the end user.

Simpler examples. Contrast:

(is (= (run* [q] (nom-fresh [a b] (nom-hash a q) (nom-hash b q))) '(_0)))
(is (= (run* [q] (fresh [x]  (nom-fresh [a b] (nom-hash a x) (nom-hash b x) (== [x a b] q))))
      '(([_0 a_1 a_2] :- a_2#_0 a_1#_0))))

For the first case, we don't want:

((_0 :- <nom:b5130>#_0 <nom:a5129>#_0))
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Ok, makes sense.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/main/clojure/clojure/core/logic/nominal.clj
+ (Nom. lvar))
+
+(defn nom? [x]
+ (instance? clojure.core.logic.nominal.Nom x))
+
+(defmethod print-method Nom [x ^Writer writer]
+ (.write writer (str "<nom:" (:name x) ">")))
+
+(defn- nom-bind [sym]
+ ((juxt identity
+ (fn [s] `(nom (lvar '~s)))) sym))
+
+(defn- nom-binds [syms]
+ (mapcat nom-bind syms))
+
+(defmacro nom-fresh
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Given that nom-fresh is in the nominal namespace do we need this? I suspect people might write something like this after requiring the nominal namespace as nom:

(run* [q]
   (fresh [x]
      (nom/fresh [y]
         ...)))
@namin
Clojure member
namin added a line comment Dec 16, 2012

Done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/main/clojure/clojure/core/logic/nominal.clj
+ Object
+ (unify-with-susp [v u s]
+ (unify s (apply-pi v (invert-pi (:pi u))) (:lvar u)))
+
+ clojure.core.logic.LVar
+ (unify-with-susp [v u s]
+ (unify-with-susp (Suspension. nil v) u s)))
+
+(defn susp [pi lvar]
+ (if (empty? pi) lvar (Suspension. pi lvar)))
+
+(defn susp? [x]
+ (instance? clojure.core.logic.nominal.Suspension x))
+
+(defn fold-right [f init coll]
+ (reduce (fn [x y] (f y x)) init (reverse coll)))
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Is this reverse necessary? Is coll guaranteed to be something we can reverse in constant time?

@namin
Clojure member
namin added a line comment Dec 16, 2012

This is only used with pi, which is a vector. So I think yes.

Incidentally, should I be making fold-right and other helpers private?

@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Great.

Yes making helpers private is nice for communicating intent. I should be more consistent myself in the logic.clj but the details of the cKanren support are still changing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/main/clojure/clojure/core/logic/nominal.clj
+ (walk-term [v f]
+ (nom-tie (walk-term (:binding-nom v) f)
+ (walk-term (:body v) f)))
+ clojure.core.logic.IOccursCheckTerm
+ (occurs-check-term [v x s]
+ (occurs-check-term (:body v) x s))
+ IApplyPi
+ (apply-pi [t pi]
+ (nom-tie (api (:binding-nom t) pi) (apply-pi (:body t) pi)))
+ IApplyHash
+ (apply-hash [x a c s]
+ (if (.equals a (:binding-nom x))
+ (bind s (remcg c))
+ (bind* s (remcg c) (addcg-now (-nom-hash? a (:body x)))))))
+
+(defn nom-tie [binding-nom body]
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

As with nom/fresh I think we should just call this tie and users will write nom/tie

@namin
Clojure member
namin added a line comment Dec 16, 2012

Done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/main/clojure/clojure/core/logic/nominal.clj
+ :lvar lvar
+ :pi pi
+ :name (:name lvar)
+ not-found))
+ clojure.core.logic.IUnifyTerms
+ (unify-terms [u v s]
+ (unify-with-susp v u s))
+ clojure.core.logic.IUnifyWithObject
+ (unify-with-object [v u s]
+ (unify s (:lvar v) (apply-pi u (invert-pi (:pi v)))))
+ clojure.core.logic.IUnifyWithLVar
+ (unify-with-lvar [v u s]
+ (unify-with-susp v (Suspension. nil u) s))
+ clojure.core.logic.nominal.IUnifyWithSuspension
+ (unify-with-susp [v u s]
+ (if (.equals (:lvar v) (:lvar u))
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

.equals will trigger reflection here since there are no type hints. Any reason to not use = here? = will trigger a call to .equals if the object does not implement .equiv

@namin
Clojure member
namin added a line comment Dec 16, 2012

Oh, ok. Changed all .equals to = in nominal.clj.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/main/clojure/clojure/core/logic.clj
@@ -2891,6 +2896,10 @@
a)
((remcg c) a))))
+(defn addcg-now [c]
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Ha, that's a fun use of bind*, I'm happy how little you had to change logic.clj.

@namin
Clojure member
namin added a line comment Dec 16, 2012

Indeed! And this could even be in the nominal package, but perhaps, it is generally useful?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette commented on the diff Dec 16, 2012
src/main/clojure/clojure/core/logic/nominal.clj
+(defprotocol IUnifyWithTie
+ (unify-with-tie [v u s]))
+
+(defprotocol IApplyPi
+ (apply-pi [t pi]))
+
+(defprotocol IApplyHash
+ (apply-hash [t a c s]))
+
+;; =============================================================================
+;; Nom
+
+(declare nom api)
+
+(deftype Nom [lvar]
+ clojure.core.logic.IWalkable
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Minor nitpick, since you're using core.logic you don't need to fully qualify protocols like this IWalkable is sufficient. For Java interfaces like clojure.lang.IObj the qualification is necessary.

@namin
Clojure member
namin added a line comment Dec 16, 2012

If I change it to just IWalkable, I get:
Unable to resolve symbol: IWalkable in this context, compiling:(clojure/core/logic/nominal.clj:36)

@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Hmm, strange - I'll look into this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/test/clojure/clojure/core/logic/tests.clj
@@ -1,6 +1,8 @@
(ns clojure.core.logic.tests
(:refer-clojure :exclude [==])
(:use [clojure.core.logic :exclude [is] :as l]
+ ;; TODO(namin): If I don't include this here, nominal/tests fail... why?
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Odd, in what way do they fail?

@namin
Clojure member
namin added a line comment Dec 16, 2012

The nominal tests fail, as if the nominal src package never got imported. For example

ERROR in (test-nom-2) (core_deftype.clj:527)
expected: (= (run* [q] (fresh [x y z] (nom-fresh [a] (nom-hash a q) (== q (clojure.core/seq (clojure.core/concat (clojure.core/list x) (clojure.core/list y))))))) (quote ((_0 _1))))
  actual: java.lang.IllegalArgumentException: No implementation of method: :runnable? of protocol: #'clojure.core.logic/IRunnable found for class: clojure.core.logic.nominal$_nom_hash_QMARK_$reify__3731
 at clojure.core$_cache_protocol_fn.invoke (core_deftype.clj:527)
    clojure.core.logic$eval6142$fn__6143$G__6133__6150.invoke (logic.clj:165)
    clojure.core.logic$cgoal$reify__8147.invoke (logic.clj:3016)
    clojure.core.logic.Substitutions.bind (logic.clj:1147)

In other cases, it's not doing nominal unification, for example:

FAIL in (test-nom-4) (tests.clj:84)
expected: (= (run* [q] (nom-fresh [a b] (== (nom-tie a q) (nom-tie b b)))) (quote (a_0)))
  actual: (not (= () (a_0)))

The test works when I run them in emacs in the repl, but fail with lein test. Some configuration issue?

@namin
Clojure member
namin added a line comment Dec 27, 2012

Any insights on this mundane TODO?

@swannodette
Clojure member
swannodette added a line comment Dec 27, 2012

I tried your branch, I think you need to drop :reload. The tests then work fine for me.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@swannodette swannodette and 1 other commented on an outdated diff Dec 16, 2012
src/test/clojure/clojure/core/logic/nominal/tests.clj
+ (is (= (run* [q] (fresh [x] (nom/fresh [a] (nom/hash a q) (== q `(~x))))) '((_0))))
+ (is (= (run* [q] (fresh [x y] (nom/fresh [a] (nom/hash a y) (== y `(~x)) (== [y a] q))))
+ '(([(_0) a_1] :- a_1#_0))))
+ (is (= (run* [q] (fresh [x y z] (nom/fresh [a] (nom/hash a q) (== q `(~x ~y))))) '((_0 _1))))
+ (is (= (run* [q] (fresh [x y z] (nom/fresh [a] (nom/hash a z) (== z `(~x ~y)) (== [z a] q))))
+ '(([(_0 _1) a_2] :- a_2#_1 a_2#_0))))
+ (is (= (run* [q] (fresh [x y] (nom/fresh [a] (nom/hash a q) (conso x y q)))) `(~(lcons '_0 '_1))))
+ (is (= (run* [q] (fresh [x y z] (nom/fresh [a] (nom/hash a z) (conso x y z) (== [z a] q))))
+ [[[(lcons '_0 '_1) 'a_2] ':- 'a_2#_1 'a_2#_0]]))
+ (is (= (run* [q] (fresh [x y] (nom/fresh [a] (conso x y q) (nom/hash a q)))) `(~(lcons '_0 '_1))))
+ (is (= (run* [q] (fresh [x y z] (nom/fresh [a] (nom/hash a z) (conso x y z) (== [z a] q))))
+ [[[(lcons '_0 '_1) 'a_2] ':- 'a_2#_1 'a_2#_0]]))
+ (is (= (run* [q] (nom/fresh [a b] (== q nil) (nom/hash a q))) '(nil)))
+ (is (= (run* [q] (nom/fresh [a b] (== q 1) (nom/hash a q))) '(1)))
+ (is (= (run* [q] (nom/fresh [a b] (== q [1 1]) (nom/hash a q))) '([1 1])))
+ (is (= (run* [q] (nom/fresh [a b] (== q '(1 . 1)) (nom/hash a q))) '((1 . 1))))
@swannodette
Clojure member
swannodette added a line comment Dec 16, 2012

Just making sure that you actually want to test that q unifies with a list that contains 2 numbers and 1 symbol. Clojure doesn't have pairs like Scheme. lcons and the supporting protocol fns lfirst lnext exist so that you can construct sequence like things with an improper tail as you can in Scheme via cons - but in the case of core.logic only logic vars are truly allowed. Though we don't do any explicit validation around lcons now - we may do so in the future. A closer translation of this test would be:

(= (run* [q] 
     (nom/fresh [a b] 
       (== q (lcons 1 1))
       (nom/hash a q)))
   (lcons 1 1))
@namin
Clojure member
namin added a line comment Dec 16, 2012

Good catch. Done.

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

I've been working on a possible solution to this. The purpose of the SubstValue type is to support "compound" values in the Substitutions. For example I think what we want the Substitutions map to look like is something like this:

{x (SubstValue. ::unbound {::fd (interval 1 3) ::nom ...})
 y (SubstValue. ::unbound {::fd (interval 1 3) ::nom ...})}

I'm not exactly sure what we would store under ::nom as I still haven't had time to look into how alphaKanren works because I've been a bit busy trying to squash some pressing cKanren bugs. But perhaps you can see if this will work or needs to be augmented in some way?

Clojure member

Oh, this is insightful, thanks. I'll think more about it. My first idea of storing the pis of suspensions in there doesn't quite work, since the same variable can have many suspensions, and they shouldn't unify.

BTW, I signed the CCA and sent it by snail mail today. It will probably arrive before we figure all this out ;-)

@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.

@namin
Clojure member

Sure, I'll send you a patch.

Here is the status for the alphaKanren work. Good news first: all constraints except for != are compatible with alphaKanren. I also managed to turn my quine generator into a nominal quine generator :) Bad news is that I am not too happy with the current design. So I'll explore your hunch of using meta attributes for suspensions, and also think about != and efficiency.

I am still not sure I've grasped all the invariants that should hold in the substitution map -- what you've written above is already tremendously useful, so if you have more info to share, would love to hear. I think understanding the substitution map is key to a better alphaKanren integration.

@swannodette
Clojure member

nominal quine generator!!! :D

Some other interesting bits related to Substitution, logic var aliasing, and unification.

root-val, returns the actual value store in the Substitution for a logic var - the SubstValue if it exists. walk does not do this, it will look inside the SubstValue and extract the :v field.

root-var, returns the "root" for a given var - so it does what walk does, but it stops before returning the bound value. We should identify the critical locations where this is actually required. I've done some work to ensure this but perhaps it could be improved?

If a constrained unbound logic var becomes unified with another constrained unbound logic var we need to migrate the constraints in the ConstraintStore and repoint one of the vars to the "root". You can see the sketch of this in LVar's implementation of IUnifyWithLVar. We also need to merge domain information. You can see this approach in the logic-77-lead branch. I'm sort of experimenting there, I don't yet have a principled approach. I believe your insight about addc, remc, udpatec may lead to quite a few simplifications across the board.

Also, in the logic-77-lead branch I've changed SubstValue to have an explicit :doms field and added corresponding fns for manipulating them, add-dom, get-dom, rem-dom etc. I have left the related add-attr operators alone as there are other kinds of information one might want to tag a variable with - for example optimizations for cKanren such as custom domain enumeration strategies for a particular logic var. This ad-hoc information goes into the meta field of SubstValue.

There's a big assumption in the design here - unification and other kinds of constraint solving are distinct steps. Unification only occurs on bound values - unification does not occur on the finite domain types for example. One cKanren implementation I played around with had instances of the finite domain types stored directly in the substitution and some constraint solving happened via unification - but of course I ran into trouble with !=. This pushed me to consider many different designs because I didn't want to abandon the simple approach to disequality nor the optimizations around the ConstraintStore representation - I settled on the SubstValue idea.

I've discerned at least the big possibilities - but I don't yet see the repercussions:

  • Unification becomes a constraint like any other - it has no privileged position (does this have performance implications?). This seems a bit strange in that in miniKanren unification doesn't need "delays" the way the cKanren does (terms must be ground before the constraint can run). But perhaps unification for alphaKanren does not follow this? I understand that alphaKanren unification involves suspensions? You'll have to shed some light on this for me :)

  • Unification remains privileged. Other constraints trying to get a free ride on unification (like disequality) becomes an anti-pattern. Perhaps some of the issues arise from the implementation of update-prefix, where we pass the the value of the substitution prior to unification into a goal which runs the constraints on the new additions to the substitution. This seems yucky to me - why not just run the constraints at the point of unification? Then disequality could work this way too and we could eliminate the :l field from Substitution which is just there to support the elegant but perhaps inflexible unification prefix approach Dan & Will took for disequality.

Perhaps your understanding about the implementation details of nominal unification can settle which way we should go?

Fortunately the code where these big decisions must be made in core.logic is tiny :)

@namin
Clojure member

Thanks for the write-up, very insightful.

Regarding alphaKanren, we need to be able to ensure constraints like "t1 should unify with t2 after swapping all a's and b's in t2". Now if t2 is a variable, we can't just swap all a's and b's, hence a suspension is just a bundle of swaps to do and a variable. So, now we can say, unify t1 with ((a b))t2, where ((a b))t2 is a suspension. Even if t2 is not grounded, there could be some constraints rewriting rules to apply: e.g. if t1==t2, then you can just replace this unification requirement with two freshness constraints 'a fresh in t2' and 'b fresh in t2'.

This paper has a nice summary on page 5 of the rewrite rules for nominal unification:
http://www.inf.kcl.ac.uk/staff/maribel/papers/TERMGRAPH06.pdf

I am naturally attracted to making unification a constraint like any other, but still wondering about the repercussions... will sleep on it.

BTW, there are some complications with the LOGIC-81 patch that I need to investigate. So don't expect something today.

@swannodette
Clojure member

Ok, my hazy picture of nominal unification is getting less hazy. One question, why do we need the Suspension type at all if we have a constraint solver backing our miniKanren implementation? Reading over Will's dissertation again it seems the susp tag is there specifically because miniKanren didn't have a generic constraint infrastructure in place. Is there some subtlety to your nominal unification approach that prevents simply saying this fresh var has a constraint such that if a unification happens we update the ::nom information of its SubstValue with the swapped version of the partially or fully instantiated term? If partially instantiated then we constrain the fresh vars within in the same way?

While making unification a regular constraint is enticing I suspect it will be more work than simply redefining disequality to not use unification. It might be fruitful to first attempt to get unification / finite domains / nominal unification all working under the same framework first - then perhaps consider what it would take to get unification working as normal constraint.

That said, converting unification into a normal constraint would be a very big step forward - we would have some notion of how polymorphic constraints work, eliminating the need for both != and !=fd and so on.

@namin
Clojure member

Yes, that's what I want to explore next. What I am not sure about is whether we can really treat the nom-swaps as properties of the vars as opposed to the unification. For example,
x == (b c)z
x == (a b)y
y == (a b)z
etc.
now, what do we store with each variable/constraint? In my current implementation, I am composing the swaps through the suspensions.

@swannodette
Clojure member

Couldn't something like this work?

x == (b c)z ; s0 = {x (SubstValue. ::unbound {::nom [(swap b c z)]})}
x == (a b)y ; s1 = {x (SubstValue. ::unbound {::nom [(swap a b y) (swap a b z)]})}
y == (a b)z ; s2 = {x (SubstValue. ::unbound {::nom [(swap a b y) (swap a b z)]})
                    y (SubstValue. ::unbound {::nom [(swap a b z)]})}
@namin
Clojure member

It might work. I'll give it a shot sometimes.

@namin namin Merge branch 'master' into nominal-base
Conflicts:
	src/main/clojure/clojure/core/logic.clj
5a98456
@swannodette
Clojure member

I've made unification less tedious to implement, but this means your code will break if you were depending on the type specific unification protocols. Fortunately most of the code changes should involve deleting boilerplate.

@namin
Clojure member

I started trying out storing the swaps as attributes. The problem is when we have a collection, and need to propagate the swaps:
x == swap (a b) in [y z]
Any suggestions on how to store the swaps in this case? In the current implementation, this becomes
x == [ swap (a b) y , swap (a b) z ]

@swannodette
Clojure member

I'm assuming that the substitution looks like the following:

s0 = {x [y z]}

x is a vector containing two fresh logic vars.

Then we apply the swap to x. When you encounter fresh logic vars you would make them root vars by associating them with a SubstValue with the swap information in the :dom field. This doesn't need to be done by hand, the following should work:

(add-dom s y :nom [(swap a b)]) ; and
(add-dom s z :nom [(swap a b)])

Is this what you are doing?

@namin
Clojure member

Hmm. I am just not convinced we can express everything with swaps on unbound variables, because what happens is that we need to apply the swaps within structures.

Say we have (== (nom/tie a [[x] y]) (nom/tie b [w z])), then we need (== (swap (a b) in [x y]) [w z]). How do we represent this?

@swannodette
Clojure member

Since the tie is in control of unification is there some difficulty here I'm missing? It seems to me the tie deeply applies swaps to itself updating the substitution. Then it unifies itself with the other term.

@namin
Clojure member

I am just not sure how to deeply apply swaps without having suspensions. Let's take it on chat sometimes.

@swannodette
Clojure member

Yes would also need to add a constraint to each var that gets a swap. This constraint would apply the swap list when the var becomes ground. Related I think we can eliminate the Suspension type altogether. We can just leverage the constraint solving infrastructure to do that work.

@swannodette
Clojure member

Starting to look more closely at the nominal implementation, I believe removing Suspension and leveraging the constraint solving framework is the key.

namin added some commits Dec 26, 2012
@swannodette
Clojure member

Check out master, we have deep constraints now in the form of treec :)

@namin
Clojure member

Cool, @swannodette. I could use treec for nom/hash. I added some hacks for special handling and reifyc (but just saw that you anticipated that as well).

@namin
Clojure member

@swannodette : I've been working on an implementation of core.logic.nominal which doesn't use suspensions. I am almost there, but the quine example gets generated with extra nils at the end of lists. Debugging that.

In addition, with the latest core.logic master, I'm having trouble printing to the repl for debugging. Have you been experiencing that?

@namin
Clojure member

FYI, the no-susp branch is here: https://github.com/namin/core.logic/compare/nominal-no-susp

All tests pass, but there's still a problem with quines related to extra nils.

@swannodette
Clojure member

Wow, cool! Now that run expressions are lazy you need to wrap them in a doall when debugging. I'm happy to add a debug atom that we can set to make this less tedious. Let me know.

@swannodette
Clojure member

Code is looking pretty! :) :) :)

@swannodette
Clojure member

Please feel free to attach a patch in JIRA. As soon as your CA is in more than happy to give you commit rights to core.logic :)

@namin
Clojure member

Neat, thanks :)

The quines now run with the no-susp branch. I'll attach a patch on JIRA soon. Just want to iron out a few more quirks.

@namin
Clojure member

Patch attached to http://dev.clojure.org/jira/browse/LOGIC-78

Closing this pull request.

@namin namin closed this Dec 31, 2012
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment