пятница, 15 декабря 2017 г., 18:11:16 UTC+3 пользователь Greg Rosenblatt написал: > > > Yeah, this is similar. But one thing I'm confused about is how this > handles situations such as (not (fresh (x) (== 1 x))). Normally, (fresh > (x) (== 1 x)) would lead to a substitution: > > x = 1 > > the negation of which becomes: > > x =/= 1 > > But what do you do then? It looks like this situation succeeds when it > should fail, due to x's scoping. >
I oversimplified the explanation of "swapping" substituion/disequalities. You right, additional efforts are required to handle `fresh` variables that apper under negation. First of all, I will admit, that when I execute `g` we consider its `fresh` variables as usual, but when I negate its answers I change my point of view on this variables and start to treat them like `universally` quantified. I do not consider these variables as `universal` on the fly because of cases like `forall (x) (x =/= 1) || (x == 1))` (which, taken my approach, executed as (not (fresh (x) (x == 1) && (x =/= 1) )). Substituion `x_1 = t_1 & ... & x_n = t_n` (if it contains bindings for `universal` variables) becomes not a regular disequality, but `anti-subsumption` constraint, or in other words constraint of the form `forall (x) (t =/= u)`. I've already meantioned that constraints in previous posts. In your example, after we get answer-substituion `x = 1`, it becomes constraint `forall (x) (x =/= 1)` which fails trivially (because there is such x = 1). When I "swap" disequality `x_1 =/= t_1 || ... || x_n =/= t_n` I first translate it to substutuion `x_1 = t_1 & ... & x_n = t_n`, but I also have to recheck and detect if `universal` variables escape their scope. It is not very smart, and I am not yet know how to perform this step more efficiently without rechecking of each binding. > It seems like there are missing details for tracking and accounting for > scope. Do you have something worked out for this case? > > >> 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. >>> >> > Your fix, for reference: `s_tmp := (not s1) && (not s2)`, then `s_tmp := > s_tmp && (not s3)` > > That we're streaming conjuncts rather than disjuncts is what allows us to > do this on the fly, incorporating each conjunct on demand as it bubbles out > of the negated goal. > > Do you have a reason in mind that would make you want to wait until you > have all of g's answers first? > Well you right, In some cases it is possible to fail earlier and do not consume all stream. It is the case when `s_tmp = F` (F for the bottom of lattice), i.e. when none of conjuncts from answer `s_(i-1)` compatible with conjuncts from `s_i`. Note hovewer, that you should propogate each conjunct through the whole stream of answers, because it may be compatible with some other conjunct. I haven't yet experimented with infinite streams under negation a lot. But you right. Definately, in some cases it is feasible to fail earlier. In fact, I use a kind of `fold-like` function on streams during negation, and consume answers one by one (just like `fold` on regular lists works). I've found this `fold` analogy very useful. But again, I haven't yet experimented with infinite streams. > > >> 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. >>> >> > This kind of stratification is common in settings with finite goals (e.g., > basic datalog with negation). It also lets you handle aggregation (sum, > min, max, etc.). > > In our setting, as long as we're not aggregating, we shouldn't have to > stratify. Incorporating each conjunct monotonically adds information. > > > By the way, I noticed a small mistake in my last trace, though it doesn't > change the result. I'll show the fix for future reference, then follow up > with some more motivation: > > >> ==> ;; 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) (== x v)) >>>> >>> ;; ==> (fresh (x) (=/= 5 x) (=/= 5 v)) >>>> >>> > This first step is wrong. It should be this: > > ==> (fresh (x) (=/= 5 x) (== x v)) > ==> (fresh (x) (=/= 5 v) (== x v)) > ==> (and (=/= 5 v) (fresh (x) (== x v))) > (not (and (=/= 5 v) (fresh (x) (== x v)))) > ==> (conde ((== 5 v)) ((not (fresh (x) (== x v))))) > ==> (conde ((== 5 v)) (F)) > ==> (== 5 v) ;; This is the same result as before. > > The strategy is to factor out goals that don't depend on x so that the > fresh scope can shrink, leaving behind the negation of an irrefutable > statement (negation of an irrefutable statement is a failure). In this > case that statement is: > > (not (fresh (x) (== x v)) > > Relative to the negation, this fresh is irrefutable because it's on the > inside of the negation, so x cannot escape to the rest of the program, and > because the unification can't fail, no matter what v is. > > > More motivation for on-the-fly processing: > > If we weren't able to factor out any other goals, the entire clause would > have been irrefutable, meaning the entire top-level negation would fail on > the spot. Looking at the bad example from before: > > (fresh (v w y z) > (forall (x) > (conde ((== 5 x) (== x w) (symbolo y)) > ((=/= 5 x) (== x v) (numbero z))))) ;; Note the (== x v) > instead of (=/= x v). > > This would have given us the conde clause ((=/= 5 x) (=/= x v)) instead > of what we just processed. This is how it progresses: > ==> (fresh (x) (=/= 5 x) (=/= x v)) ;; Nothing can be factored out. > (not (fresh (x) (=/= 5 x) (=/= x v))) ;; The entire clause is > irrefutable. Negating it leads to failure. > ==> F > > Consider a slightly different example with an infinite goal: > > (fresh (v w y z) > (forall (x) > (conde ((== 5 x) (== x w) (symbolo y)) > ((=/= 5 x) (== x v) (infinite-goal z))))) > > This motivates on-the-fly processing of negations. The early failure we > just saw can save us from having to process the infinite goal. > >> -- 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.
