Lack of attention is temporary. ... Dan
On Thu, Dec 14, 2017 at 9:25 AM, Greg Rosenblatt <[email protected]> wrote: > Hi Evgenii, > > I've been working on negation too, and have an idea you might like. > > If you assume a closed universe of values/types (e.g., pairs, numbers, > symbols, (), #t, #f), you can make negation more precise, to the point where > you no longer need anti-subsumption goals, because you can break them down > into simpler parts (negated type constraints and =/=). > > For instance, we currently have numbero and symbolo, can express (pairo x) > as (fresh (a d) (== `(,a . ,d) x)), and can express the others using == on > atomic values. To these we can add not-numbero, not-symbolo, and not-pairo, > with =/= handling the atoms. > > > (not (fresh (x) (== t u))) still becomes (forall (x) (=/= t u)), but for any > structures t and u, we can further simplify to eliminate the forall. Here's > an example: > > (fresh (y) (forall (x) (=/= `(2 . ,x) y))) > ==> > (fresh (y) (conde ((not-pairo y)) ((fresh (a d) (== `(,a . ,d) y) (=/= 2 > a))))) > > There's a question of efficiency raised by the introduction of new > disjunctions. It's possible to keep some derived disjunctions in the > constraint store to avoid branching, much like we do for =/=*. In this way > it would also possible to efficiently implement the negated type constraints > as complements: disjunctions of positive type constraints. This is also > possible in an implementation that can defer or reschedule arbitrary goals. > > > What does this gain over anti-subsumption goals? There are situations where > you can pull structure out of the forall: > > (fresh (y) (forall (x) (=/= `(2 . ,x) `(y . ,x)))) > ==> > (fresh (y) (=/= 2 y)) > > > More generally: > > (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)) > > > When you can break 'forall' into a stream of conjuncted constraints like > this, you can refute some branches of search even when negating "infinite" > goals. > > > On Thursday, December 14, 2017 at 6:09:20 AM UTC-5, Evgenii Moiseenko wrote: >> >> > Can you give a couple of concrete examples of constructive negation in >> > OCanren? What is a simple but real example, and what do the answers >> > look like? >> >> Well, first of all negation of the goal, that have no fresh variables, is >> equivalent to same goal where all conjuncts/disjuncts and >> unifications/disequalities are swapped: >> >> run q >> (fresh (x y) >> (q == (x, y)) >> (x =/= 1) >> (y =/= 2) >> ) >> >> q = (_.0 {=/= 1}, _.1 {=/= 2}) >> >> run q >> (fresh (x y) >> (q == (x, y)) >> ~((x == 1) || (y == 2)) >> ) >> >> q = (_.0 {=/= 1}, _.1 {=/= 2}) >> >> But this is not very interesting. >> >> Consider the case when there is fresh variable under negation: >> >> run q >> ~(fresh (y) >> (q === [y]) >> ) >> >> q = _.0 {=/= [_.1]} >> >> ([y] is single-element list in OCanren) >> >> At first glance there is no difference from the following query: >> >> run q >> (fresh (y) >> (q =/= [y]) >> ) >> >> q = _.0 {=/= [_.1]} >> >> However, they really behave differently: >> >> run q >> (fresh (x) >> (q === [x]) >> ) >> ~(fresh (y) >> (q === [y]) >> ) >> >> --fail-- >> >> >> run q >> (fresh (x) >> (q === [x]) >> ) >> (fresh (y) >> (q =/= [y]) >> ) >> >> q = _.0 {=/= [_.1]} >> >> > And, is the resulting code fully relational? Can you reorder the >> > goals in conjuncts and disjuncts, and not affect the answers >> > generated? (Other than the standard divergence-versus-failure?) >> >> Yes, I suppose it is relational. The trick is that negation of goal can >> produce constraints (unlike Negation as a Failure). >> There is no difference: negate the goal and produce constraints first and >> then check them in following goals or do the opposite (in case when all >> goals terminate, of course). >> >> > Also, is this especially difficult or computationally expensive to >> > implement? >> >> Well, I don't think it is very difficult or requires a lot of changes in >> MiniKanren's core. >> There is basically two implementation challenges: >> >> 1) Anti-subsumption constraints (constraints of the form `forall (x) >> (t=/=u)). >> They can be veiwed as generalization of regular disequality >> constraints, that MiniKanren already has. >> In fact, this constraints are very useful on its own, since they allow >> to express facts like `forall (i) (e =/= Const i)` from my first example. >> >> 2) Negated goal constructor: `~g`. >> It takes goal `g` and produces new goal. >> This new goal should behave the following way: >> >> It takes state `st` and runs `g` on it obtaining stream of answers `[ >> st' ]`. >> Then it rearranges all conjuncts/disjuncts and >> unifications/disequalities in `[ st' ]` and obtains a stream of new >> "negated" states >> >> The insight here is to realize that every answer ` st' ` is more >> specialized than input ` st `. >> Because MiniKanren uses persistent data-structures, it is always >> possible to take "diff" of two states of search. >> In case of negation this "diff" will be all substituion's bindings and >> disequalities, produced by goal `g`. >> >> > When you say finite goals, do you mean goals that produce a finite >> > number of solutions, and which cannot diverge? >> >> Yes, the goal should produce finite number of solutions from current state >> of search >> (i.e. reordering of conjuncts of negated goal and positive goals may >> change divergency). >> >> четверг, 14 декабря 2017 г., 1:17:21 UTC+3 пользователь William Byrd >> написал: >>> >>> > >>> > On Wed, Dec 13, 2017 at 11:39 AM, Evgenii Moiseenko >>> > <[email protected]> wrote: >>> >> Hi everybody. I want to share some of my experiments with negation in >>> >> MiniKanren (OCaml's OCanren more precisely) that I was doing last >>> >> months. >>> >> >>> >> I've recently give a talk in my university about it, so I attach the >>> >> pdf-slides. >>> >> They contain some insight and motivating examples along with overview >>> >> of the >>> >> field (negation in logic programming), including >>> >> Negation-As-a-Failure, >>> >> Answer Set programming and so on. >>> >> >>> >> In this post I will give quick overview, those who are interested may >>> >> find >>> >> more details in pdf-slides. >>> >> >>> >> I want to begin with two motivating examples. >>> >> >>> >> First: suppose you have an AST-type (i will consider typed case of >>> >> MiniKanren in OCaml, but you can easily translate it to untyped >>> >> Racket) >>> >> >>> >> type expr = >>> >> | Const of int >>> >> | Var of string >>> >> | Binop of op * expr * expr >>> >> >>> >> >>> >> Now, suppose you want to express that some expression is not a const >>> >> expression. >>> >> Probably, you first attempt would be to use disequality constraints >>> >> >>> >> let not_consto e = fresh (i) (e =/= Const i) >>> >> >>> >> Unfortunately, this doesn't work as one may expect: >>> >> >>> >> run q ( >>> >> fresh (i) >>> >> (q == Const i) >>> >> (not_consto q) >>> >> ) >>> >> >>> >> That query will give answer >>> >> q = _.0 {=/= _.1} >>> >> >>> >> The reason is that disequality >>> >> >>> >> fresh (i) (e =/= Const i) >>> >> >>> >> roughly says that "there is an `i` such that `e =/= Const i`. >>> >> And for every `e == Const j` you always may pick such `i`. >>> >> What we need is to say that (e =/= Const i) for every `i`. >>> >> >>> >> We can express it in terms of unification >>> >> >>> >> let not_consto e = conde [ >>> >> fresh (x) >>> >> (e == Var x); >>> >> >>> >> fresh (op e1 e2) >>> >> (e == Binop op e1 e2); >>> >> ] >>> >> >>> >> >>> >> But that may became a little tedious if we have more constructors of >>> >> type >>> >> expr. >>> >> >>> >> Let's consider second example. Say we have 'evalo' for our expr's and >>> >> we >>> >> want to express that some expression doesn't evalute to certain value. >>> >> >>> >> (evalo e v) && (v =/= 1) >>> >> >>> >> >>> >> Pretty simple. >>> >> >>> >> But If we add non-determinism in our interpreter, that will no longer >>> >> work >>> >> (hint: Choice non-deterministically selects one of its branch during >>> >> evaluation). >>> >> >>> >> type expr = >>> >> | Const of int >>> >> | Var of string >>> >> | Binop of op * expr * expr >>> >> | Choice of expr * expr >>> >> >>> >> >>> >> The reason is that (evalo e v) && (v =/= 1) says that there is an >>> >> execution >>> >> of `e` such that its result in not equal to 1. >>> >> When there is only one execution of `e` its okay. >>> >> But if `e` has many "executions" we want to check that none of its >>> >> executions leads to value 1. >>> >> >>> >> That's how I end up with idea of general negation operator in >>> >> MiniKanren ~g. >>> >> >>> >> My first try was to use Negation is a Failure, NAF (that is very >>> >> common in >>> >> Prolog world). >>> >> However NAF is unsound if arguments of negated goal have free >>> >> variables. >>> >> >>> >> My second idea was to execute `g`, collect all its answers (that is, >>> >> all >>> >> pairs of subst and disequality store) and then, to obtain result of >>> >> `~g`: >>> >> "swap" diseqealities and substituion. >>> >> It turns out, that similar idea is known under the name "Constructive >>> >> Negation" in the world of logic programming and Prolog. >>> >> I've also attached some papers on subject to this post. >>> >> Idea is simple, but there are some delicate moments: >>> >> >>> >> 1) The single MiniKanren answer with substitution and disequalities >>> >> can be >>> >> viewed as a formula: x_1 = t_1 & ... & x_n = t_n & (y_11 =/= u_11 \/ >>> >> ... \/ >>> >> y_1n =/= u_1n) & ... & (y_n1 =/= u_n1 \/ ... \/ y_nn =/= u_nn) >>> >> Several answers to query are formulas of this form bind by >>> >> disjunctions. >>> >> During negation we shoud carefully swap conjunctions and >>> >> disjunctions. >>> >> >>> >> 2) The second moment, that I did not discover right away, is the use >>> >> of >>> >> `fresh` under negation. >>> >> Roughly speaking, `fresh` under negation should became a kind of >>> >> `eigen` >>> >> or `universal` quantifier. >>> >> However, I did not use eigen in my implementation. That's because >>> >> it's >>> >> overkill here. In case of negation these `universally` quantified >>> >> variables >>> >> can stand only in restricted positions. >>> >> Instead I use disequality constraints of more general form (also >>> >> knowns >>> >> as anti-subsumption constraints in the literature). >>> >> That is disequalities of the form `forall (x) (t =/= u). (t/u may >>> >> contain x-variable). >>> >> To solve this constraints one can try to unify `t` and `u`. If >>> >> they are >>> >> unifiable, and unification binds only universally quantified variables >>> >> - >>> >> constraint is doomed. >>> >> There is more efficient algorithm to incrementally refine these >>> >> constraints during search. It is based on disequality constraint >>> >> implementation in faster-minikanren. >>> >> I can share details, If someone is interested. >>> >> >>> >> With this kind of negation it is possible to solve both problems I've >>> >> mentioned earlier. >>> >> >>> >> There is a restriction, of course. This kind of negation can only work >>> >> with >>> >> finite-goals. >>> >> >>> >> Hope, someone will find it interesting and useful. >>> >> >>> >> -- >>> >> 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. > > -- > 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. -- 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.
