> Thanks, Greg. I can see now. Sorry that it took several posts in order to
> explain it to me.
>
> Very interesting and clever idea. So there is a kind of distribution of
> complement information across different branches of conde under forall. I
> didn't think about it under this angle.
>
Don't thank me yet. I need to issue some corrections. I found a gaping
hole in the approach I described.
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))
>
I was sloppy here. This example should actually fail because the (== x v)
isn't satisfiable when x must be everything other than 5. This is a better
example:
(fresh (v w y z)
(forall (x)
(conde ((== 5 x) (== x w) (symbolo y))
((=/= 5 x) (=/= x v) (numbero z))))) ;; (== x v) changed
to (=/= x v)
==>*
(fresh (v w y z) (== 5 v) (== 5 w) (symbolo y) (numbero z))
This also points out a shortcoming of my description of the bounded forall
operation.
> 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.
>
This operational explanation needs to be fixed. Transferring to a fresh
variable is only sound when the quantified variable is unified with a
single value (without nested quantified variables).
The problem exposed in the above example is that in (forall-bounded (x)
((=/= 5 x)) ...), the (=/= 5 x) behaves as a *conjunction* of all
unifications with something other than 5 (in the normal situation with a
fresh x, =/= instead behaves like a disjunction of these unifications).
Here is a trace of the working example, which undoes forall via double
negation, then uses term rewritings that only involve not and fresh, making
it simpler to understand:
(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)
(not (not (forall (x)
(conde ((== 5 x) (== x w) (symbolo y))
((=/= 5 x) (=/= x v) (numbero z)))))))
==>
(fresh (v w y z)
(not (fresh (x)
(not (conde ((== 5 x) (== x w) (symbolo y))
((=/= 5 x) (=/= x v) (numbero z)))))))
==>
(fresh (v w y z)
(not (fresh (x)
(conde ((=/= 5 x) (=/= x w) (not-symbolo y))))
(conde ((== 5 x) (== x v) (not-numbero z)))))))
==> ;; 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) (== 5 x))
;; ==> F
;; (not F)
;; ==> S
((=/= 5 x) (== x v))
;; ==> (fresh (x) (=/= 5 x) (=/= 5 v))
;; v doesn't depend on x, so shrink the scope of fresh.
;; ==> (and (fresh (x) (=/= 5 x)) (=/= 5 v))
;; (not (and (fresh (x) (=/= 5 x)) (=/= 5 v)))
;; ==> (conde ((not (fresh (x) (=/= 5 x)))
((not (=/= 5 v)))
;; ==> (conde (F) ((== 5 v)))
;; ==> (== 5 v)
((=/= 5 x) (not-numbero z))
;; The pattern is the same as above so let's make this shorter:
;; ==>* (and (fresh (x) (=/= 5 x)) (not-numbero z))
;; (not (and (fresh (x) (=/= 5 x)) (not-numbero z)))
;; ==>* (numbero z)
((=/= x w) (== 5 x))
;; ==>* (and (fresh (x) (== 5 x)) (=/= 5 w))
;; (not (and (fresh (x) (== 5 x)) (=/= 5 w)))
;; ==>* (== 5 w)
((=/= x w) (== x v))
;; ==> (fresh (x) (=/= x w) (== x v))
;; ==> (fresh (x) (=/= v w) (== x v))
;; ==> (and (=/= v w) (fresh (x) (== x v)))
;; (not ...)
;; ==>* (== v w)
((=/= x w) (not-numbero z))
;; Shorter still, now that we've seen enough patterns:
;; (not ...)
;; ==>* (numbero z)
((not-symbolo y) (== 5 x))
;; (not ...)
;; ==>* (symbolo y)
((not-symbolo y) (== x v))
;; (not ...)
;; ==>* (symbolo y)
((not-symbolo y) (not-numbero z))
;; (not ...)
;; ==>* (conde ((symbolo y)) ((numbero z)))
))))
==>*
(fresh (v w y z)
S
(== 5 v)
(numbero z)
(== 5 w)
(== v w)
(numbero z)
(symbolo y)
(symbolo y)
(conde ((symbolo y)) ((numbero z)))
==>
;; This time, we get the right result.
(fresh (v w y z)
(== 5 v)
(numbero z)
(== 5 w)
(symbolo y))
Since soundness is clearer in this case, maybe we can operationalize this
rewriting process instead. It seems simpler than figuring out proper
treatment for forall-bounded.
--
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.
