Author(s): Claudio Vaucheret, Francisco Bueno.
This package allows modules execution under the Basic Andorra Model
[BibRef: andorra-principle]. The model classifies goals as
determinate, if at most one clause matches the goal, or
nondeterminate, otherwise. In this model a goal is delayed until
either it becomes determinate or it becomes the leftmost goal and no
determinate goal is available. The implementation of this selection
rule is based on the use of attributed variables
[BibRef: holzbaur-plilp92,holzbaur-phd].
In order to test determinacy, we verify only the heads of clauses and
builtins in the bodies of clauses before the first cut. By default,
when a goal is determinate, is detected dynamically, regarding the non
matching clauses each time a variable appearing in the goal is
instantiated.
In addition, efficiency can be improved by user directives setting the
determinacy conditions.
The directive:
:- determinate(Pred,Cond)
states than the predicate Pred
is determinate when Cond
holds. Cond
can be a single condition or conjunctions and
disjunctions of conditions. A single condition can be:
ground(A)
where A is an argument of Pred
nonvar(A)
where A is an argument of Pred
instatiated(A,Path)
which means that the subterm of A
addressed by Path
is not var. A
is an argument of
Pred
and Path
is a list of integer numbers describing a
path to the subterm regarding the whole term A as a tree. For example,
instantiated(f(g(X),h(i(Z),Y)),[2,1])
tests whether i(Z)
is
not var.
Term1 ?\= Term2
which means "if the terms Term1
and Term2 are instantiated they do not unify". Term1
and
Term2
can be either any argument of Pred
or a term
term(V,Path)
which refers to the subterm of V
addressed by Path
.
Term1 ?= Term2
which means "if the terms Term1
and Term2 are instantiated they unify"
==/2
, \==/2
, atomic/1
).
For example
:- determinate(member(A,B,C), ( A ?= term(B,[1]) ; C?\=[_|_]) ). member(A,[A|B],B). member(A,[B|C],[B|D]) :- A==B, member(A,C,D).
In this example, the directive states than the call member(A,B,C)
is determinate when A
doesn't unify to the first argument of B
or C
doesn't unify to [_|_]
.
It is possible to preserve the computation rule for calls to
predicates defined in other modules. These modules should obviously also
use this package. In addition all predicates from such modules should
imported, i.e., the directive :- use_module(module)
, should be used in
this case instead of :- use_module(module,[...])
. Otherwise calls to
predicates outside the module will only be called when they became the leftmost goal.
andorra
)Go to the first, previous, next, last section, table of contents.