Module 5, part 5

Module 5

Determinism and equality in list processing

count_elems_acc/3 revisited

Amongst the queries we gave for count_elems_acc/3 was:

     | ?- count_elems_acc(List, 0, 3).

     List = [_A,_B,_C] ? 

     yes

Note that we did not ask for any alternative solutions. This was quite deliberate. Look again at the procedures:

     % 1 terminating condition
     count_elems_acc([], Total, Total).
     % 2 recursive
     count_elems_acc([Head|Tail], Sum, Total) :-
          Count is Sum + 1, 
          count_elems_acc(Tail, Count, Total).

We'll look at the output of the demo version of this program, demo_count_elems_acc/3 for this query:

     | ?- demo_count_elems_acc(List, 0, 3).
          Before recursion at depth 1
             List is: [_196|_197]
             Count is: 0
             Total is: 3
               Before recursion at depth 2
                  List is: [_708|_709]
                  Count is: 1
                  Total is: 3
                    Before recursion at depth 3
                       List is: [_1480|_1481]
                       Count is: 2
                       Total is: 3
                         At the termination condition
                            List is: []
                            Count is: 3
                            Total is: 3
                    After recursion at depth 3
                       List is: [_1480]
                       Count is: 2
                       Total is: 3
               After recursion at depth 2
                  List is: [_708,_1480]
                  Count is: 1
                  Total is: 3
          After recursion at depth 1
             List is: [_196,_708,_1480]
             Count is: 0
             Total is: 3
     
     List = [_A,_B,_C] ?

The key to understanding what is going on is to understand what is happening to the first argument. In the query, the first argument is an uninstantiated variable:

     | ?- demo_count_elems_acc(List, 0, 3).

Remember that an uninstantiated variable will unify with anything. Now look at the heads of the two rules:

     % 1 terminating condition
     count_elems_acc([], Total, Total).
     % 2 recursive
     count_elems_acc([Head|Tail], Sum, Total) :- ...

We can test the unification of the heads of the rules with the query by typing the following into the Prolog interpreter:

     | ?- count_elems_acc([], Total, Total) = count_elems_acc(List, 0, 3).

     no
     | ?- count_elems_acc([Head|Tail], Sum, Total) = count_elems_acc(List, 0, 3).

     Sum = 0,
     List = [Head|Tail],
     Total = 3 ? ;

     no

The first fails because Total can't simultaneously be instantiated to 0 and 3; the second succeeds because this condition isn't specified. The interesting thing is that List has been instantiated to [Head|Tail], ie a list with variables as head and tail.

We could repeat this exercise for each stage of recursion, but next we'll look at the unification of the heads when the recursive call is:

     count_elems_acc(_1481, 3, 3).

As before, we'll try each in turn:

     | ?- count_elems_acc([], Total, Total) = count_elems_acc(_1481, 3, 3).

     Total = 3 ? ;

     no
     | ?- count_elems_acc([Head|Tail], Sum, Total) = count_elems_acc(_1481, 3, 3).

     Sum = 3 
     Total = 3 

     no

We would expect the terminating condition to unify, but we may be surprised that the recursive condition also unifies with the sub-goal. (It unifies because Sum and Total may or may not have the same instantiation.)

We'll now look at what happens if we require a second solution to the query:

     count_elems_acc(List, 0, 3).

The output of the demo version of the procedure restarts at depth 4, the level of recursion of the terminating condition for this query:

                    Before recursion at depth 4
                       List is: [_2512|_2513]
                       Count is: 3
                       Total is: 3
                         Before recursion at depth 5
                            List is: [_3804|_3805]
                            Count is: 4
                            Total is: 3
                              Before recursion at depth 6
                                 List is: [_5356|_5357]
                                 Count is: 5
                                 Total is: 3
                                   Before recursion at depth 7
                                      List is: [_7168|_7169]
                                      Count is: 6
                                      Total is: 3
                                        Before recursion at depth 8
                                           List is: [_9240|_9241]
                                           Count is: 7
                                           Total is: 3
                                             Before recursion at depth 9
                                                List is: [_11572|_11573]
                                                Count is: 8
                                                Total is: 3

at which point, we are clearly in infinite recursion, so I stopped the run.

Why has Prolog gone off into infinity? There are two kinds of answers to this. The first is at the practical level: when the second solution is requested, the recursive rule is used. This adds 1 to Count. Now Count is greater than Total and the terminating condition can never unify with anything this recursive rule will produce.

The second kind of answer is the real point of this example. The procedure is poorly written. The terminating condition is fine: it specifies very precisely what is to happen when the counter and the total are equal. The recursive condition is poorly written. It clearly is supposed only to be applicable when the counter is less than the total, but this nowhere specified. To correct the problem, we should make a new version:

     % 1 terminating condition
     count_elems_acc_correct([], Total, Total).
     % 2 recursive
     count_elems_acc_correct([Head|Tail], Sum, Total) :-
          Sum < Total,
          Count is Sum + 1, 
          count_elems_acc_correct(Tail, Count, Total).

When we try the query again, we get the solution we intend:

     | ?- count_elems_acc_correct(List, 0, 3).

     List = [_A,_B,_C] ? ;

     no

Take time to work through the Self-Test 8

An alternative way of looking at clauses in a procedure

One way of thinking about clauses in a procedure is in terms of sets. Take count_elems_acc/3 as an example. Then we can let:

        A = {all possible unifications with % 1}
        B = {all possible solutions with % 2}

So set A should include instances such as:

     count_elems_acc([], 0, Total)
     count_elems_acc(List, 0, 3)

Set B should include

     count_elems_acc([a,b,c], 0, Total)
     count_elems_acc(List, 0, 3)

From this rather inexhaustive example, we can see:

In the rewritten version, count_elems_acc_correct/3, we achieved:

If A union B is the universal set, then B = ¬A or to put it another way, B is the complement of A, written as A'.

It is often useful to think about clauses within procedures in terms of set relations. However, it should be realised that one of Prolog's strengths is its capability to handle non-deterministic situations which, in turn, presupposes that clauses within procedures aren't mutually exclusive.

Multiple answers and memb/2

The definition of memb/3 given so far is:

     % 1 terminating condition
     memb(Elem, [Elem|_]).
     % 2 recursive
     memb(Elem, [_|Tail]) :-
          memb(Elem, Tail).

We'll embed this within a small program which is rather trivial, but makes helps to make the relevant point:

     small_prog(Elem, List, Output) :-
          memb(Elem, List),
          Output = Elem.

If we try a query such as:

     | ?- small_prog(a, [a,b,b,a], Res).

     Res = a ? ;

     Res = a ? ;

     no

we can see that Prolog will give two solutions. It does this because the recursive clause will unify with anything that the terminating condition will unify with. This is illustrated by the following query which attempts to unify the heads of the two clauses of memb/3:

     | ?- memb(Elem, [Elem|_]) = memb(Elem, [_|Tail]).

     true ? ;

     no

There are various views about this behaviour. It seems pointless to get into discussions about whether it is "correct" for Prolog to give one solution to examples like the above or whether it should give as many as possible: the answer presumably is that it depends on what you want the program to do. For some purposes it is merely necessary to know that a particular element occurs at least once in a list; for other purposes it is necessary to retrieve every instance.

It should be remembered that when a program is backtracking, a non-deterministic procedure like memb/3 will be exhaustively searched each time it is encountered. This can be very time-consuming.

It is possible to write deterministic version of memb/3 simply by insisting that within the recursive clause, it is required that the Elem being sought and the Head of the list don't unify:

     % 1 terminating condition
     memb_det(Elem, [Elem|_]).
     % 2 recursive
     memb_det(Elem, [Head|Tail]) :-
          \+ (Elem = Head),
          memb_det(Elem, Tail).

'\+' is Prolog's way of writing "not". If we now use this procedure with small_prog/2, we can see that there is only one solution given.

Take time to work through the Self-Test 9

Unification and equality again

The example of memb/2 and memb_det/2 both matched the sought Elem and the Head using unification (ie =/2). However, this is not the only criterion we may wish to use. For instance, we may want to insist on strict equality, ==/2. I've written both a non-deterministic and deterministic version:

     % 1 terminating condition
     memb_eq(Elem, [Head|_]) :-
          Elem == Head.
     % recursive
     memb_eq(Elem, [_|Tail]) :-
          memb_eq(Elem, Tail).

     % 1 terminating condition
     memb_eq_det(Elem, [Head|_]) :-
          Elem == Head.
     % recursive
     memb_eq_det(Elem, [Head|Tail]) :-
          Elem \== Head,
          memb_eq_det(Elem, Tail).

We can illustrate the behaviour of these two procedures as follows:

     | ?- Elem = a, memb_eq(Elem, [a,b,a,b]), Elem=Output.

     Elem = a 
     Output = a ? ;

     Elem = a 
     Output = a ? ;

     no
     | ?- Elem = a, memb_eq_det(Elem, [a,b,a,b]), Elem=Output.

     Elem = a 
     Output = a ? ;

     no

Take time to work through the Self-Test 10

More flexible procedures

It gets rather difficult to remember the names of the various procedures written to implement deterministic and non-deterministic membership with different kinds of matching. An alternative to having to remember the several names is to write a more versatile membership procedure that allows the matching to be specified in the arguments.

We want to be able to write goals that look like:

     | ?- memb_ext(a, [a,b,a,b], =).
     | ?- memb_ext(Var, [a,b,a,b], ==).
     | ?- memb_ext(3, [4,2,5,1,3], <).

and so on.

One way to program this would be to write clauses for every type of matching, eg:

     % 1 terminating - =/2 condition
     memb_ext(Elem, [Elem|_], =).
     % 2 terminating - ==/2 condition
     memb_ext(Elem, [Head|_], ==) :-
          Elem == Head.
     % 2 terminating - </2 condition
     memb_ext(Elem, [Head|_], <) :-
          Elem < Head.
etc.

This would be a time-consuming way of writing a program. A better way would be to, in some way, use the third argument in the running of the program. This is quite easy to do, providing we know a few more built-in predicates.

The first thing to do is to check that the third argument of memb_ext/3 is instantiated. In fact, we can go further than this by insisting that it is instantiated to an atom and, if so, calling memb_ext/3:

     % 1
     memb_ext(Elem, List, Relation) :-
          atom(Relation),
          memb_ext1(Elem, List, Relation).

memb_ext1/3 implements the membership relation. The simpler clause is the recursive one, which has the same pattern as the basic memb/3 procedure:

     % 2 recursive
     memb_ext1(Elem, [_|List], Relation) :-
          memb_ext1(Elem, List, Relation).

The terminating condition is lengthier. Here we use three built-ins: functor/3, arg/3 and call/1:

     % 1 terminating
     memb_ext1(Elem, [Head|_], Relation) :-
          functor(Relation1, Relation, 2),
          arg(1, Relation1, Elem),
          arg(2, Relation1, Head),
          call(Relation1).

The line functor(Relation1, Relation, 2) has the effect of forming whatever Relation is instantiated to into a structured object with two arguments. As an example, consider the following:

     | ?- functor(Object, fred, 2).

     Object = fred(_A,_B) ? ;

     no
     | ?- functor(Obj, ==, 2).

     Obj = _A==_B ? ;

     no

The line arg(1, Relation1, Elem) has the effect of instantiating the first argument of Relation1 to Elem. Hence the following:

     | ?- arg(1, _22768==_22769, a), write(_22768==_22769), nl.
     a==_104

     yes

The following line instantiates the second argument. The last line, call(Relation1) merely executes Relation1 as a Prolog goal.

To illustrate the working of these procedures, consider the following:

     | ?- Elem = a, memb_ext(a, [a,b,a,b], =), Elem = Output.

     Elem = a 
     Output = a ? ;

     Elem = a 
     Output = a ? ;

     no
     | ?- memb_ext(Var, [a,b,a,b], ==).

     no
     | ?- Elem = 3, memb_ext(3, [4,2,5,1,3], <), Elem = Output.

     Elem = 3 
     Output = 3 ? ;

     Elem = 3 
     Output = 3 ? ;

     no

Although the use of "templates" such as these is rather esoteric, the built-ins used in the terminating rule of memb_ext1/3 are extremely important in Prolog because they are widely used in building compilers for specialised languages in Prolog.

Take time to work through the Self-Test 11

Back | Top of this Module | Next