Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Nominal unification inspired by alphaKanren #12

Closed
wants to merge 64 commits into from
Closed

Nominal unification inspired by alphaKanren #12

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
64 commits
Select commit Hold shift + click to select a range
475239f
Nominal unification inspired by alphaKanren
namin Dec 15, 2012
1b38ce4
.equals to =
namin Dec 16, 2012
502007e
nom-free|tie|hash -> nom/free|tie|hash
namin Dec 16, 2012
ffdbdde
in tests, lcons instead of invalid pairs a la scheme
namin Dec 16, 2012
60e54c6
make some helpers private
namin Dec 16, 2012
5b5734b
bug fix: suspension must handle all iunifywith methods, b/c it behave…
namin Dec 16, 2012
0fc2518
fix occurs-check-term to call occurs-check
namin Dec 17, 2012
ea3a87f
spurious when -- bind takes care of it
namin Dec 17, 2012
7c52d1d
walk-term for suspension now tries to apply-pi if possible
namin Dec 17, 2012
211e155
more flexible printing
namin Dec 17, 2012
5785a72
bug fix: some edge cases
namin Dec 17, 2012
0e35e8c
suspensions do not mesh well with constraints :-(
namin Dec 17, 2012
26297e2
Merge branch 'master' into nominal-base
namin Dec 17, 2012
a3b9872
misaligned args to unify
namin Dec 17, 2012
10e5f15
a bug in nominal unification
namin Dec 17, 2012
b7d272f
bug fix for nominal unification: hack upon hack... in need of some pr…
namin Dec 17, 2012
0f6e600
bug fix: suspensions need to be deep-walked
namin Dec 18, 2012
8e5a733
minor whitespace formatting
namin Dec 18, 2012
a7822f7
perhaps a more principled nominal unification... but less protocolaire?
namin Dec 18, 2012
b59d7c8
minor whitespace
namin Dec 18, 2012
63a9805
anoter issue with cKanren, related to suspensions
namin Dec 18, 2012
3f8b6d1
minor typo
namin Dec 19, 2012
5dbcf8f
addcg should not clobber any binding information.
namin Dec 19, 2012
db83189
handling simultaneous cloberring
namin Dec 19, 2012
feb75b3
Merge branch 'logic-81' into nominal-base
namin Dec 19, 2012
b419144
predc now works with nominal uni
namin Dec 19, 2012
74167de
cKanren constraints work!
namin Dec 19, 2012
8ee782a
print ties so that they can be evaluated in clojure
namin Dec 19, 2012
baec652
principled rooting of vars
namin Dec 20, 2012
673babc
Merge branch 'logic-81' into nominal-base
namin Dec 20, 2012
104b154
fix merge for tie/predc test
namin Dec 20, 2012
1cc361f
Merge branch 'master' into nominal-base
namin Dec 20, 2012
d4a7558
Merge branch 'nominal-base' of github.com:namin/core.logic into nomin…
namin Dec 20, 2012
5a98456
Merge branch 'master' into nominal-base
namin Dec 21, 2012
bb32fe6
Merge branch 'master' into nominal-base
namin Dec 24, 2012
9047dd8
update to latest unify API
namin Dec 24, 2012
2fb005c
nominal disequality test works now, thanks @swannodette
namin Dec 24, 2012
0910252
change needed to run quine_nom. TODO: find a small test to reproduce …
namin Dec 24, 2012
62bdd93
Revert "change needed to run quine_nom. TODO: find a small test to re…
namin Dec 24, 2012
e00d5a0
Merge branch 'master' into nominal-base
namin Dec 24, 2012
2ea7167
Merge branch 'master' into nominal-base
namin Dec 24, 2012
369493e
tweaks
namin Dec 25, 2012
40fe26d
Merge branch 'master' into nominal-base
namin Dec 26, 2012
8329675
all tests pass
namin Dec 26, 2012
833979b
needed to avoid infinite loops in quines prog
namin Dec 26, 2012
9f59a44
Merge branch 'master' into nominal-base
namin Dec 26, 2012
974f6ca
bug fix: susp should trump lvar for unify-terms
namin Dec 26, 2012
f3330bc
disunify does not quite work with suspensions
namin Dec 26, 2012
a5b9301
fix disunify with suspensions and be more systematic about tovar
namin Dec 26, 2012
7750c88
Merge branch 'master' into nominal-base
namin Dec 26, 2012
2c17edb
Merge branch 'master' into nominal-base
namin Dec 26, 2012
f1ffc6a
Merge branch 'master' into nominal-base
namin Dec 27, 2012
a176adf
Merge branch 'master' into nominal-base
namin Dec 27, 2012
1e1bc79
use treec for nom/hash
namin Dec 27, 2012
9bba714
Merge branch 'master' into nominal-base
namin Dec 27, 2012
a005907
no need for addcg-now anymore
namin Dec 27, 2012
ddb8a4d
removing :reload from core.logic tests enable core.logic.nominal test…
namin Dec 27, 2012
64bb9af
Merge branch 'master' into nominal-base
namin Dec 27, 2012
5106567
Merge branch 'master' into nominal-base
namin Dec 27, 2012
ebd8f63
Merge branch 'master' into nominal-base
namin Dec 27, 2012
c33bfac
Merge branch 'master' into nominal-base
namin Dec 28, 2012
84d9770
Merge branch 'master' into nominal-base
namin Dec 29, 2012
f70b108
Merge branch 'master' into nominal-base
namin Dec 30, 2012
d44949c
change for suspensions
namin Dec 30, 2012
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
18 changes: 14 additions & 4 deletions src/main/clojure/clojure/core/logic.clj
View file
Open in desktop
Expand Up @@ -20,6 +20,7 @@
;; =============================================================================
;; Marker Interfaces

(definterface IWalkable)
(definterface IVar)

;; =============================================================================
Expand Down Expand Up @@ -309,7 +310,7 @@
;; =============================================================================
;; Constraint Store

(declare lvar? interval multi-interval)
(declare lvar? walkable? interval multi-interval)

(defn bounds [i]
(pair (lb i) (ub i)))
Expand Down Expand Up @@ -1050,12 +1051,12 @@
(Substitutions. (assoc s u v) l cs cq cqs _meta)))

(walk [this v]
(if (lvar? v)
(if (walkable? v)
(loop [lv v [v vp :as me] (find s v)]
(cond
(nil? me) lv

(not (lvar? vp))
(not (walkable? vp))
(if-let [sv (and (subst-val? vp) (:v vp))]
(if (= sv ::unbound)
(with-meta v (assoc (meta vp) ::unbound true))
Expand Down Expand Up @@ -1268,6 +1269,10 @@
(defn lvar? [x]
(instance? clojure.core.logic.IVar x))

(defn walkable? [x]
(or (lvar? x)
(instance? clojure.core.logic.IWalkable x)))

;; =============================================================================
;; LCons

Expand Down Expand Up @@ -2891,6 +2896,10 @@
a)
((remcg c) a))))

(defn addcg-now [c]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

(fn [a]
(bind* a (addcg c) (run-constraint c) (fn [a] (queue a c)))))

;; TODO NOW: try an implementation that allows constraints
;; to run roughly in the order they normaly would. reverse
;; xcs in run-constraints, (into cq (reverse xcs)), cq should
Expand Down Expand Up @@ -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? %))))]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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))

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, makes sense.

(if (empty? rcs)
(choice (list v) empty-f)
(choice (list `(~v :- ~@rcs)) empty-f))))
Expand Down