> > 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 ?
>
Yes, I think it's equivalent, but should be stored after extracting as much
structure as possible first.
> > (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" ?
>
Though some static simplification may be possible, I use 'simplify' to
describe operational behavior. So, this happens during 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.
>
Right, similar idea.
> > (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 ?
>
I was trying to show how constraints may be extracted from a forall in a
more complex case, by eliminating dependence on the universally quantified
variable.
Maybe I can motivate this better by exploring some examples involving an
overly-simplistic evalo, which is still "infinite" in an interesting way:
(define (literalo v)
(conde
((== #t v))
((== #f v))
((== '() v))
((numbero v))))
(define (evalo e v)
(conde
((== `(quote ,v) e))
((== e v) (literalo e))
((fresh (ea ed va vd)
(== `(cons ,ea ,ed) e)
(== `(,va . ,vd) v)
(evalo ea va)
(evalo ed vd)))))
Here are some results you would expect:
(run* (e) (evalo e 1))
===>
((('1)) ((1)))
(run* (_) (not (fresh (e) (evalo e 1))))
===>
()
(run 2 (v) (fresh (e) (evalo e v)))
==>
(((_.0)) ((#t)))
Here's a harder one that should be possible given our current definition of
evalo:
(run 1 (_) (not (fresh (v) (not (fresh (e) (evalo e v))))
===>
(((_.0)))
We can trace what should happen:
(run 1 (_) (not (fresh (v) (not (fresh (e) (evalo e v))))
==>
(run 1 (_) (forall (v) (fresh (e) (evalo e v))))
==>
(run 1 (_)
(forall (v)
(fresh (e)
(conde
((== `(quote ,v) e))
((== e v) (literalo e))
((fresh (ea ed va vd)
(== `(cons ,ea ,ed) e)
(== `(,va . ,vd) v)
(evalo ea va)
(evalo ed vd)))))))
==>
(run 1 (_)
(conde
((fresh (x y) (== `(quote ,x) y))) ;; The first answer bubbles up here.
((forall (v)
(fresh (e)
(conde
((== e v) (literalo e))
((fresh (ea ed va vd)
(== `(cons ,ea ,ed) e)
(== `(,va . ,vd) v)
(evalo ea va)
(evalo ed vd)))))))
Which produces an answer thanks to the quote rule, which doesn't constrain
v.
Here's another one we can do, that proves a stronger statement:
(run* (v) (not (fresh (e) (evalo e v))))
===>
()
Here's a trace of what will happen:
(run* (v) (not (fresh (e) (evalo e v))))
==>
(run* (v) (forall (e) (not (evalo e v))))
==>
(run* (v)
(forall (e)
(not
(conde
((== `(quote ,v) e))
((== e v) (literalo e))
((fresh (ea ed va vd)
(== `(cons ,ea ,ed) e)
(== `(,va . ,vd) v)
(evalo ea va)
(evalo ed vd)))))))
==>
(run* (v)
(forall (e)
(not (== `(quote ,v) e))
(not (== e v) (literalo e))
(not
(fresh (ea ed va vd)
(== `(cons ,ea ,ed) e)
(== `(,va . ,vd) v)
(evalo ea va)
(evalo ed vd)))))
==>
(run* (v)
(forall (e)
(=/= `(quote ,v) e) ;; This fails as it bubbles up.
(conde ((=/= e v)) ((not (literalo e))))
(forall (ea ed va vd)
(conde
((=/= `(cons ,ea ,ed) e))
((=/= `(,va . ,vd) v))
((not (evalo ea va)))
((not (evalo ed vd))))))))
==>
(run* (v)
F
(forall (e)
(conde ((=/= e v)) ((not (literalo e))))
(forall (ea ed va vd)
(conde
((=/= `(cons ,ea ,ed) e))
((=/= `(,va . ,vd) v))
((not (evalo ea va)))
((not (evalo ed vd))))))))
==>
(run* (v) F)
==>
()
It's interesting to consider what happens if evalo is changed so that its
quote clause is restricted to only allow quoted symbols.
(define (evalo e v)
(conde
((== `(quote ,v) e) (symbolo v))
((== e v) (literalo e))
((fresh (ea ed va vd)
(== `(cons ,ea ,ed) e)
(== `(,va . ,vd) v)
(evalo ea va)
(evalo ed vd)))))
We no longer have an immediate way to produce any v. Although they
should logically produce the same answers, If we try the above two queries
again, we will fail to produce the same answers unless we add stronger
inference capabilities to the search, such as proof by induction.
Here's the crucial trace step from the last example, this time with the
modified quote clause.
==>*
(run* (v)
(forall (e)
;; The quote case no longer fails immediately.
(conde ((=/= `(quote ,v) e))
((not-symbolo v)))
(conde ((=/= e v)) ((not (literalo e))))
(forall (ea ed va vd)
(conde
((=/= `(cons ,ea ,ed) e))
((=/= `(,va . ,vd) v))
((not (evalo ea va)))
((not (evalo ed vd))))))))
The problem is this query will act out something like Zeno's paradox while
gradually covering all cases of nested pairs. With induction, we would
refute the recursive instances of the original problem: (not (evalo ea va))
and (not (evalo ed vd)).
> четверг, 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.
