Mercury: Determinism and Pattern Comparison

Question

I have a semi-deterministic function. When I rewrite it to use pattern matching instead of the if statement, Mercury says it becomes non-deterministic. I would like to understand why.

Source:

:- pred nth(list(T), int, T). :- mode nth(in, in, out) is semidet. nth([Hd | Tl], N, X) :- (if N = 0 then X = Hd else nth(Tl, N - 1, X)). 

Revised Code:

 :- pred nth(list(T), int, T). :- mode nth(in, in, out) is nondet. nth([Hd | _], 0, Hd). % Case A nth([_ | Tl], N, X) :- N \= 0, nth(Tl, N - 1, X). % Case B 

I'm used to thinking about pattern matching in SML, where 0 in case A will guarantee that in case of BN it is not 0. Does Mercury work differently? Can call B cause even if N is 0? (I added the sentence N \= 0 to case B in the hope of making the predicate semi-deterministic, but that did not work.)

Is there a way to write this predicate with pattern matching, which is also semi-deterministic?

Answer 1

Yes, mercury pattern matching works differently with SML. Mercury is quite strict in its declarative semantics. A predicate with several sentences is equivalent to the disjunction of all bodies (modulo some complications for unification in the chapters of the sentence), and the meaning of the disjunction does not depend on the order in which the different shoulders of the disjunction are written. In fact, very little Mercury matters, which is affected by the order you write (state variables are the only example I can think of).

Therefore, without putting N \= 0 in the body, your predicate with two sentences using pattern matching is non-deterministic. There would be nothing to stop nth(Tl, 0 - 1, X) as a valid abbreviation nth([_ | Tl], 0, X) .

With N \= 0 you get to the correct path. Unfortunately, although if A then B else C logically equivalent to (A, B) ; (not A, C) (A, B) ; (not A, C) , the conclusion about the determinant of Mercury is usually not smart enough to understand the opposite.

In particular, the conclusion about determinism Mercury does not try to find out at all that the two sentences are mutually exclusive. In this case, he knows that N = 0 can succeed or fail, depending on the value of N , and that N \= 0 can succeed or fail, depending on the value of N Since he sees two different paths for the predicate for success, and he can fail, he must be non-deterministic. There are ways to promise the compiler that detminism is not something that it could output, but in such cases it's easier to just stick to using if / then / else.

In cases where you can use pattern matching without a compiler, you can have several solutions when you map a single variable to several different constructors of the same type. For instance:

 :- pred some_pred(list[T]) is det. some_pred([]) :- something. some_pred([H | T]) :- something_else. 

This is called a switch. . The compiler knows that the list has two constructors (an empty list [] or cons cons [|] ), and this list can be only one of them, so the disjunction (or several predicate clauses) that has a hand for both constructors must be deterministic. A clause (multiple sentences) with cases for some, but not all constructors, will be deduced as semi-deterministic.

Mercury can also generate very efficient code for switches, and also notify you of all the places that need to be changed when you change the type, adding new cases, so it’s considered a good way to use switches where possible. In cases like yours, you are stuck if / then / else.