Меркурий: детерминизм и сопоставление с образцом - PullRequest
Новая
       31

Меркурий: детерминизм и сопоставление с образцом

4 голосов
/ 19 сентября 2011

У меня есть полудетерминированная функция.Когда я переписываю его, чтобы использовать сопоставление с образцом вместо оператора if, Меркурий говорит, что он становится недетерминированным.Я хотел бы понять, почему.

Оригинальный код: 

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

Пересмотренный код: 

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

Я привык думать о сопоставлении с образцом вSML, где 0 в случае A гарантирует, что в случае B N не равно 0. Работает ли Меркурий по-другому?Может ли быть вызван случай B, даже если N равно 0?(Я добавил предложение N \= 0 к случаю B в надежде сделать предикат полудетерминированным, но это не сработало.)

Есть ли способ записи этого предиката с сопоставлением с шаблоном, который также является полудетерминированным?

1 Ответ

8 голосов
/ 19 сентября 2011

Да, сопоставление с образцом Меркурия работает иначе, чем в SML.Меркурий довольно строг в своей декларативной семантике.Предикат с несколькими предложениями эквивалентен дизъюнкции всех тел (по модулю некоторые сложности для объединений в главах клаузулы), и значение дизъюнкции не зависит от порядка, в котором пишутся различные ветви дизъюнкции.На самом деле очень мало Меркурия влияет на его значение в том порядке, в котором вы пишете вещи (переменные состояния - единственный пример, который я могу придумать).

Так что, не помещая N \= 0 в тело, ваш предикат с двумя предложениямииспользование сопоставления с шаблоном является недетерминированным.Ничто не могло бы помешать nth(Tl, 0 - 1, X) быть действительным сокращением nth([_ | Tl], 0, X).

С N \= 0 вы идете по правильному пути.К сожалению, в то время как if A then B else C логически эквивалентен (A, B) ; (not A, C), вывод детерминизма Меркурия обычно не достаточно умен, чтобы понять обратное.

В частности, вывод детерминизма Меркурия не делаетпопытаться выяснить в целом, что два пункта являются взаимоисключающими.В этом случае ему известно, что N = 0 может быть успешным или неудачным в зависимости от значения N, и что N \= 0 может быть успешным или неудачным в зависимости от значения N.Так как он видит два разных пути успеха предиката и может потерпеть неудачу, он должен быть недетерминированным.Есть способы пообещать компилятору, что детминизм не тот, который он вывел бы, но в подобных случаях проще просто использовать if / then / else.

Случаи, когда вы можете использовать сопоставление с образцом без компилятора, думая, что у вас может быть несколько решений, когда вы сопоставляете одну переменную с несколькими разными конструкторами одного типа.Например: 

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

Это называется switch .Компилятор знает, что список имеет два конструктора (пустой список [] или ячейка cons [|]), и данный список может быть только одним из них, поэтому дизъюнкция (или несколько предложений предиката), которая имеетрука для обоих конструкторов должна быть детерминированной.Разъединение (несколько предложений) с падежами для некоторых, но не для всех конструкторов будет считаться полудетерминированным.

Меркурий также способен генерировать очень эффективный код для коммутаторов, а также уведомлять вас обо всех местахэто нужно изменить, когда вы меняете тип, добавляя новые случаи, поэтому считается хорошим стилем использовать переключатели там, где это возможно.Однако в таких случаях, как ваш, вы застряли с if / then / else.

...