Next: Exclusion Terms Up: Finite Domains and Exclusions Previous: Introduction

Domain Terms

As the predefined term for finite domains we will use variable-length dom structures. They are built from an arbitrary finite number, , of unordered, repetition-free constants, :

In general, dom structures can be used like ordinary terms.

The empty and singleton domains reduce as follows (unknown indicates failure):

In our RELFUN implementation, the behavior of dom structures is handled by an extension of the unification routine (cf. appendix A). This behavior will be described by employing RELFUN's generalized is-primitive for unification:

unifies (e.g. a variable) with the value of (e.g. another term).

For instance, the (left-to-right-ordered) conjunction

X is dom[1,2,3], X is dom[2,3,4,5]
initializes X with the three-element domain containing the integers 1, 2, and 3, and then intersects it with the four-element domain containing 2, 3, 4, and 5, thus specializing the X value to the two-element domain dom[2,3]. Similarly, the conjunction

X is dom[1,2,3], X is dom[2,3,4,5], X is dom[1,3,5]
specializes X to a singleton domain, i.e. is equivalent to

X is 3

X is dom[1,2,3], X is dom[2,3,4,5], X is dom[1,3,5],
                                                 X is dom[1,2,4,8]
fails since X now degenerates to the empty domain.

Note that all orders of successive domain constraining are (result-)equivalent, including the usual left-to-right order of PROLOG's implementation of SLD resolution, which we could thus keep for our domain implementation: information about the current domain specialization can always immediately be stored as variable values, and goals need never be delayed.

There is an analogy between our finite-domain structures and the well-known non-ground structures of LP: binding a variable to a finite-domain structure corresponds to binding a variable to a non-ground structure. In both cases, when unified with another such variable, its value may become specialized:

  1. Some elements of the domain structure may become deleted. (The domain structure can thus transmute to a single element.)
  2. Some inner variables of the non-ground structure may become bound. (The non-ground structure can thus become a ground structure.)

This extension thus preserves the `specializing-assignment' property of logic programming (a given value can be subsequently specialized, while arbitrary reassignment of a variable leads to failure).

Two conjunctions exhibit the analogy:

X is dom[1,2,3], Y is dom[2,3,4,5], X is Y
deletes 1 from X, 4 and 5 from Y, assigning dom[2,3] to X and Y.

X is f[A,B,3,4,5], Y is f[1,B,3,D,E], X is Y
binds A to 1, D and E to 4 and 5, respectively, assigning f[1,B,3,4,5] to X and Y.

Note that the final (right-most) result of domain specializations need not be a single value such as 3 but can still be a domain value such as dom[2,3], because such an `intensional answer' is perfectly legitmate in our language; lack of further specialization possibilities does not lead to `floundering' goals.

We can carry the analogy one step further. Instead of being assigned to a variable, a non-ground structure can occur directly everywhere a term can occur in a formula (e.g., within another structure). Such `anonymous use' can also be permitted for finite-domain structures. An anonymous non-ground structure or domain structure has the same advantages as an anonymous variable: by eliminating variable names, `single-occurrence' and `back-substitutable' variables (non-ground structures, domain structures) can be immediately identified as such, programs become more concise, and no spurious bindings will be created.

For instance, since the variables X and Y are only used as intermediate stores, the above conjunctions via back-substitution become single expressions:

dom[1,2,3] is dom[2,3,4,5]
succeeds, bindingless, with the intersection domain dom[2,3].

f[A,B,3,4,5] is f[1,B,3,D,E]
succeeds, not creating spurious bindings (just A = 1, D = 4, and E = 5), with the most general common non-ground structure f[1,B,3,4,5].

Next: Exclusion Terms Up: Finite Domains and Exclusions Previous: Introduction

Harold Boley & Michael Sintek (