This package implements attributed variables. It provides a means of associating with variables arbitrary attributes, i.e. named properties that can be used as storage locations as well as to extend the default unification algorithm when such variables are unified with other terms or with each other. This facility was primarily designed as a clean interface between Prolog and constraint solvers, but has a number of other uses as well. The basic idea is due to Christian Holzbaur and he was actively involved in the final design. For background material, see the dissertation [Holzbaur 90].
To load the package, enter the query
| ?- use_module(library(atts)).
The package provides a means to declare and access named attributes of variables. The attributes are compound terms whose arguments are the actual attribute values. The attribute names are private to the module in which they are defined. They are defined with a declaration
:- attribute AttributeSpec, ..., AttributeSpec.
where each AttributeSpec has the form (Name/Arity). There must be at most one such declaration in a module Module.
Having declared some attribute names, these attributes can now be added, updated and deleted from unbound variables. For each declared attribute name, any variable can have at most one such attribute (initially it has none).
The declaration causes the following two access predicates to become
defined by means of the user:goal_expansion/3 mechanism. They take a
variable and an AccessSpec as arguments where an AccessSpec
is either +(Attribute), -(Attribute),
or a list of such.
The + prefix may be dropped for convenience.
The meaning of the +/- prefix is documented below:
Module:get_atts(-Var, ?AccessSpec)
+(Attribute)
-(Attribute)
Module:put_atts(-Var, +AccessSpec)
put_atts/2 are undone on backtracking.
+(Attribute)
-(Attribute)
A module that contains an attribute declaration has an opportunity to extend the default unification algorithm by defining the following predicate:
Module:verify_attributes(-Var, +Value, -Goals)
verify_attributes/3. Value is a non-variable term, or
another attributed variable. Var might have no attributes present
in Module; the unification extension mechanism is not
sophisticated enough to filter out exactly the variables that are
relevant for Module.
verify_attributes/3 is called before Var has
actually been bound to Value. If it fails, the unification is
deemed to have failed. It may succeed non-deterministically, in which
case the unification might backtrack to give another answer. It is
expected to return, in Goals, a list of goals to be called
after Var has been bound to Value.
verify_attributes/3 may invoke arbitrary Prolog goals, but
Var should not be bound by it. Binding Var will result
in undefined behavior.
If Value is a non-variable term, verify_attributes/3 will
typically inspect the attributes of Var and check that they are
compatible with Value and fail otherwise. If Value is
another attributed variable, verify_attributes/3 will typically
copy the attributes of Var over to Value, or merge them with
Value's, in preparation for Var to be bound to Value.
In either case, verify_attributes/3 may determine Var's
current attributes by calling get_atts(Var,List) with
an unbound List.
An important use for attributed variables is in implementing coroutining
facilities as an alternative or complement to the built-in coroutining
mechanisms. In this context it might be useful to be able to interpret
some of the attributes of a variable as a goal that is blocked on that
variable. Certain built-in predicates (frozen/2,
call_residue/2) and the Prolog top level need to access blocked
goals, and so need a means of getting the goal interpretation of
attributed variables by calling:
Module:attribute_goal(-Var, -Goal)
An important use for attributed variables is to provide an interface to constraint solvers. An important function for a constraint solver in the constraint logic programming paradigm is to be able to perform projection of the residual constraints onto the variables that occurred in the top-level query. A module that contains an attribute declaration has an opportunity to perform such projection of its residual constraints by defining the following predicate:
Module:project_attributes(+QueryVars, +AttrVars)
call_residue/2 in each module
that contains an attribute declaration. QueryVars is the list of
variables occurring in the query, or in terms bound to such variables,
and AttrVars is a list of possibly attributed variables created
during the execution of the query. The two lists of variables may or
may not be disjoint.
If the attributes on AttrVars can be interpreted as constraints,
this predicate will typically "project" those constraints onto the
relevant QueryVars. Ideally, the residual constraints will be
expressed entirely in terms of the QueryVars, treating all other
variables as existentially quantified. Operationally,
project_attributes/2 must remove all attributes from
AttrVars, and add transformed attributes representing the
projected constraints to some of the QueryVars.
Projection has the following effect on the Prolog top level. When the
top level query has succeeded, project_attributes/2 is called
first. The top level then prints the answer substition and residual
constraints. While doing so, it searches for attributed variables
created during the execution of the query. For each such variable, it
calls attribute_goal/2 to get a printable representation of the
constraint encoded by the attribute. Thus, project_attributes/2
is a mechanism for controlling how the residual constraints should
be displayed at top level.
Similarly during the execution of
call_residue(Goal,Residue), when Goal has
succeeded, project_attributes/2 is called. After that, all
attributed variables created during the execution of Goal are
located. For each such variable, attribute_goal/2 produces a
term representing the constraint encoded by the attribute, and Residue
is unified with the list of all such terms.
The exact definition of project_attributes/2 is constraint system
dependent, but see section Projection and Redundancy Elimination for details about projection in clp(Q,R).
In the following example we sketch the implementation of a finite
domain "solver". Note that an industrial strength solver would have
to provide a wider range of functionality and that it quite likely
would utilize a more efficient representation for the domains proper.
The module exports a single predicate
domain(-Var,?Domain) which associates Domain
(a list of terms) with Var. A variable can be queried for its
domain by leaving Domain unbound.
We do not present here a
definition for project_attributes/2. Projecting finite domain
constraints happens to be difficult.
:- module(domain, [domain/2]).
:- use_module(library(atts)).
:- use_module(library(ordsets), [
ord_intersection/3,
ord_intersect/2,
list_to_ord_set/2
]).
:- attribute dom/1.
verify_attributes(Var, Other, Goals) :-
get_atts(Var, dom(Da)), !, % are we involved?
( var(Other) -> % must be attributed then
( get_atts(Other, dom(Db)) -> % has a domain?
ord_intersection(Da, Db, Dc),
Dc = [El|Els], % at least one element
( Els = [] -> % exactly one element
Goals = [Other=El] % implied binding
; Goals = [],
put_atts(Other, dom(Dc))% rescue intersection
)
; Goals = [],
put_atts(Other, dom(Da)) % rescue the domain
)
; Goals = [],
ord_intersect([Other], Da) % value in domain?
).
verify_attributes(_, _, []). % unification triggered
% because of attributes
% in other modules
attribute_goal(Var, domain(Var,Dom)) :- % interpretation as goal
get_atts(Var, dom(Dom)).
domain(X, Dom) :-
var(Dom), !,
get_atts(X, dom(Dom)).
domain(X, List) :-
list_to_ord_set(List, Set),
Set = [El|Els], % at least one element
( Els = [] -> % exactly one element
X = El % implied binding
; put_atts(Fresh, dom(Set)),
X = Fresh % may call
% verify_attributes/3
).
Note that the "implied binding" Other=El was deferred until after
the completion of verify_attribute/3. Otherwise, there might be a
danger of recursively invoke verify_attribute/3, which might bind
Var, which is not allowed inside the scope of verify_attribute/3.
Deferring unifications into the third argument of verify_attribute/3
effectively serializes th calls to verify_attribute/3.
Assuming that the code resides in the file `domain.pl', we can use it via:
| ?- use_module(domain).
Let's test it:
| ?- domain(X,[5,6,7,1]), domain(Y,[3,4,5,6]), domain(Z,[1,6,7,8]).
domain(X,[1,5,6,7]),
domain(Y,[3,4,5,6]),
domain(Z,[1,6,7,8]) ?
yes
| ?- domain(X,[5,6,7,1]), domain(Y,[3,4,5,6]), domain(Z,[1,6,7,8]),
X=Y.
Y = X,
domain(X,[5,6]),
domain(Z,[1,6,7,8]) ?
yes
| ?- domain(X,[5,6,7,1]), domain(Y,[3,4,5,6]), domain(Z,[1,6,7,8]),
X=Y, Y=Z.
X = 6,
Y = 6,
Z = 6
To demonstrate the use of the Goals argument of
verify_attributes/3, we give an implementation of
freeze/2. We have to name it myfreeze/2 in order to
avoid a name clash with the built-in predicate of the same name.
:- module(myfreeze, [myfreeze/2]).
:- use_module(library(atts)).
:- attribute frozen/1.
verify_attributes(Var, Other, Goals) :-
get_atts(Var, frozen(Fa)), !, % are we involved?
( var(Other) -> % must be attributed then
( get_atts(Other, frozen(Fb)) % has a pending goal?
-> put_atts(Other, frozen((Fa,Fb))) % rescue conjunction
; put_atts(Other, frozen(Fa)) % rescue the pending goal
),
Goals = []
; Goals = [Fa]
).
verify_attributes(_, _, []).
attribute_goal(Var, Goal) :- % interpretation as goal
get_atts(Var, frozen(Goal)).
myfreeze(X, Goal) :-
put_atts(Fresh, frozen(Goal)),
Fresh = X.
Assuming that this code lives in file `myfreeze.pl', we would use it via:
| ?- use_module(myfreeze). | ?- myfreeze(X,print(bound(x,X))), X=2. bound(x,2) % side effect X = 2 % bindings
The two solvers even work together:
| ?- myfreeze(X,print(bound(x,X))), domain(X,[1,2,3]),
domain(Y,[2,10]), X=Y.
bound(x,2) % side effect
X = 2, % bindings
Y = 2
The two example solvers interact via bindings to shared attributed
variables only. More complicated interactions are likely to be found
in more sophisticated solvers. The corresponding
verify_attributes/3 predicates would typically refer to the
attributes from other known solvers/modules via the module prefix in
Module:get_atts/2.
Go to the first, previous, next, last section, table of contents.