While finite domains prescribe some constant of a disjunction, finite exclusions forbid every constant of a conjunction. Thus the constants in an exclusion structure are implicitly `negative'. If a variable is constrained by an exclusion and a domain assignment (in any order), both possibly singleton, the constants of the exclusion delete equal constants of the domain (set difference). If a variable is constrained by two exclusion assignments, their constants are taken together (set union), which specializes the original values.
Our predefined term for finite exclusions will be variable-length exc structures. They are again built from an arbitrary finite number, , of unordered, repetition-free constants, :
In general, also exc structures can be used like ordinary terms.
The empty exclusion reduces as follows (the anonymous variable, ``_'', indicates success):
A singleton exclusion cannot be reduced context-freely since its element represents a single `negative' constant, which has to await a unification partner.
In RELFUN, exc structures are again handled by an extension of the unification routine (cf. appendix A).
For instance, these conjunctions show three principal unifications of exc structures:
X is exc[1,2,3], Y is dom[2,3,4,5], X is Y X is dom[1,2,3], Y is exc[2,3,4,5], X is Y X is exc[1,2,3], Y is exc[2,3,4,5], X is YThe first binds X to an exclusion of 1, 2, and 3, Y to dom[2,3,4,5], and then subtracts the former from the latter, specializing both X and Y to dom[4,5]. The second symmetrically `excludes' 2 through 5 from dom[1,2,3], ultimately binding X and Y to dom or 1. The third leads to X and Y being bound to the united exclusion exc[1,2,3,4,5].
Note that an exclusion can result from unification only if both respective unification partners are exc structures. If one partner is a dom structure or a constant, either of these kinds of terms also appears in successful results; exc structures ``subtract and disappear''. Thus, the first result, dom[4,5], is a - sufficiently specialized - finite domain (``Only constants 4 or 5 are allowed''), while, say, exc[1,2,3,6,...] would not be a - sufficiently specialized - finite exclusion (``All constants but 1 and 2 and 3 and 6 and ... are allowed'').
Like for domains, we can choose any order of exclusion constraining, and thus keep the left-to-right order: the negative information of exclusions is also stored as part of the variable substitution, not with goals, which, again, need never be delayed. Also, if only exclusions are involved, the right-most result of exclusion specializations still is a `negative answer' such as exc[1,2,3,4,5]; if all intermediate values are identical singleton exclusions, a `negative singleton answer' such as exc arises.
Exclusions can also be used anonymously, with the same advantages as mentioned for anonymous domains (see end of section 2). For instance, shortening the above conjunctions, the expressions
exc[1,2,3] is dom[2,3,4,5] dom[1,2,3] is exc[2,3,4,5] exc[1,2,3] is exc[2,3,4,5]succeed bindingless with, respectively, the difference domain dom[4,5], the difference constant 1, and the united exclusion exc[1,2,3,4,5].
Summarizing the domain and exclusion constructs, a `domain assignment'
corresponds to the disjunction of -solved equalities
with ``='' being used like RELFUN's ``is'', while an `exclusion assignment'
corresponds to the conjunction of -solved disequalities (where shows that exclusions are negated domains)
with ``'' having no direct analogue in RELFUN. However, since in such conjunctions (in RELFUN written with ``,'' instead of ``'') exclusion values become united, the equivalent -ary exclusion assignment
naturally corresponds to the following conjunction of unary ones:
Thus, finite exclusions express negative information as values (`object-centered') that can be simply passed around and unified like positive information, while LP extensions via a ``'' connective (symmetric) suggest two-variable constraints like , normally entailing another layer of complexity such as the need to delay a disequality until a variable becomes bound. (A possible non-ground extension of exclusions for representing two-variable constraints will be discussed in section 9.)