Determinism categories in Mercury

When you define a predicate in Mercury, you have to specify if it can fail or succeed more than once. This is called a determinism category.

The category is specified as part of a predicate (or function) declaration. For example:

:- pred get_partitions(
          list(int)::in,
              list(list(int))::out) is multi.

The is multi section says that this predicate belongs to the multi category.

The following tables describe the main determinism categories.

Maximum number of solutions:

Mode	1	> 1
det	x
multi		x
semidet	x
nondet		x

Failure:

Mode	Can fail?
det	no
multi	no
semidet	yes
nondet	yes

(Based on information from https://mercurylang.org/information/doc-latest/mercury_ref/Determinism-categories.html#Determinism-categories ).

Other categories exist : erroneous , failure, cc_mult and cc_nondet. These are not discussed in this post, see the link above for more info.

Now a some of each category:

det

These predicates in must always succeed . For example:

:- pred list_length(list(int)::in, int::out) is det.

list_length([_|R], Length) :-
   list_length(R,SubListLength),
   Length = SubListLength + 1.
list_length([], 0).

In this case this predicate is going to calculate the size of a list. It should not fail.

semidet

These predicates can either succeed or fail. For example the following code shows the definition of a first_even_number predicate.

:- pred first_even_number(list(int)::in, int::out) 
           is semidet.

first_even_number([X|R], N) :-
   (if (X mod  2) = 0 then
       N = X
    else
       first_even_number(R,N)).

Notice that this predicate can fail for a couple of reasons:

• The input list may be empty
• The input list may not contain an even number

I think it's pretty nice that you these situations will be handled without explicitly writing code for it.

A use of this predicate looks like this:

...
   (if first_even_number([3,41,5,32,342], EvenNumber) then
       io.write_string("First even number: ", !IO),
       io.write(EvenNumber, !IO)
    else
       io.write("Not even number found", !IO)
    ).

Another think that's pretty nice about Mercury is that, the compiler is going to detect inconsistent determinism annotations. For example, if I change the declaration of the predicate to:

:- pred first_even_number(list(int)::in, int::out) 
           is det.

The compiler is going to fail with the following error:

testsolutions.m:093: In `first_even_number'(in, out):
testsolutions.m:093:   error: determinism declaration not satisfied.
testsolutions.m:093:   Declared `det', inferred `semidet'.

multi

The multi category is used for predicates that succeed in multiple ways. At least one solution exists.

For example the following predicate is used to get a pair of lists that, when concatenated together, result in the input list (ex. [1,2,3] result in { [1],[2,3] }) .

:- pred partitions(list(int)::in, 
           {list(int), list(int)}::out) is multi.


partitions(InputList,Output) :-
(
   Output = {[] ,  InputList}
 ;
   InputList = [A|TMP],
   partitions(TMP,{R,B}),
   Output = { [A|R], B }
).

This predicate is multi because we can get several different pairs of lists that from an input list. For example:

main(!IO) :-
   solutions(partitions([513,242,355,4]),Pairs1),
   io.write(Pairs1,!IO),
   io.nl(!IO).

Running this program result in the following output:

[{[], [513, 242, 355, 4]}, {[513], [242, 355, 4]}, {[513, 242], [355, 4]}, {[513, 242, 355], [4]}, {[513, 242, 355, 4], []}]

In the case we use the solutions/2 Mercury predicate to get a list from the generated solutions.

It's important to note that multi predicates must not fail.

nondet

Finally the nondet category is used for predicates that result on 0 or many solutions.

For example the following predicate result on an even number that is part of the input list.

:- pred even_member(list(int)::in, int::out) is nondet.

even_member([X|_], X) :-
   (X mod  2) = 0.
even_member([_|Rest], X) :-
  even_member(Rest,X).

This predicate is nondet because :

• The list may be empty
• It may not contain an even number

Here's an example of how to use it:

main(!IO) :-
   solutions(even_member([513,242,18,355,12,4]),Pairs1),
   io.write(Pairs1,!IO).

Running this program result in the following output:

[4, 12, 18, 242]