понедельник, 18 декабря 2017 г., 16:21:59 UTC+3 пользователь Greg Rosenblatt написал: > > What do you mean by compatibility in this case? Are you looking for >>> unsatisfiability? Do you have an efficiency concern in mind (with an >>> example)? >>> >> >> What I was trying to say can be illustrated by following examples. >> >> Suppose, after (lazy) negation of individual states in stream we get the >> following stream: >> >> ((x == 1) || ... ) && ((x == 2) || ... ) && ... // here goes other >> conjuncts (probably, infinitely many) >> >> We start folding this stream, i.e we are trying to convert it from CNF to >> DNF. >> >> First, we try to combine (x == 1) and (x == 2). Since the formula is >> unsatisfiable, we can drop it and start to proceed with other disjuncts. >> >> But lets consider other case: >> >> ((x == 1) || ... ) && ((y == 2) || ... ) && ... >> >> >> Now (x == 1) && (y == 2) is satifiable, and we have to drag it through >> other `negated` answers. In the worst case, we have to drag (x == 1) >> through the whole stream. >> > > This sounds like you're switching search strategies to depth-first. Why > not consider each of these disjuncts like any other goal in a conjunction, > and benefit from interleaving? Are you noticing too much space usage? >
Hmmm, I just didn't think about it. I was thinking about negation as a operator that takes goal, executes it in current state, obtains stream of states and then folds it into another stream of states. But I think you right, I actually can build the resulting stream using `mplus` and interleaving search. I shoud try that. -- 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.
