Next: Finite-Domain/Exclusion Functional Programming Up: Domains/Exclusions in Relation Previous: Facts and dom/exc

Clauses and bnd-to-is Reductions

A typed version of a well-known PROLOG program contains a rule with a non-single-occurrence variable X, whose head occurrence is domain-bound:


likes(john,bnd[X,dom[ann,mary,susan]]) :- likes(X,wine).
likes(dom[mary,peggy,susan],wine).
The query

likes(john,Whom)
here binds Whom to dom[mary,susan]. The query (indefinite even wrt john)

likes(dom[fred,john],bnd[Whom,dom[ann,susan,tina]])
binds Whom to susan (not selecting fred or john from the anonymous dom).

A `negatively' typed version of the program again contains a rule with a non-single-occurrence variable X, whose head occurrence is exclusion-bound:


likes(john,bnd[X,exc[mary,claire,linda]]) :- likes(X,wine).
likes(exc[mary,peggy,susan],wine).
The query

likes(john,Whom)
now binds Whom to exc[peggy,susan,mary,claire,linda]. The query

likes(dom[fred,john],bnd[Whom,dom[ann,susan,tina]])
binds Whom to dom[ann,tina] (again leaving ``fred or john'' anonymous).

A binding construct in a clause head can always be replaced by by introducing a new premise . If is further transformed to , applying a unary predicate corresponding to , the entire reduction is similar to the reduction of a sorted logic to an unsorted one.

Thus, the bnd/dom rule is equivalent to


likes(john,X) :- X is dom[ann,mary,susan], likes(X,wine).
and, with ann-mary-or-susan, to

likes(john,X) :- ann-mary-or-susan(X), likes(X,wine).
ann-mary-or-susan(dom[ann,mary,susan]).

Also, the bnd/exc rule is equivalent to


likes(john,X) :- X is exc[mary,claire,linda], likes(X,wine).
and, with not-mary-claire-and-linda, to

likes(john,X) :- not-mary-claire-and-linda(X), likes(X,wine).
not-mary-claire-and-linda(exc[mary,claire,linda]).

The reduced form can perform `type' checking only after unification, once the former bnd variable is bound. Unlike the transformation (in section 4) of


bnd[X,dom[1,2,3]] is dom[2,3,4,5]     % fact p(bnd[X,dom[1,2,3]]).
bnd[X,exc[1,2,3]] is dom[2,3,4,5]     % fact p(bnd[X,exc[1,2,3]]).
to the `pre-typing' (domain/exclusion-initializing, not possible for clause heads as indicated by the ``%''-comments)

X is dom[1,2,3], X is dom[2,3,4,5]  % X is dom[1,2,3] not in p(X).
X is exc[1,2,3], X is dom[2,3,4,5]  % X is exc[1,2,3] not in p(X).
the above bnd-to-is reduction thus performs `post-typing' (domain/exclusion-specializing, generally applicable), as in

X is dom[2,3,4,5], X is dom[1,2,3] % rule p(X) :- X is dom[1,2,3].
X is dom[2,3,4,5], X is exc[1,2,3] % rule p(X) :- X is exc[1,2,3].

Unfortunately, post-typed clauses no longer permit the selectivity of typed (e.g. domain-constrained or sorted) unification and WAM-indexing and of typed anti-unification (for generalization, see section 7). Also, at least if compared with the ``:''-infix syntax of bnd as usable for our versions of the PROLOG example,


likes(john,X:dom[ann,mary,susan]) :- likes(X,wine).
likes(john,X:exc[mary,claire,linda]) :- likes(X,wine).
the is-reduced formulations are less readable.

Combining post-typing with the reformulation of an is-assigned exclusion as a conjunction of solved disequalities (cf. in section 3), we can repeatedly transform any -ary-exc-head clause

to an equivalent unary-exc-body clause

(for anonymous exclusions we choose a new variable for ``''), representing

where the non-Horn-clause character engendered by the exc terms is revealed by the ``'' constraints preceding the ordinary premises.



Next: Finite-Domain/Exclusion Functional Programming Up: Domains/Exclusions in Relation Previous: Facts and dom/exc


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