Next: Conclusions Up: Finite Domains and Exclusions Previous: Domain and Exclusion

Operational Semantics

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 domain and exclusion notions, as well as the larger part of our bnds, 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


unify( [bnd,[vari,x],[exc,a,b,c]], [dom,b,c,d,e], [ [bottom] ] )
successfully returns the substitution [ [[vari,x],[dom,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 bnds 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 doms 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 excs are successful in any case. Plain partner arguments to doms and excs are checked via member calls simplifying earlier cases with singleton doms 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 bnds 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.



Next: Conclusions Up: Finite Domains and Exclusions Previous: Domain and Exclusion


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