> 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] <javascript:>> 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] <javascript:>.
> >> To post to this group, send email to [email protected]
> <javascript:>.
> >> 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.
