prologpredicateclause

How do [ H | _ ] and [ _ | T ] in predicates work?


I am still learning Prolog and I came across this little snippet of code that I don't quite know if I have understood correctly.

Code:

% Takes the spiders friends and returns a list with persons who don't know each other.
getConspirators( [], Res, Res).

getConspirators( [H|T], CConspirators, Res):-
  append( [H|T], CConspirators, PK),
  knowsAtleastOne( PK),
  % Gets all the friends of the possible conspirator H.
  allFriends( H, PFriends),
  subtract( T, PFriends, Pprim),
  getConspirators( Pprim, [H|CConspirators], Res).

getConspirators( [_|T], CConspirators, Res) :-
  getConspirators( T, CConspirators, Res).

% Checks if any person Y or Y's friends know anybody in PK.
knowsAtleastOne( PK):-
    forall( person(Y), (memberchk(Y,PK) ; friendCons(Y,PK)) ).

% Checks if a person X's friends know any of the conspirators.
friendCons( X, Conspirators):-
    friend( X, Y),
    memberchk( Y, Conspirators),
    !.

(this is NOT the whole program, just a small snippet of it)

I am not sure if I have understood the getConspirators( [H|T], CConspirators, Res) :- and the getConspirators( [_|T], CConspirators, Res) :- parts of the getConspirators predicate. They look almost the same! Now, I do know that the "_" symbol means "literally any value" (AKA Prolog doesn't care about what value it is). But how does Prolog know which case to pick when running through the code? My theory is that Prolog runs the getConspirators( [_|T], CConspirators, Res) :- case if and only if the getConspirators( [H|T], CConspirators, Res) :- case fails (returns false) somewhere along the way. Have I understood this correctly?


Solution

  • There are three elements in play here: backtracking, unification and the list notation. I'll explain the three with a simpler example:

    moon(europa).
    moon(ganymede).
    
    planet(jupiter).
    planet(saturn).
    

    We know that Europa and Ganymede are two moons (of Jupiter) and that Jupiter and Saturn are planets. When we query what planets are known, we write:

    ?- planet(X).
    X = jupiter ;  % type ; for the next answer
    X = saturn.    % there's no more answer, hence .
    

    Unification happens when prolog looks for a rule head which fits to the query where the variables are substituted accordingly. For instance, there is no substitution that makes moon(X) = planet(Y) equal, but there is one for planet(jupiter) = planet(X), namely X=jupiter. That's how you obtain the first solution. For the second solution, Prolog needs to unifywith the second rule head, namely planet(saturn) = planet(X). Because this is done after the first option is completely enumerated, we call this backtracking.

    Now we can focus on (linked) lists. A list is either empty ([]) or it has a first element X prepended to a tail list Xs ([X|Xs]). Prolog has also a nicer notation for the list [X | [Y | [] ]], namely [X,Y]. Internally they are the same. When we now want to collect a list of astral objects, we can formulate the following three rules:

    astral_objects([]).        % The empty list is a list of astral objects.
    
    astral_objects([X|Xs]) :-  % The list [X | Xs] is a list of astral objects if...
        moon(X),               % ... its first element X is a moon
        astral_objects(Xs).    % ... and the remaining list Xs is a list of astral objects
    
    astral_object([X|Xs]) :-   % Likewise for planets
        planet(X),
        astral_objects(Xs).
    

    When we formulate query for a two-element list, we get all combinations of objects:

    ?- astral_object([A,B]).
    A = B, B = europa ;
    A = europa,
    B = ganymede ;
    A = europa,
    B = jupiter ;
    A = europa,
    B = saturn ;
    A = ganymede,
    B = europa ;
    A = B, B = ganymede ;
    A = ganymede,
    B = jupiter
    %...
    

    By unification, only rules 2 and 3 apply. In both cases we have astral_objects([X|Xs]) = astral_objects([A,B]). Remember that [A,B] is shorthand for [A|[B]] and there for X=A and Xs=[B]. The first rule of the body will unify X with the corresponding moon/planet and the recursion step describes the tail. Again, we unify astral_objects([X|Xs]) = astral_objects([B]), leading to X=B and Xs = []. Now the recursion step will only match the terminal case of the empty list and we have fully explored this path.

    Now what happens if we look for an arbitrary list of astral objects?

    ?- astral_object(Xs).
    Xs = [] ;
    Xs = [europa] ;
    Xs = [europa, europa] ;
    Xs = [europa, europa, europa] ;
    Xs = [europa, europa, europa, europa] ;
    Xs = [europa, europa, europa, europa, europa] 
    %... does not terminate
    

    The head astral_objects(Xs) matches all three bodies. After returning the substitution for the terminal case, it descends into the first rule over and over again. Since the length of the list is unrestricted, there are an infinite number of solutions to find before the third rule is ever tried. To avoid this, you can fairly enumerate the lists before you try to make them satisfy the predicate:

    ?- length(Xs,_), astral_object(Xs).
    Xs = [] ;
    Xs = [europa] ;
    Xs = [ganymede] ;
    Xs = [jupiter] ;
    Xs = [saturn] ;
    Xs = [europa, europa] ;
    Xs = [europa, ganymede] ;
    Xs = [europa, jupiter] ;
    Xs = [europa, saturn] ;
    Xs = [ganymede, europa]
    %...
    

    It still does not terminate, but you see the lists in ascending length and therefore the variety.