lib-is_directives (SICStus Prolog)

10.19 Declaring determinacy attributes—`library(is_directives)`

This library module gives access to the information declared by is/2 directives. The is/2 declarations can be used for declaring arbitrary predicate attributes, but the main application is for declaring determinacy information, and this is what is described here.

10.19.1 Introduction

Determinacy, i.e. whether a call to a predicate can produce more than one solution on backtracking, is an important property for understanding the predicate and the code that uses it. For this reason it is desirable to describe the behavior in the documentation that accompanies a predicate.

The determinacy properties of a predicate can also be used by various tools, and for this reason it is possible to declare the determinacy of a predicate in a way that can be automatically processed by such tools. One example is the determinacy analyzer in the SPIDER IDE (see SPIDER), which uses the declared determinacy of a called predicate to improve the precision of the analysis of the caller in the common case that the caller does not have any determinacy declaration of its own.

The SICStus libraries contain determinacy declarations for most exported predicates. These can serve as useful examples.

Determinacy declarations are hints, i.e. they are meant to convey the expected behavior. Due to the dynamic nature of Prolog, almost any call can fail, throw an exception, or succeed more than once for reasons not directly related to the called predicate. Examples where these things can happen are timeouts (library(timeout)) and functionality that can cause goals to run when a variable is bound, e.g. freeze/2. For this reason, anything that uses determinacy declarations must be prepared to handle any runtime behavior, not just the behavior specified by the declarations.

10.19.2 Available Determinacy Annotations

The following determinacy attributes are available:

det: A call will always succeed exactly once. I.e. the number of solutions is expected to be one. This is probably the most common behavior.
semidet: A call will fail, or succeed exactly once. I.e. the number of solutions is expected to be zero or one. This can be used for for describing tests, e.g. X>Y.
multi: A call will succeed more than once. I.e. the number of solutions is expected to be one or more. This is uncommon, but could be used to describe the builtin repeat/0.
nondet: A call may fail or succeed any number of times. I.e. the number of solutions is expected to be zero or more. This is the most general determinacy information and is what must be assumed unless no other information is available.
failing: A call will fail. I.e. the number of solutions is expected to be zero. This is uncommon, but could be used to describe the builtin false/0.
throwing: A call is expected to throw an exception. This is similar to failing in that the number of solutions is expected to be zero but differs in situations where failure is treated specially, like if-then-else. This is uncommon, but could be used to describe the builtin throw/1 and some of the error reporting predicates in library(types).

10.19.3 Syntax of Determinacy Declarations

Determinacy is declared using directives that use is/2. Note that in this usage, is/2 has nothing to do with the arithmetic predicate of the same name.

The format of a determinacy directive is:

:- SPEC is ANNOTATION.

where ANNOTATION is one of the atoms used for determinacy annotation. The SPEC describes the predicate and can be either a predicate specification (like those used by the abolish/1 predicate) or a skeletal goal (like those used by the meta_predicate/1 directive).

Example:

% foo/2 is expected to always succeed, once, for any argument.
:- foo/2 is det.

foo(X, Y) :-
        Y = hello(X).

% bar/2, when called with a non-variable first argument,
% is expected to succeed at most once.
:- bar(+, ?) is semidet.

% bar/2, when called with a variable first argument,
% is expected to succeed any number of times.
:- bar(-, ?) is nondet.

bar('a', lowercase).
bar('A', uppercase).
…
bar('z', lowercase).
bar('Z', uppercase).

The SPEC tells which predicate is being annotated and, if it is a skeletal goal, it can restrict the declaration to only apply for the specified instantiation of the arguments. It can have one of the following forms:

Module:Name/Arity
Name/Arity: Module and Name should be atoms, Arity should be a non-negative integer. This predicate specification denotes the predicate Name with arity Arity in module Module, where Module defaults to the source module.
Module:Name(ARG1, ARG2, …, ARGN)
Name(ARG1, ARG2, …, ARGN): This skeletal goal denotes the predicate Name with arity N in the module Module, where Module defaults to the source module. The argument positions is typically used to indicate an instantiation pattern.

10.19.3.1 Specifying Instantiation Patterns

Many predicates have different determinacy depending on how their arguments are instantiated. This can be indicated using the skeleton goal form of specification, with each argument of the skeleton goal being one of the following:

+: Indicates that the argument is instantiated, i.e. it is not a variable when the predicate is called.
-: Indicates that the argument is uninstantiated, i.e. it is a variable when the predicate is called.
?
*: Indicates that the argument can be anything, i.e. the declared determinism is not affected by the instantiation of this argument

if the argument is a compound term with one argument (like + hello, or - Bar), only the functor is used when interpreting the argument. This makes it possible to use variables as descriptive names for the arguments, e.g.

:- parent_of(+Parent, -Child) is nondet.

Not only variables can be used as descriptions in this way, any term is accepted.

When declaring determinism, the skeleton argument only specifies whether an argument is a variable or not. This is different from whether the argument should be considered input or output (var(X) has only an input argument, but will often be called with a variable as input argument).

10.19.3.2 Declaring Meta Predicate Determinacy

The declarations above is sufficient for most predicates. However, they do not suffice for predicates whose determinism depends on an argument goal, like lists:maplist/2.

For such predicates, i.e. meta predicates that take a single closure (goal) argument, it is possible to specify different determinacy for each of the possible determinacies of the closure argument, as in the following example:

% The last argument of dolist/3 is a closure with two
% suppressed arguments that will be supplied using call/3.
:- meta_predicate dolist(*, *, 2).

% This is the expected mode, a determinate producer. In this
% case dolist/3 will also succeed exactly once.
:- dolist(+, -, det) is det.

% If the closure can fail, then dolist/2 can also fail.
:- dolist(+, -, semidet) is semidet.

% If the closure succeeds more than once, then so will dolist/2.
:- dolist(+, -, multi) is multi.

% If the closure always fails (a strange usage, indeed) then dolist/3
% can nevertheless succeed, when the input is an empty list.
:- dolist(+, -, failing) is semidet.

% In general, dolist/3 will be nondeterminate if the closure is
% nondeterminate.
% This declaration may seem redundant, but it may not be for some tools.
:- dolist(+, -, nondet) is nondet.

% dolist/3 calls the argument closure, which expects two extra
% arguments, on each pair of corresponding list elements
dolist([], [], _G_2).           % The closure is ignored here
dolist([X|Xs], [Y|Ys], G_2) :-
        call(G_2, X, Y),
        dolist(Xs, Ys, G_2).

:- square/2 is det. % always expected to succeed (once)
square(X, XX) :-
        XX is X*X.

%  Example use:
%  | ?- square_list([1,2,3], Squares).
%  Squares = [1,4,9] ?
%
% It can be inferred that this is expected to succeed exactly once.
square_list(Numbers, Squares) :-
        % Calls square(X,Y) on each X in Numbers and Y in Squares.
        % Since square/2 is 'det', the call do dolist/3 will
        % be considered 'det' as well.
        dolist(Numbers, Squares, square).

10.19.4 Using Determinacy Declarations

Since determinacy declarations by necessity are only hints, it is often better to focus on the expected behavior rather than the exact behavior when declaring determinism for a predicate.

Also, only very simple instantiation patterns can be specified, so it may be useful to pretend they indicate more than they actually do.

As an example, consider how to declare the determinacy of the builtin length(List, Length):

It will succeed at most once if the second argument is instantiated (It will succeed once if the first argument can be unified with a list of the specified length, otherwise it will fail), regardless of the instantiation of the first argument. This corresponds to the attribute semidet.
It will succeed exactly once if the first argument is a proper list and the second argument is a variable. This corresponds to the attribute det.
It will succeed more than once if the first argument is a partial list (i.e. is a variable or has a variable tail). This corresponds to the attribute multi.
Finally, it will throw an exception for some invalid inputs, but this is not specified with determinacy declarations (… is throwing is only meant for predicates expected to always throw an exception).

However, it is not possible to specify “proper list”, “partial list“ and non-list as instantiation patterns. On the other hand, it would be unfortunate to not be able to say anything about the determinacy of length/2.

In such cases it may make sense to pretend that ‘+’, the non-variable argument instantiation, means “a properly/fully instantiated input”, i.e. a “proper list” in the case of length/2. Similarly, it may make sense to pretend that ‘?’, any instantiation, means “a partially instantiated input”, i.e. a “partial list” in the case of length/2.

So, for the builtin length/2 it would make sense to specify the following determinacy declarations:

:- length(*, +) is semidet.     % this is precise
:- length(+, -) is det.         % pretend '+' means proper list
:- length(?, -) is multi.       % pretend '?' means partial list

It is up to the documentation accompanying the predicate, and any tools that use these declarations, to handle this appropriately.

10.19.5 Accessing Determinacy Declarations at Runtime

The determinacy declarations are saved when code is compiled or consulted and can be accessed when the code has been loaded. This could be used by documentation generators, smart debuggers, and many other purposes, not all of which documented. New uses may be added without notice, so you should ignore any recorded is/2 directive that you do not understand.

The loaded is/2 directives can be accessed using the following, non-determinate, predicate:

current_is_directive(Skel, M, Annotation, Spec, Directive, Context).

Skel: This is a compound term with the same name as the predicate and one anonymous variable in each argument position.
M: This is the module of the predicate specification. Typically the same as the source module.
Annotation: This is the second argument of the is/2 directive.
Spec: This is the first argument of the is/2 directive, with module prefixes peeled off.
Directive: This is the entire is/2 directive (without the surrounding :- ...).
Context: this is the source module.

Consider the following code:

:- module(example, [p1/3]).

:- p1/3 is det.
:- user:bar(+, +) is semidet.

This corresponds to the following two clauses of current_is_directive/6:

current_is_directive(p1(_,_,_),
                     example,
                     det,
                     p1/3,
                     (p1/3 is det),
                     example).
current_is_directive(bar(_,_),
                     user,
                     semidet,
                     bar(+,+),
                     (user:bar(+,+) is semidet),
                     example).

Exported predicates:

current_is_directive(Skel, M, Annotation, Spec, Directive, Context).: Low-level access to the information recorded by is/2 directives. See the library documentation for details.
current_is_directive(:MSkel, Annotation, Spec).: Like current_is_directive(Skel, M, Annotation, Spec, _, _) where M and Skel are the parts of the meta argument MSkel.

Send feedback on this subject.

10.19 Declaring determinacy attributes—library(is_directives)