> 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.
>
It's more flexible than the existing eigen implementation, which gives
forall-like behavior only when == is the only basic constraint.
2) You propogate `not` down to primitive goals like unification,
> constraints, etc, swapping conjuncts/disjuncts and fresh/forall on the road.
>
Right.
> 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)))) ?
>
I'm implementing a system with dynamic goal scheduling, which has the
luxury of being able to translate to the conde immediately without
branching (hypothetically, because I haven't implemented this approach to
negation yet). Complex goals like this conde are deferred by default, and
checked for satisfiability when dependency constraints are tightened. In
this case, y is the only dependency, and unifying y will trigger an update
for the conde.
For instance, (== 7 y) means the conde is irrefutable, and can be removed,
whereas (fresh (v) (== `(,v . 3) y)) instead will lead to the conde being
simplified to just (=/= 2 v).
> 2) What would be the answer to the following queries: `forall (x) (x ==
> 1)`, `forall (x) (x =/= 1)` ? Should they fail or not ?
>
These would both fail. Logically, forall will only succeed when its
variable could be any value from your data universe...
> 3) Can you handle cases like : `forall (x) (conde (x == 1) (x =/= 1))` ?
>
.. for instance, yes, (forall (x) (conde ((== x 1)) ((=/= x 1)))) will
succeed.
> 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` ?
>
Your solution is nice and straightforward in cases like this, and I'd
prefer this strategy where possible.
I'll describe an alternative approach that can handle more complex
situations on the fly, using bounded forall, which seems the least
"magical" of the approaches I've considered:
(forall-bounded (x* ...) (bound* ...) body* ...)
Normal forall can be desugared to a bounded forall where the bound is the
Top of the data lattice (or S for success), i.e., there is no bound because
there are no constraints on the quantified variable.
Your example is a simpler version of an example from my first message,
which for reference was:
(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))
It should be possible to work out how this works after seeing how yours
works.
I'll step through yours since it's less noisy. The way it works is, as
answers bubble up, the quantified variable is transferred to a new fresh
variable, and any constraints it had, are complemented and fed back into
the original forall as a more constrained bound. Once the bound becomes
Bottom (or F for fail), the process can stop with success.
(not (fresh (x) (=/= x 1) (== x 1)))
==>
(forall (x) (not (=/= x 1) (== x 1)))
==>
(forall (x)
(conde ((== x 1)) ;; Let's bubble this branch up first.
((=/= x 1))))
==>
(conde
;; This is what the bubbled up branch became.
(
;; Transfer x to a new fresh variable.
(fresh (x0) (== x0 1)
;; Conjuct with the original forall...
(forall-bounded (x) ((=/= x 1)) ... bounded with x's constraint
complemented.
(conde ((== x 1)) ;; The complemented branch will fail, as you'd
expect.
((=/= x 1)))))) ;; But (=/= x 1) is coincidentally
satisfiable here, allowing success.
;; This is what's left over from the original goal, after the first
branch was bubbled up.
((forall (x) (=/= x 1)))) ;; It will end up failing, so we'll prune it
in the next step for clarity.
==>
(conde
((fresh (x0) (== x0 1)
(forall-bounded (x) ((=/= x 1))
(conde (F) (S)))))
(F))
==>
(fresh (x0) (== x0 1)
(forall-bounded (x) ((=/= x 1)) S))
==>
(fresh (x0) (== x0 1) S)
==>
(fresh (x0) (== x0 1)) ;; The fresh variable doesn't escape, so it's
uninformative.
==>
S ;; This is success, by the way.
To be complete, let's look at the (forall (x) (=/= x 1)) case more closely,
which we pruned via hand-waving before:
(forall (x) (=/= x 1))
==>
(fresh (x1) (=/= x1 1)
(forall-bounded (x) ((== x 1))
(=/= x 1))) ;; This is going to fail under these bounds.
==>
(fresh (x1) (=/= x1 1) F)
==>
F
You can view forall operationally as a goal that attempts to obtain
complete domain coverage for its quantified variables, failing otherwise.
--
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.
