>
> I oversimplified the explanation of "swapping" substituion/disequalities.
> You right, additional efforts are required to handle `fresh` variables that
> apper under negation.
>
> First of all, I will admit, that when I execute `g` we consider its
> `fresh` variables as usual, but when I negate its answers I change my point
> of view on this variables and start to treat them like `universally`
> quantified. I do not consider these variables as `universal` on the fly
> because
> of cases like `forall (x) (x =/= 1) || (x == 1))` (which, taken my
> approach, executed as (not (fresh (x) (x == 1) && (x =/= 1) )).
>
> Substituion `x_1 = t_1 & ... & x_n = t_n` (if it contains bindings for
> `universal` variables) becomes not a regular disequality, but
> `anti-subsumption` constraint, or in other words constraint of the form
> `forall (x) (t =/= u)`. I've already meantioned that constraints in
> previous posts.
>
> In your example, after we get answer-substituion `x = 1`, it becomes
> constraint `forall (x) (x =/= 1)` which fails trivially (because there is
> such x = 1).
>
> When I "swap" disequality `x_1 =/= t_1 || ... || x_n =/= t_n` I first
> translate it to substutuion `x_1 = t_1 & ... & x_n = t_n`, but I also have
> to recheck and detect if `universal` variables escape their scope. It is
> not very smart, and I am not yet know how to perform this step more
> efficiently without rechecking of each binding.
>
I think you can automatically achieve the factoring I describe in the
rewrite examples, which might be more direct than what you have in mind.
States will track scope and maintain an order on variables based on the
order they're introduced. When variables introduced in newer scopes are
unified with variables in older scopes, the newer variable points to and
hands over ownership of its constraints to the older variable. By tracking
the 'fresh' scopes that a state has seen inside of a negation, the negation
will know to clean out (that is, fail) constraints involving these
variables, while complementing the others as usual, building a disjunction
out of whatever remains, as you do.
Example:
(fresh (v) ;; v is older than x.
...
(not (fresh (x) ;; state (x in scope)
(=/= 5 x) ;; state (x in scope): (=/= x 5)
(== x v))) ;; state (x in scope): (x points to v), (=/= v 5)
;; v has inherited x's =/= constraint.
...)
The negation sees this state bubble up to it:
state (x in scope): (x points to v), (=/= v 5)
Since x is in scope, the (x points to v) equality is thrown away as a
failure.
Since v is not in scope, (=/= v 5) is complemented to (v points to 5).
So you end up with a disjunction of (== v 5) and F.
This corresponds to the behavior of the factoring:
(fresh (v) ;; v is older than x.
...
(not (fresh (x) (=/= 5 x) (== x v)))
...)
==>
(fresh (v)
...
(not (fresh (x) (=/= 5 v) (== x v)))
...)
==>
(fresh (v)
...
(not (=/= 5 v) (fresh (x) (== x v)))
...)
==>
(fresh (v)
...
(conde ((== 5 v)) (F))
...)
In some cases, such as pair unifications, some juggling is necessary to
maintain the invariant that new variables always point to old. "Old" may
be the wrong description, since juggling may require generating new
variables in old scopes.
I'll show this in an example:
(fresh (v)
...
(not (fresh (x)
(== `(2 . ,x) v)))
...)
We don't want v to point to x. We can accomplish this with a complex
maneuver that then leads to simplicity. We can introduce a new tautology
relating v to pairs, using fresh variables to provide a layer of
indirection later on. (I think this is a general maneuver that should work
anytime we see such a pair unification.)
(fresh (v va vd) ;; va and vd are added here.
...
;; This conde is the tautology.
;; Since va and vd are newly added, they are guaranteed not to be
referenced anywhere except our tautology.
;; Therefore this goal implements the proposition: v is either a pair, or
not a pair.
(conde
((not-pairo v))
((== `(,va . ,vd) v)))
;; This goal will be absorbed into each conde clause.
(not (fresh (x)
(== `(2 . ,x) v)))
...)
==>
(fresh (v va vd)
...
(conde
((not-pairo v)
(not (fresh (x)
(== `(2 . ,x) v)))) ;; Since (not-pairo v), this will fail.
((== `(,va . ,vd) v)
(not (fresh (x)
(== `(2 . ,x) v))) ;; This can now be decomposed using va
and vd.
...)
==>
(fresh (v va vd)
...
(conde
((not-pairo v)
(not (fresh (x) F)))
((== `(,va . ,vd) v)
;; Now this fresh can produce a state where nothing points to x.
;; We saw how to handle negating such a fresh in an earlier example.
(not (fresh (x)
(== 2 va)
(== x vd)))
...)
==>
(fresh (v va vd)
...
;; This is the desired result, equivalent in meaning to (forall (x) (=/=
`(2 . ,x) v)). v isn't any pair with a car that is 2.
(conde
((not-pairo v))
((== `(,va . ,vd) v)
(=/= 2 va))
...)
I'm demonstrating using rewrites for clarity, but we should be able to
perform this maneuver with a running computation. One way is to allow v to
temporarily point to `(2 . ,x), then have the negation recognize this
situation, performing the tautology split itself.
Do you have a reason in mind that would make you want to wait until you
>> have all of g's answers first?
>>
>
> Well you right, In some cases it is possible to fail earlier and do not
> consume all stream. It is the case when `s_tmp = F` (F for the bottom of
> lattice), i.e. when none of conjuncts from answer `s_(i-1)` compatible with
> conjuncts from `s_i`.
>
> Note hovewer, that you should propogate each conjunct through the whole
> stream of answers, because it may be compatible with some other conjunct.
>
What do you mean by compatibility in this case? Are you looking for
unsatisfiability? Do you have an efficiency concern in mind (with an
example)?
--
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.
