Next: Domains/Exclusions in Relation Up: Finite Domains and Exclusions Previous: Exclusion Terms

Occurrence Bindings

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).



Next: Domains/Exclusions in Relation Up: Finite Domains and Exclusions Previous: Exclusion Terms


Harold Boley & Michael Sintek (sintek@dfki.uni-kl.de)