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.
