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.
