Since all user-defined relations and functions are invoked through
unification, we were able to handle
the relational-functional domain
extensions in a uniform, efficient manner
by building our first-class `dom`ain and `exc`lusion notions,
as well as the larger part of our `bnd`s, into the (pure LISP) unification
routine `unify` of the definitional interpreter of RELFUN.
(A smaller, less interesting part of occurrence bindings is
built into the term-instantiation routine, not treated here.)
In appendix A we use a meta-interpreter approach for specifying the
operational semantics of the extended `unify` via RELFUN clauses only relying on
non-extended unification. This will contain enough detail both to document
the actual RELFUN implementation and to permit transfers to
other LP languages.

While constants will stand for themselves, non-constant terms will be coded as ground lists as shown by the table below, where ``'' indicates recursive coding.

Substitutions will be represented as lists of pair lists of variables
and their values of the form , i.e. the empty
substitution becomes `[[bottom]]` (not `[]`, see below).

For instance, the call

successfully returns the substitutionunify( [bnd,[vari,x],[exc,a,b,c]], [dom,b,c,d,e], [ [bottom] ] )

In appendix A, the `unify` function takes two terms `X` and `Y` and a substitution `Environment`
(initially often empty),
and returns the substitution extended by the mgu of `X` and `Y` in `Environment`
(on success) or `[]` (on failure).
It calls `unify-ua` with `ultimate-assoc`-dereferenced
`X`/`Y` arguments for case analysis.
This workhorse decomposes one or two `bnd`s into their variable and
expression parts for `unify-bnd`, where a missing
`bnd` (variable) is indicated by `[]`.
Mixed `dom`/`exc` arguments are handed to `dom-exc`,
performing (set-as-list) subtraction.
Homogeneous `dom`s are handed to
`dom-intersection` for (set-as-list) intersection.
In both cases (only) the non-emptiness of the result list is
checked (so this can be optimized).
Homogeneous `exc`s are successful in any case.
Plain partner arguments to `dom`s and `exc`s
are checked via `member` calls simplifying earlier
cases with singleton `dom`s reduced to the plain argument.
The last `unify-ua` clause does `unify` on constructors
(incl. `tup`) and calls `unify-args` (not expanded here)
for corecursive processing of their arguments.
The `unify-bnd` function essentially parallels the `dom` and `exc`
cases of `unify-ua`, but hands subtraction, intersection,
and union results to `unify-bnd-env` for extension of the
`Environment` argument, using the variable(s) of the
`bnd`(s).
Such `bnd`s for `dom`/`exc`-variable updates
may be generated by the function `ultimate-assoc`:
it returns the dereferenced value of a variable in
`Environment`, except if the value is a `dom` or an `exc`,
in which case it creates a `bnd` pair of the variable
immediately preceding in the reference chain and of the
`dom` or `exc` expression.

While RELFUN's generalized `is`-primitive also automatically
profits from the `dom`/`exc`-enhanced unification,
for ordinary built-in
relations and functions the actual arguments
that are finite domains
have to be `multiplied out' (built-in calls cannot have exclusion
arguments); for built-in (constant-valued) functions the values then
have to be recollected into a new domain structure.

As we have seen in section 5.1, the transformation could be performed statically for user-defined operations, too, thus eliminating the domain extension for a non-enhanced LP implementation. However, this would lose the combinatorial efficiency advantage of finite domains. Also, their complementarity with finite exclusions, not allowing this treatment, would become occluded.

For a model-theoretic characterization [9] of programs containing first-class finite domains, the transformation could also be exploited semantically. Of course, a characterization via a domain-extended Herbrand base would be more `direct'. And again, leaving domains in the semantic kernel would allow to exploit the domain/exclusion complementarity.