Finite Domains and Exclusions as First-Class Citizens

A recent RELFUN extension permits finite domains (generally, 'types')

as VALUES of variables, giving them a full 'first-class' status. The

separate type and value slots of 'destructive-assignment' (procedural)

languages are thus joined in 'specializing-assignment' (LP) languages:

type

/

procedural variable logical variable -- type/value

\

value

For example, an initial

X is dom[a,b,c], ... % assign the finite domain containing a, b, c to X

makes the domain act both as the X value (allowed as/in an intensional

answer) and as the X type (constraining possible further unifications).

Extending the conjunction,

..., X is d % try to assign d to X

fails (since d is not in the 'enumeration type' {a,b,c}), while

..., X is dom[c,d] % try to assign the finite domain of {c,d} to X

specializes the domain value of X to the ordinary value c (the

intersection result of the two domains, normalized via dom[c] = c).

For obtaining the below report, please email me your snail address.

Abstract:

Languages based on logical variables can regard finite domains, finite

exclusions, and, generally, types as values. Like a variable can be

bound to a non-ground structure which can be later specialized through

in-place assignment of some inner variables, it can also be bound to,

say, a domain structure which can be specialized later through

`in-place deletion' of some of its elements (e.g. by intersection with

other domain structures). While finite domains prescribe the elements

of a disjunctive structure, the complementary finite exclusions forbid

the elements of a conjunctive structure. Domains and exclusions can be

values of variables or occur inside clauses as/in terms or within an

occurrence-binding construct (useful to name arbitrary terms). In a

relational-functional language (e.g., RELFUN) they can also be

returned as values of functions. Altogether, domains and exclusions

become first-class citizens. Because they are completely handled by an

extended unification routine, they do not require delay techniques

needed in (more expressive) constraint systems. Still, their

backtracking-superseding `closed' representation leads to smaller

proof trees (efficiency), and abstracted, intensional answers

(readability). Anti-unification (for generalization) exchanges the

roles of domains and exclusions. The operational semantics of

domains, exclusions, and occurrence bindings is specified by a RELFUN

meta-unify function (and implemented in pure LISP).

AUTHOR = {Harold Boley},

TITLE = {{Finite Domains and Exclusions as First-Class Citizens}},

BOOKTITLE = {Fourth International Workshop on

Extensions of Logic Programming,

St. Andrews, Scotland, March 1993, Preprints and Proceedings},

EDITOR = {Roy Dyckhoff},

NOTE = {Also available as Research Report RR-94-07, Feb.\ 1994,

DFKI, P.\ O.\ Box 2080, D-67608 Kaisers\-lautern},

PUBLISHER = {Springer},

SERIES = {LNAI},

YEAR = {1994}

Quote:

}