Sunday, April 10, 2016

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(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


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

(Based on information from ).

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:


These predicates in must always succeed . For example:

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

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

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


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

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)
       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'.


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],
   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) :-

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.


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) :-

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) :-

Running this program result in the following output:

[4, 12, 18, 242]

No comments: