CLP(Set)

CLP(Set) would be a welcome additions to the constraint solvers provided out of the box. It would remove the need for inefficient usage of membero you see so often in core.logic code.

CLP(Set) for completely ground sets is not difficult and could be accomplished easily via Constraints & Modes. However CLP(Set) which allows for partially instantiated sets would be extremly powerful and could support writing some very useful source analysis tools.

Imagine the following code:

(unionc seta setb oset)

If seta and setb are completely ground there's nothing more to do. But let's imagine seta and setb look like the following:

seta = #{:cat x y}
setb = #{:dog :bird z}

Here we have three fresh vars. There are some things we know immediately:

• x & y must be distinct from :cat and each other (distinctfd constraint)
• z must be distinct from :dog and :bird

oset can be of size 3, 4, 5 or 6.

These possibilities look something like this:

#{:cat :dog :bird}
#{:cat :dog :bird x}
#{:cat :dog :bird y}
#{:cat :dog :bird z}
#{:cat :dog :bird x y}
#{:cat :dog :bird x z}
#{:cat :dog :bird y z}
#{:cat :dob :bird x y z}

So if oset ever unifies with a set larger than count 6 or smaller than count 3 we can immediately fail. If oset ever unifies with a set of specific size we can discard the other possibilities which are not of that size. Where complications arise is that these possibilities alone are not enough, each possibility comes along with a permutation of variable assignments.

For example for the first case we have the following permutations of variable assignments:

x = :dog,  y = :bird, z = :cat
x = :dog,  y = :cat,  z = :bird
x = :bird, y = :dog,  z = :cat
x = :bird, y = :cat,  z = :dog
x = :cat,  y = :dog,  z = :bird
x = :cat,  y = :bird, z = :dog

We are already getting a taste of how this can get exponential. It seems though in general as the set size becomes larger the permutations are smaller, for example in the case of #{:cat :dog :bird x y} we know z must be :cat.

Still this is work we do not want to do unless we must. So we can take a page out of cKanren's book - we don't actually enumerate these possibilities until right before reification, by delaying this process we hope that we can constraint oset enough to eliminate pointless permutations.

There are many ways to constrain oset. If any of the involved vars becomes ground we know several things - a more refined notion of the set size, and which possibilities and permutations do not apply.

So we could imagine a series of new domain types to support CLP(Set), similar to how CLP(FD) has a series of data types. These domain types could store the size of the set as well as the remaining vars involved in permutations.

Note we could imagine the most complex case - the cartesian product of two these domains types, i.e.:

(unionc seta setb setc)

Where seta and setb are not ground and already have set domains. This will be slow if setc reaches reification without seta or setb becoming ground - and that should be expected.