Go to the first, previous, next, last section, table of contents.


Andorra execution

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:

  1. ground(A) where A is an argument of Pred
  2. nonvar(A) where A is an argument of Pred
  3. 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.
  4. 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.
  5. Term1 ?= Term2 which means "if the terms Term1 and Term2 are instantiated they unify"
  6. any test that does not unify variables, ( ==/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.

Usage and interface (andorra)


Go to the first, previous, next, last section, table of contents.