Thanks for a detailed explanation !
It's much clearer now.
So, If I understand correctly that's what you do:
1) You treat forall(x) like eigen(x). Eigen variable can be unified with
itself or `fresh` variable that occurs deeper.
2) You propogate `not` down to primitive goals like unification,
constraints, etc, swapping conjuncts/disjuncts and fresh/forall on the road.
That's different from my approach, since I do not "propogate" negation on
the fly, but I try first to execute it in current state of search and then
"negate" answers.
Although, I think this two share a lot of common.
However, there are several details of your approach that is still unclear
to me.
1) How exactly `forall` interacts with constraints ? When you see `(forall
(x) (=/= `(2 . ,x) y))` you delay this goal as long as possible and then
replace it to
(conde ((not-pairo y)) ((fresh (a d) (== `(,a . ,d) y) (=/= 2 a)))) ?
2) What would be the answer to the following queries: `forall (x) (x ==
1)`, `forall (x) (x =/= 1)` ? Should they fail or not ?
3) Can you handle cases like : `forall (x) (conde (x == 1) (x =/= 1))` ?
Taken my approach, it can be viewed as (not (fresh (x) (x =/= 1) (x ==
1) )). The inner goal will fail and negation of failed goal is `success`.
How similar effect can be achieved with `on-the-fly` propagation of
`not` ?
четверг, 14 декабря 2017 г., 20:04:12 UTC+3 пользователь Greg Rosenblatt
написал:
>
>
> > 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.
