Hi Greg !
Thank you for a quick response !
> 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 =/=*.
Yeap, I was thinking about it too. I do not know about implementation of
=/=* (is this some special case of =/= ?)
As for Anti-Subsumption constraints, I was thinking about them exactly as a
way to reduce branching.
Instead of (e == Var x) || (e == Binop op e1 e2) || ... etc, we can simply
store the constraint forall (v) (e =/= Const v).
Is it what you also meant ?
> (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.
How do you simplify forall ? Is there some kind of preprocessing involved
(or macro, in terms of Lisp) ? Or `forall` works entirely at "runtime" ?
> 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)))))
This reminds me implementation of disequalitis from faster-minikanren. It
also breaks complex disequalities into simplier parts.
> (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))
Not sure I understood this example. What it meant to show ?
четверг, 14 декабря 2017 г., 17:25:45 UTC+3 пользователь Greg Rosenblatt
написал:
>
> 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.
>
> 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.
