search

rvs314 / faster-clpset-minikanren

A fast implementation of miniKanren with CLP(Set) constraints, disequality and absento, compatible with Racket and Chez.
MIT License
0 stars 0 forks source link

`!uniono` in `mk.scm` has `conde` clauses that overlap #4

Open webyrd opened 4 months ago

webyrd commented 4 months ago

!uniono in mk.scm has conde clauses that overlap:

;; Derived set constraints
(define (!uniono l r l+r)
  (fresh (N)
    (conde
     [(ino N l+r) (!ino N l) (!ino N r)]
     [(ino N r)   (!ino N l+r)]
     [(ino N l)   (!ino N l+r)])))

This definition will lead to duplicate answers when N is in r and l but not in l+r.

One way to avoid this overlap would be to explicitly enumerate all three cases: N in r but not in l; N in l but not in r; and N in both r and l.

Another way to avoid the overlap would be to leave !uniono as it is currently defined, but to change the last clause from 

[(ino N l)   (!ino N l+r)]

to

[(ino N l) (!ino N r) (!ino N l+r)]

This approach introduces asymmetry with respect to the 

[(ino N r)   (!ino N l+r)]

clause, though.

Other relations in the implementation of CLP(Set) might also have this issue of overlapping clauses.

rvs314 commented 4 weeks ago

This should be fixed by fcbb31b89c2749c3361b9fad175cb4b5c378614f