There was a typo. Instead of `s_tmp := (not s1) || (not s2)`, then `s_tmp := s_tmp || (not s3)` read `s_tmp := (not s1) && (not s2)`, then `s_tmp := s_tmp && (not s3)`
пятница, 15 декабря 2017 г., 16:28:20 UTC+3 пользователь Evgenii Moiseenko написал: > > 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.
