I’m looking for the best way to constrain variables to a set of terms in a similar way freeze(X, member(X, [..values]) would. However, at some point later in the code I’d like to further refine these constraints in similar ways I would with CLP(FD), namely narrow the possible value set using eg. dif or introduce rules like "if X is foo then Y must/cannot be baz`. I could just freeze multiple goals on the variables, but this seems messy, especially considering that compound terms would require me to deal with partial instantiation.
What I would rather do is use a solution similar to clp(fd). Some examples of how it would be used:
Tense in [praes, pf, fut],
Mode in [ind, conj],
Tense #= fut #==> Mode #\= conj.
Decl in [1, 2, 3:a, 3:b],
% ...
Decl #= 3:_,
Decl #/= 1. % etc
In general this problem looks much more difficult than FD because of (possibly cyclic) compounds. Since my domain is much simpler, I also thought about creating a dedicated solution using eg. CHR but I’m unsure if that’s a suitable tool for this kind of task, so any tips on that are appreciated.
Lastly, this has some common points with typing and type constraints, but the focus is on constraining the answer space not correctness checks.
My first impression is to start with understanding the basics of attributed variable unification. That allows vetoing unifications. Here more importantly, it allows you to define a new constraint when two constrained variables are unified. In the unification hook you have access to the attribute value on both variables. If the attributes are incompatible you fail. Otherwise you either compute a concrete value from the joined attributes and bind the unified variables to this new value or you compute a new intersection that carries the combined attribute. How you do that is completely up to you.
In finite domain reasoning, regardless of the domain this boils down to
Compute the intersection of the two domains
When empty, fail
When the intersection contains a single value, unify to that value
Else set the domain to the new intersection.
clp(fd) does this for integers. You can do the same for concrete values represented in lists, ordered sets, assocs, etc. or for classes where you can reason about intersecting. In many of these domains the reasoning is way simpler than clp(fd). clp(fd) needs to deal with large domains (ranges of integers) as well as the semantics of all arithmetic operators it supports.
Just wanted to add that the same logic can be applied to non-finite domains, e.g., real numbers. The only caveat is that it’s generally impossible to have an intersection with a single value due to the infinite number of real values.
Due to the nature of joint constraints, I think you usually end up with a cyclic structure for constraint networks, i.e., variables are associated with a list of constraints that must be checked when something changes (possibly but not always unification since constraints can usually be added incrementally). These constraints reference other variables which are constrained similarly, so it’s fairly easy to see where cycles are formed. It all seems to work but it can be difficult to get your head around it.
Thinking a bit about this, this network appears when we have constrained variables that have some relation to one another, no. For example A = B + C (as mathematical relation) and we have a domain (or value) for each of these. Now we can reason about the semantics of the relation in combination to the domains and possibly decide that this can never work (no solution) or we can shrink some or the domains. This is called propagation, i.e. if the domain of C changes this has implications for (propagates to) the domains of A and B.
clpBNR is built on a set of relational interval arithmetic (RIA) primitives exactly as you describe. Attributes attached to A, B, and C would all reference the same primitive call if A = B + C. A narrowing of any one of them can trigger narrowing in the others, i.e., propagation.
I thought I’d give some update on how I solved this problem in my project: for simple cases of the form if X = value then Y cannot be other_value it’s enough to use a custom CHR constrain to relate them:
Used in code as constr(X, Y), this waits until X is instantiated and checks it against value. This approach is flexible enough for what I wanted to do, especially since I can constrain multiple variables that are closely related using a single constraint with multiple rules.