CODEWITHSUNDEEP
listprologconcatenationtrace
Pavindu
Pavindu

Reputation: 3112

How prolog derivation works in this query?

I tried to write a simple Prolog program with the following ruleset.

conc([],L,L).
conc([X|L1],L2,[X|L3]):- conc(L1,L2,L3).

Then I loaded this in the SWI-Prolog shell and executed the following query in the trace mode.

 ?-conc([2,3],[p,q],[2,3,p,q]).

The output was as follows.

[trace]  ?- conc([2,3],[p,q],[2,3,p,q]).
   Call: (8) conc([2, 3], [p, q], [2, 3, p, q]) ? creep
   Call: (9) conc([3], [p, q], [3, p, q]) ? creep
   Call: (10) conc([], [p, q], [p, q]) ? creep
   Exit: (10) conc([], [p, q], [p, q]) ? creep
   Exit: (9) conc([3], [p, q], [3, p, q]) ? creep
   Exit: (8) conc([2, 3], [p, q], [2, 3, p, q]) ? creep
true.

Now the problem is to draw the derivation tree of this goal, but I can't exactly understand how prolog does this, even by looking at the trace output above.

Can someone explain the derivation tree of the above query with regard to the mentioned ruleset? Helpful answers are highly appreciated.

Upvotes: 1

Views: 279

Answers (3)

David Tonhofer
David Tonhofer

Reputation: 15316

I feel that using the tracer is generally unhelpful unless you already know what you are doing and know that there is a problem at a precise location and even then it's a hard-to-disentangle mess.

It's much better to look closely at the program, and read it as the definition of a recursive call (or alternatively, as an inductive definition):

  1. The concatenation of an empty list [] and some other list L is that same list L:
    conc( [], L, L ).
  1. The concatenation of a nonempty list whose first element is X and some other list L2 is a list which is starting with that same X and continuing with a list L3 such that:
    • L3 is the concatenation of lists L1 and L2:
    conc( [X | L1], L2, [X | L3] ) :- 
        conc(  L1,  L2,      L3 ).

This is a pretty good actionable definition of concatenation:

  • Whenever a conc(A1,A2,R) succeeds, then we certainly have that all the element of A1 followed by all the elements of A2 form R (and so the definition makes sense as "concatenation").
  • Whenever conc "refers to itself" (recursively) the first list argument is smaller by one, so we have a "variant" that is monotonically decreasing and are getting somewhere (we will also automatically stop because a list length is always >= 0).
  • There is a non-recursive definition for a "base case" to be applied when the first list argument is of length 0, so when we stop, we can do so successfully (if the first clause conc([],L,L). was missing we would stop but fail due to lack of a matching clause for an empty list).

The "derivation tree" is rather linear (and not different from a derivation that you would find in a functional language), i.e. apply the second clause recurisvely until it no longer applies, then apply he first clause.

And thus we see:

Call: (8) conc([2, 3], [p, q], [2, 3, p, q])
   Call: (9) conc([3], [p, q], [3, p, q])
      Call: (10) conc([], [p, q], [p, q])
      Exit: (10) conc([], [p, q], [p, q])
   Exit: (9) conc([3], [p, q], [3, p, q])
Exit: (8) conc([2, 3], [p, q], [2, 3, p, q])

Note the traditional name of the "Exit port". The correct name is and should have always been "Success", even back in the 1980s. It never got changed.

Upvotes: 1

slago
slago

Reputation: 5509

The derivation tree is the following (considering clauses with renamed variables):

enter image description here

Upvotes: 2

tiffi
tiffi

Reputation: 683

?- conc([2,3],[p,q],[2,3,p,q]).

Call: (8) conc([2, 3], [p, q], [2, 3, p, q]) ? creep

The current goal is the question.

Since [2,3] does not match [], rule 1 is no option, thus rule 2 is tried. To match the head of rule 2, these substitutions are made: X/2, L1/[3], L2/[p,q], L3/[3,p,q].

Our new goal is now the body of rule 2, conc(L1,L2,L3), after the substitutions above, that is conc([3],[p,q],[3,p,q]).

Call: (9) conc([3], [p, q], [3, p, q]) ? creep

Since [3] does not match [], rule 1 is no option, thus rule 2 is tried. Substitutions: X/3, L1/[], L2/[p,q], L3/[p,q] Our new goal is now conc(L1,L2,L3) after the appropriate solutions, which amounts to conc([],[p,q],[p,q]).

Call: (10) conc([], [p, q], [p, q]) ? creep

Matches rule 1 => proof suceeded

Thus, the to-do-list for goal 10 is proven, thus goal 10 is proven:

Exit: (10) conc([], [p, q], [p, q]) ? creep

Thus, the to-do-list for goal 9 is proven, thus goal 9 is proven:

Exit: (9) conc([3], [p, q], [3, p, q]) ? creep

Thus, the to-do-list for goal 8 is proven, thus goal 8 is proven:

Exit: (8) conc([2, 3], [p, q], [2, 3, p, q]) ? creep

Since goal8 was the question, we're done, the proof is complete:

true.

Upvotes: 1

Related Questions