What use does if_/3 have?

问题:

The predicate if_/3 seems to be fairly popular among the few main contributors in the Prolog part of Stack Overflow.

This predicate is implemented as such, courtesy of @false:

if_(If_1, Then_0, Else_0) :-
   call(If_1, T),
   (  T == true -> call(Then_0)
   ;  T == false -> call(Else_0)
   ;  nonvar(T) -> throw(error(type_error(boolean,T),_))
   ;  /* var(T) */ throw(error(instantiation_error,_))
   ).

However, I have been unable to find a clear, simple, and concise explanation of what this predicate does, and what use it has compared to e.g. the classical if-then-else construct of Prolog if -> then ; else.

Most links I have found directly use this predicate and provide little explanation as to why it gets used, that a non-expert in Prolog could understand easily.

回答1:

In old-fashioned Prolog code, the following pattern arises rather frequently:

predicate([], ...).
predicate([L|Ls], ...) :-
        condition(L),
        then(Ls, ...).
predicate([L|Ls], ...) :-
        \+ condition(L),
        else(Ls, ...).

I am using lists here as an example where this occurs (see for example include/3, exclude/3 etc.), although the pattern of course also occurs elsewhere.

The tragic is the following:

• For an instantiated list, pattern matching can distinguish the first clause from the remaining two, but it cannot distinguish the second one from the last one because they both have '.'(_, _) as the primary functor and arity of their first argument.
• The conditions in which the last two clauses apply are obviously mutually exclusive.
• Thus, when everything is known, we want to obtain an efficient, deterministic predicate that does not leave choice points, and ideally does not even create choice points.
• However, as long as not everything can be safely determined, we want to benefit from backtracking to see all solutions, so we cannot afford to commit to either of the clauses.

In summary, the existing constructs and language features all fall short in some way to express a pattern that often occurs in practice. Therefore, for decades, it seemed necessary to compromise. And you can make a pretty good guess in which direction the "compromises" usually go in the Prolog community: Almost invariably, correctness is sacrificed for efficiency in case of doubt. After all, who cares about correct results as long as your programs are fast, right? Therefore, until the invention of if_/3, this was frequently wrongly written as:

predicate([], ...).
predicate([L|Ls], ...) :-
        (    condition(L) ->
             then(Ls, ...).
        ;    else(Ls, ...).
        )

The mistake in this is of course that when the elements are not sufficiently instantiated, then this may incorrectly commit to one branch even though both alternatives are logically possible. For this reason, using if-then-else is almost always declaratively wrong, and stands massively in the way of declarative debugging approaches due to its violation of the most elementary properties we expect from pure Prolog programs.

---

Using if_/3, you can write this as:

predicate([], ...).
predicate([L|Ls], ...) :-
        if_(condition(L),
            then(Ls, ...),
            else(Ls, ...)).

and retain all desirable aspects. This is:

• deterministic if everything can be safely decided
• efficient in that it does not even create choice points
• complete in that you never incorrectly commit to one particular branch.

The price of this is rather affordable: As Boris mentioned in the comments, you need to implement a reification. I have now some experience with this and found it rather easy with some practice.

Good news everyone: In many cases, condition is of the form (=)/2, or (#=)/2, and the first even ships with library(reif) for free.

For more information, see Indexing dif/2 by Ulrich Neumerkel and Stefan Kral!

回答2:

Let's try to solve a simple problem using if_/3; for example, I will try to partition a list (sorted on a predicate p/2) in two lists: a prefix in which, for every element X, we have p(X, true), and a rest (in which, if the list was sorted on p/2, we would have p(X, false).

I will use the library reif as here. So, here is the complete code of my program:

:- use_module(reif).

pred_prefix(Pred_1, List, L_true, L_false) :-
        pred_prefix_aux(List, Pred_1, L_true, L_false).

pred_prefix_aux([], _, [], []).
pred_prefix_aux([X|Xs], Pred_1, True, False) :-
        if_(    call(Pred_1, X),
                (       True = [X|True0],
                        pred_prefix_aux(Xs, Pred_1, True0, False)
                ),
                (       True = [],
                        False = [X|Xs]
                )
        ).

The predicate passed to this meta-predicate will take two arguments: the first is the current list element, and the second will be either true or false. Ideally, this predicate will always succeed and not leave behind choice points.

In the first argument of if_/2, the predicate is evaluated with the current list element; the second argument is what happens when true; the third argument is what happens when false.

With this, I can split a list in leading as and a rest:

?- pred_prefix([X, B]>>(=(a, X, B)), [a,a,b], T, F).
T = [a, a],
F = [b].

?- pred_prefix([X, B]>>(=(a, X, B)), [b,c,d], T, F).
T = [],
F = [b, c, d].

?- pred_prefix([X, B]>>(=(a, X, B)), [b,a], T, F).
T = [],
F = [b, a].

?- pred_prefix([X, B]>>(=(a, X, B)), List, T, F).
List = T, T = F, F = [] ;
List = T, T = [a],
F = [] ;
List = T, T = [a, a],
F = [] ;
List = T, T = [a, a, a],
F = [] .

How can you get rid of leading 0's for example:

?- pred_prefix([X, B]>>(=(0, X, B)), [0,0,1,2,0,3], _, F).
F = [1, 2, 0, 3].

Of course, this could have been written much simpler:

drop_leading_zeros([], []).
drop_leading_zeros([X|Xs], Rest) :-
    if_(=(0, X), drop_leading_zeros(Xs, Rest), [X|Xs] = Rest).

Here I have just removed all unnecessary arguments.

If you would have to do this without if_/3, you would have had to write:

drop_leading_zeros_a([], []).
drop_leading_zeros_a([X|Xs], Rest) :-
    =(0, X, T),
    (   T == true -> drop_leading_zeros_a(Xs, Rest)
    ;   T == false -> [X|Xs] = Rest
    ).

Here, we assume that =/3 will indeed always succeed without choice points and the T will always be either true or false.

And, if we didn't have =/3 either, you'd write:

drop_leading_zeros_full([], []).
drop_leading_zeros_full([X|Xs], Rest) :-
    (   X == 0 -> T = true
    ;   X \= 0 -> T = false
    ;   T = true, X = 0
    ;   T = false, dif(0, X)
    ),
    (   T == true -> drop_leading_zeros_full(Xs, Rest)
    ;   T == false -> [X|Xs] = Rest
    ).

which is not ideal. But now at least you can see for yourself, in one single place, what is actually going on.

PS: Please read the code and the top level interaction carefully.