> There is a restriction, of course. This kind of negation can only work with > finite-goals.
When you say finite goals, do you mean goals that produce a finite number of solutions, and which cannot diverge? On Wed, Dec 13, 2017 at 4:13 PM, William Byrd <[email protected]> wrote: > Thanks Evgenii! > > I find this work very interesting! > > 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? > > Also, is this especially difficult or computationally expensive to implement? > > 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?) > > Thanks! :) > > --Will > > > 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.
