Let us further introduce a generally useful construct for binding a variable to some (initial) value(s) at one or more of its occurrences in arbitrary formulas. If this is a type-like value, e.g. a non-ground structure or a domain or an exclusion, it can become specialized by subsequent unification.
Occurrence bindings are written as binary bnd structures built from a variable, , and a term, :
In general, bnd structures can be used as terms.
Taking a non-ground-structure example,
bnd[X,f[A,B,3,4,5]] is f[1,B,3,D,E]binds X to f[A,B,3,4,5], which is then unified with f[1,B,3,D,E], binding A to 1, D and E to 4 and 5, respectively, thus specializing the X value to f[1,B,3,4,5].
An analogous finite-domain example,
bnd[X,dom[1,2,3]] is dom[2,3,4,5]binds X to dom[1,2,3], which is then unified with dom[2,3,4,5], thus specializing the X value to dom[2,3].
A complementary finite-exclusion example,
bnd[X,exc[1,2,3]] is dom[2,3,4,5]binds X to exc[1,2,3], which is then unified with dom[2,3,4,5], thus specializing the X value to dom[4,5].
If the unification partner of an occurrence binding is directly given, here as the is-rhs (right-hand side), the bnd structure can always be equivalently replaced by an initializing (`pre-typing') is call:
X is f[A,B,3,4,5], X is f[1,B,3,D,E] X is dom[1,2,3], X is dom[2,3,4,5] X is exc[1,2,3], X is dom[2,3,4,5]For bnds in clause heads, however, the unification partner is not directly given, as will be illustrated by the relational examples in section 5.2.
The binding construct, pairing a variable with a value, can again be assigned to a variable. Actually, in our implementation it is generated from dom/exc-bound variables at the end of reference chains to keep track of domain/exclusion specializations (while non-ground structures can be specialized via direct in-place assignments).