Afternoon, I'm new to core.logic, and was working through the αKanren <http://webyrd.net/alphamk/alphamk.pdf> paper with core.logic.nominal. On page 4, there is an example which translates to:
*(l/run* [q] (n/fresh [a b] (l/fresh [x y] (l/== (n/tie a (n/tie a x)) (n/tie a (n/tie b y))) (l/== `(~x ~y) q)))) * *=> ((_0 _1))* The example output in the paper is as follows, with the given explanation: *((((susp ((a0 a1)) _0) _0) : ((a0 . _0))))* *The first call to ≡ applies the swap (a b) to the unbound variable y, and then associates the resulting suspension (susp ((a b)) y) with x . Of course, the unifier could have applied the swap to x instead of y, resulting in a symmetric answer. The freshness constraint states that the nom a can never occur free within y, as required by the definition of binder equivalence.* Could somebody explain to me, as if I were a child, this discrepancy? I looked at the source, and saw code that looked very much like suspensions being applied at creation time, rather than on var instantiation like the paper elsewhere indicates, but I'm out of my depth and not in a position to reason about strategy. Best, Moe -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en --- You received this message because you are subscribed to the Google Groups "Clojure" group. To unsubscribe from this group and stop receiving emails from it, send an email to clojure+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/clojure/756b55d5-e952-4f2c-98da-ba9a43ec34c9n%40googlegroups.com.
