> The process that you described, i.e. when you propogate `not` throgh
>> `conde` and then consider all pairs of negated conjuncts is really similar
>> to what happens under the hood in my approach.
>>
>> Let me show.
>> Suppose you negate goal `g`, i.e. `(not g)`
>>
>> You first execute `g` and the consider all its answers (you can see
>> stream of answers as a "big" disjunction)
>> That is, if `g` returns stream `[s1, s2, ..., sn]` - is is really a `s1
>> || s2 || ... || sn`.
>> Its negation should be `(not s1) && ... && (not sn)`.
>>
>> Each `si` is itself a formula of the form :
>> x_1 = t_1 & ... & x_n = t_n \\ this is a substitution
>> &
>> (y_11 =/= u_11 \/ ... \/ y_1n =/= u_1n) \\ this is a single disequality
>> &
>> ... (here goes other disequalities)
>>
>> Negation of `si` then becomes:
>> x_1 =/= t_1 || ... || x_n =/= t_n \\ substitution becomes a disequality
>> ||
>> (y_11 = u_11 & ... & y_1n = u_1n) \\ each disequality becomes a
>> substituion
>> ||
>> ... (here goes other substituions)
>>
>
Yeah, this is similar. But one thing I'm confused about is how this
handles situations such as (not (fresh (x) (== 1 x))). Normally, (fresh
(x) (== 1 x)) would lead to a substitution:
x = 1
the negation of which becomes:
x =/= 1
But what do you do then? It looks like this situation succeeds when it
should fail, due to x's scoping.
It seems like there are missing details for tracking and accounting for
scope. Do you have something worked out for this case?
> Then you need to consider all combinations of substituions/disequalities
>> from different negated answers.
>> The process can be done incrementally, i.e. first consider only `s_tmp :=
>> (not s1) || (not s2)`, then `s_tmp := s_tmp || (not s3)` etc.
>> You should prune unsatisfiable subformulas as earlier as possible.
>>
>
Your fix, for reference: `s_tmp := (not s1) && (not s2)`, then `s_tmp :=
s_tmp && (not s3)`
That we're streaming conjuncts rather than disjuncts is what allows us to
do this on the fly, incorporating each conjunct on demand as it bubbles out
of the negated goal.
Do you have a reason in mind that would make you want to wait until you
have all of g's answers first?
> A few words on my insight of problem. I was thinking about `not` and
>> `forall` as a kind of `second-order` goals, that operates not on individual
>> `states` but instead on `set of states` or `stream of states`. That's why I
>> first executed `g` and then operated on its answers.
>>
>
This kind of stratification is common in settings with finite goals (e.g.,
basic datalog with negation). It also lets you handle aggregation (sum,
min, max, etc.).
In our setting, as long as we're not aggregating, we shouldn't have to
stratify. Incorporating each conjunct monotonically adds information.
By the way, I noticed a small mistake in my last trace, though it doesn't
change the result. I'll show the fix for future reference, then follow up
with some more motivation:
> ==> ;; We enumerate all pairs of these conde clauses.
>>> (fresh (v w y z)
>>> (not (fresh (x) ;; We push fresh downward into the conde clauses.
>>> ;; As answers bubble up, we stream a conjunction of their
>>> negations.
>>> ;; This is because we're working with (not (conde ...)).
>>> (conde
>>> ...
>>>
>>
> ((=/= 5 x) (== x v))
>>>
>> ;; ==> (fresh (x) (=/= 5 x) (=/= 5 v))
>>>
>>
This first step is wrong. It should be this:
==> (fresh (x) (=/= 5 x) (== x v))
==> (fresh (x) (=/= 5 v) (== x v))
==> (and (=/= 5 v) (fresh (x) (== x v)))
(not (and (=/= 5 v) (fresh (x) (== x v))))
==> (conde ((== 5 v)) ((not (fresh (x) (== x v)))))
==> (conde ((== 5 v)) (F))
==> (== 5 v) ;; This is the same result as before.
The strategy is to factor out goals that don't depend on x so that the
fresh scope can shrink, leaving behind the negation of an irrefutable
statement (negation of an irrefutable statement is a failure). In this
case that statement is:
(not (fresh (x) (== x v))
Relative to the negation, this fresh is irrefutable because it's on the
inside of the negation, so x cannot escape to the rest of the program, and
because the unification can't fail, no matter what v is.
More motivation for on-the-fly processing:
If we weren't able to factor out any other goals, the entire clause would
have been irrefutable, meaning the entire top-level negation would fail on
the spot. Looking at the bad example from before:
(fresh (v w y z)
(forall (x)
(conde ((== 5 x) (== x w) (symbolo y))
((=/= 5 x) (== x v) (numbero z))))) ;; Note the (== x v)
instead of (=/= x v).
This would have given us the conde clause ((=/= 5 x) (=/= x v)) instead of
what we just processed. This is how it progresses:
==> (fresh (x) (=/= 5 x) (=/= x v)) ;; Nothing can be factored out.
(not (fresh (x) (=/= 5 x) (=/= x v))) ;; The entire clause is
irrefutable. Negating it leads to failure.
==> F
Consider a slightly different example with an infinite goal:
(fresh (v w y z)
(forall (x)
(conde ((== 5 x) (== x w) (symbolo y))
((=/= 5 x) (== x v) (infinite-goal z)))))
This motivates on-the-fly processing of negations. The early failure we
just saw can save us from having to process the infinite goal.
>
--
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.
