Thanks, Greg. I can see now. Sorry that it took several posts in order to explain it to me.
Very interesting and clever idea. So there is a kind of distribution of complement information across different branches of conde under forall. I didn't think about it under this angle. четверг, 14 декабря 2017 г., 22:57:18 UTC+3 пользователь Greg Rosenblatt написал: > > > So, If I understand correctly that's what you do: >> >> 1) You treat forall(x) like eigen(x). Eigen variable can be unified with >> itself or `fresh` variable that occurs deeper. >> > > It's more flexible than the existing eigen implementation, which gives > forall-like behavior only when == is the only basic constraint. > > 2) You propogate `not` down to primitive goals like unification, >> constraints, etc, swapping conjuncts/disjuncts and fresh/forall on the road. >> > > Right. > > >> However, there are several details of your approach that is still unclear >> to me. >> >> 1) How exactly `forall` interacts with constraints ? When you see `(forall >> (x) (=/= `(2 . ,x) y))` you delay this goal as long as possible and then >> replace it to >> (conde ((not-pairo y)) ((fresh (a d) (== `(,a . ,d) y) (=/= 2 a)))) ? >> > > I'm implementing a system with dynamic goal scheduling, which has the > luxury of being able to translate to the conde immediately without > branching (hypothetically, because I haven't implemented this approach to > negation yet). Complex goals like this conde are deferred by default, and > checked for satisfiability when dependency constraints are tightened. In > this case, y is the only dependency, and unifying y will trigger an update > for the conde. > > For instance, (== 7 y) means the conde is irrefutable, and can be removed, > whereas (fresh (v) (== `(,v . 3) y)) instead will lead to the conde being > simplified to just (=/= 2 v). > > >> 2) What would be the answer to the following queries: `forall (x) (x == >> 1)`, `forall (x) (x =/= 1)` ? Should they fail or not ? >> > > These would both fail. Logically, forall will only succeed when its > variable could be any value from your data universe... > > >> 3) Can you handle cases like : `forall (x) (conde (x == 1) (x =/= 1))` ? >> > > .. for instance, yes, (forall (x) (conde ((== x 1)) ((=/= x 1)))) will > succeed. > > >> Taken my approach, it can be viewed as (not (fresh (x) (x =/= 1) (x >> == 1) )). The inner goal will fail and negation of failed goal is `success`. >> How similar effect can be achieved with `on-the-fly` propagation of >> `not` ? >> > > Your solution is nice and straightforward in cases like this, and I'd > prefer this strategy where possible. > > I'll describe an alternative approach that can handle more complex > situations on the fly, using bounded forall, which seems the least > "magical" of the approaches I've considered: > (forall-bounded (x* ...) (bound* ...) body* ...) > > Normal forall can be desugared to a bounded forall where the bound is the > Top of the data lattice (or S for success), i.e., there is no bound because > there are no constraints on the quantified variable. > > > Your example is a simpler version of an example from my first message, > which for reference was: > > (fresh (v w y z) (forall (x) (conde ((== 5 x) (== x w) (symbolo y)) ((=/= > 5 x) (== x v) (numbero z))))) > ==>* > (fresh (v w y z) (=/= 5 v) (== 5 w) (symbolo y) (numbero z)) > > It should be possible to work out how this works after seeing how yours > works. > > > I'll step through yours since it's less noisy. The way it works is, as > answers bubble up, the quantified variable is transferred to a new fresh > variable, and any constraints it had, are complemented and fed back into > the original forall as a more constrained bound. Once the bound becomes > Bottom (or F for fail), the process can stop with success. > > (not (fresh (x) (=/= x 1) (== x 1))) > ==> > (forall (x) (not (=/= x 1) (== x 1))) > ==> > (forall (x) > (conde ((== x 1)) ;; Let's bubble this branch up first. > ((=/= x 1)))) > ==> > (conde > ;; This is what the bubbled up branch became. > ( > ;; Transfer x to a new fresh variable. > (fresh (x0) (== x0 1) > > ;; Conjuct with the original forall... > (forall-bounded (x) ((=/= x 1)) ... bounded with x's constraint > complemented. > > (conde ((== x 1)) ;; The complemented branch will fail, as you'd > expect. > > ((=/= x 1)))))) ;; But (=/= x 1) is coincidentally > satisfiable here, allowing success. > > ;; This is what's left over from the original goal, after the first > branch was bubbled up. > ((forall (x) (=/= x 1)))) ;; It will end up failing, so we'll prune it > in the next step for clarity. > ==> > (conde > ((fresh (x0) (== x0 1) > (forall-bounded (x) ((=/= x 1)) > (conde (F) (S))))) > (F)) > ==> > (fresh (x0) (== x0 1) > (forall-bounded (x) ((=/= x 1)) S)) > ==> > (fresh (x0) (== x0 1) S) > ==> > (fresh (x0) (== x0 1)) ;; The fresh variable doesn't escape, so it's > uninformative. > ==> > S ;; This is success, by the way. > > > To be complete, let's look at the (forall (x) (=/= x 1)) case more > closely, which we pruned via hand-waving before: > > (forall (x) (=/= x 1)) > ==> > (fresh (x1) (=/= x1 1) > (forall-bounded (x) ((== x 1)) > (=/= x 1))) ;; This is going to fail under these bounds. > ==> > (fresh (x1) (=/= x1 1) F) > ==> > F > > > You can view forall operationally as a goal that attempts to obtain > complete domain coverage for its quantified variables, failing otherwise. > -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
