The process that you described, i.e. when you propogate `not` throgh `conde` and then consider all pairs of negated conjuncts is really similar to what happens under the hood in my approach.
Let me show. Suppose you negate goal `g`, i.e. `(not g)` You first execute `g` and the consider all its answers (you can see stream of answers as a "big" disjunction) That is, if `g` returns stream `[s1, s2, ..., sn]` - is is really a `s1 || s2 || ... || sn`. Its negation should be `(not s1) && ... && (not sn)`. Each `si` is itself a formula of the form : x_1 = t_1 & ... & x_n = t_n \\ this is a substitution & (y_11 =/= u_11 \/ ... \/ y_1n =/= u_1n) \\ this is a single disequality & ... (here goes other disequalities) Negation of `si` then becomes: x_1 =/= t_1 || ... || x_n =/= t_n \\ substitution becomes a disequality || (y_11 = u_11 & ... & y_1n = u_1n) \\ each disequality becomes a substituion || ... (here goes other substituions) Then you need to consider all combinations of substituions/disequalities from different negated answers. The process can be done incrementally, i.e. first consider only `s_tmp := (not s1) || (not s2)`, then `s_tmp := s_tmp || (not s3)` etc. You should prune unsatisfiable subformulas as earlier as possible. I think, we can take my approach as `baseline` solution, since it is simplier. And then we can think, what parts of it can be done `on the fly` and what justifies `doing it on-the-fly`. A few words on my insight of problem. I was thinking about `not` and `forall` as a kind of `second-order` goals, that operates not on individual `states` but instead on `set of states` or `stream of states`. That's why I first executed `g` and then operated on its answers. пятница, 15 декабря 2017 г., 13:59:06 UTC+3 пользователь Greg Rosenblatt написал: > > > 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. >> > > Don't thank me yet. I need to issue some corrections. I found a gaping > hole in the approach I described. > > 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)) >> > > I was sloppy here. This example should actually fail because the (== x v) > isn't satisfiable when x must be everything other than 5. This is a better > example: > > (fresh (v w y z) > (forall (x) > (conde ((== 5 x) (== x w) (symbolo y)) > ((=/= 5 x) (=/= x v) (numbero z))))) ;; (== x v) changed > to (=/= x v) > ==>* > (fresh (v w y z) (== 5 v) (== 5 w) (symbolo y) (numbero z)) > > This also points out a shortcoming of my description of the bounded forall > operation. > > >> 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. >> > > This operational explanation needs to be fixed. Transferring to a fresh > variable is only sound when the quantified variable is unified with a > single value (without nested quantified variables). > > The problem exposed in the above example is that in (forall-bounded (x) > ((=/= 5 x)) ...), the (=/= 5 x) behaves as a *conjunction* of all > unifications with something other than 5 (in the normal situation with a > fresh x, =/= instead behaves like a disjunction of these unifications). > > > Here is a trace of the working example, which undoes forall via double > negation, then uses term rewritings that only involve not and fresh, making > it simpler to understand: > > (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) > (not (not (forall (x) > (conde ((== 5 x) (== x w) (symbolo y)) > ((=/= 5 x) (=/= x v) (numbero z))))))) > ==> > (fresh (v w y z) > (not (fresh (x) > (not (conde ((== 5 x) (== x w) (symbolo y)) > ((=/= 5 x) (=/= x v) (numbero z))))))) > ==> > (fresh (v w y z) > (not (fresh (x) > (conde ((=/= 5 x) (=/= x w) (not-symbolo y)))) > (conde ((== 5 x) (== x v) (not-numbero z))))))) > ==> ;; We enumerate all pairs of these conde clauses. > (fresh (v w y z) > (not (fresh (x) ;; We push fresh downward into the conde clauses. > ;; As answers bubble up, we stream a conjunction of their > negations. > ;; This is because we're working with (not (conde ...)). > (conde > ((=/= 5 x) (== 5 x)) > ;; ==> F > ;; (not F) > ;; ==> S > ((=/= 5 x) (== x v)) > ;; ==> (fresh (x) (=/= 5 x) (=/= 5 v)) > ;; v doesn't depend on x, so shrink the scope of fresh. > ;; ==> (and (fresh (x) (=/= 5 x)) (=/= 5 v)) > ;; (not (and (fresh (x) (=/= 5 x)) (=/= 5 v))) > ;; ==> (conde ((not (fresh (x) (=/= 5 x))) > ((not (=/= 5 v))) > ;; ==> (conde (F) ((== 5 v))) > ;; ==> (== 5 v) > ((=/= 5 x) (not-numbero z)) > ;; The pattern is the same as above so let's make this > shorter: > ;; ==>* (and (fresh (x) (=/= 5 x)) (not-numbero z)) > ;; (not (and (fresh (x) (=/= 5 x)) (not-numbero z))) > ;; ==>* (numbero z) > ((=/= x w) (== 5 x)) > ;; ==>* (and (fresh (x) (== 5 x)) (=/= 5 w)) > ;; (not (and (fresh (x) (== 5 x)) (=/= 5 w))) > ;; ==>* (== 5 w) > ((=/= x w) (== x v)) > ;; ==> (fresh (x) (=/= x w) (== x v)) > ;; ==> (fresh (x) (=/= v w) (== x v)) > ;; ==> (and (=/= v w) (fresh (x) (== x v))) > ;; (not ...) > ;; ==>* (== v w) > ((=/= x w) (not-numbero z)) > ;; Shorter still, now that we've seen enough patterns: > ;; (not ...) > ;; ==>* (numbero z) > ((not-symbolo y) (== 5 x)) > ;; (not ...) > ;; ==>* (symbolo y) > ((not-symbolo y) (== x v)) > ;; (not ...) > ;; ==>* (symbolo y) > ((not-symbolo y) (not-numbero z)) > ;; (not ...) > ;; ==>* (conde ((symbolo y)) ((numbero z))) > )))) > ==>* > (fresh (v w y z) > S > (== 5 v) > (numbero z) > (== 5 w) > (== v w) > (numbero z) > (symbolo y) > (symbolo y) > (conde ((symbolo y)) ((numbero z))) > ==> > ;; This time, we get the right result. > (fresh (v w y z) > (== 5 v) > (numbero z) > (== 5 w) > (symbolo y)) > > > Since soundness is clearer in this case, maybe we can operationalize this > rewriting process instead. It seems simpler than figuring out proper > treatment for forall-bounded. > -- 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.
