SWI-Prolog predicates

Question

I am very new to prolog and my prof seems to have forgotten to teach the class its basic use. He gave us the task of writing predicates stmt and stmts, with the first predicate looking like:

stmt([pass|X], X).
stmt([declare,N|X], X) :- atom(N).
stmt([use,N|X], X) :- atom(N).

which then passes the test code stmt([use,x,something,else],[something,else]).

The second part looks like the following:

define a stmts predicate such that {stmts(List1, List2)} is provable if (List1) starts with atoms that match the (stmts) nonterminal and then continues with the atoms in List2. For example, the following query should produce true: stmts([pass,use,x,more,stuff],[more,stuff]).

I don't understand how exactly to get this to work. Any help would be appreciated.

Willem Van Onsem Willem Van Onsem · Accepted Answer · 2017-05-09T16:06:50

It works because of the unification process in Prolog and the fact that a list in Prolog is a linked list.

First of all it might be useful to understand that a list is implement in a CONS-way (the term originates from Lisp if I recall correctly). That means that there is a functor (let's here use cons/2 for simplicity), such that a list, [use,x,something,else] is structured like cons(use,cons(x,cons(something,cons(else,nil)))) (nil being the end of the list). So in a linked-list fashion.

Next if you "call a predicate in Prolog" unification happens. It aims to unify the arguments in the call with the arguments in the head of the clause. For instance if the head of the claus is foo(bar(X,qux(Y))) and you call it with foo(bar(3,Z)), then as a result X = 3 and Z = qux(Y) with X and Y being "uninstantiated variables".

If we combine these two we see that a desugared variant of your code would be:

stmt(cons(pass,X), X).
stmt(cons(declare,cons(N,X)), X) :- atom(N).
stmt(cons(use,cons(N,X)), X) :- atom(N).

So now if we call stmt(cons(use,cons(x,cons(something,cons(else,nil)))),cons(something,cons(else,nil))). A unification will happen. First Prolog aim to unify with the first clause:

stmt(cons(pass,X),         X)
stmt(cons(use, cons(x,...),cons(something,cons(else,nil)))

(I used an ellipse to keep it simple).

The unification will aim to unify the first arguments, like:

cons(pass,X) ~ cons(use,cons(else,...))
X ~ cons(something,cons(else,nil))

Now the unification will peel: remove the first unification, and inject unification of the arguments, so:

pass ~ use
X ~ cons(else,...)
X ~ cons(something,cons(else,nil))

Now in Prolog pass and use are constants (since these start with a lowercase). Furthermore all constants in Prolog are different (except if the have the same "name" so to speak). So since pass ~ use cannot unify. The first clause "fails".

In Prolog a backtracking mechanism is in place: after the first clause is been called - regardless whether that was a success or a failure - Prolog will retry the call with the second clause, third clause and so on.

So now we aim to unify the call. So now we perform unification like:

stmt(cons(declare,cons(N,X  )),X)
stmt(cons(use,    cons(x,...)),cons(something,cons(else,nil)))

Which result in unification like:

cons(declare,cons(N,X)) ~ cons(use,cons(x,...))
X ~ cons(something,cons(else,nil))

again we peel:

declare ~ use
cons(N,X) ~ cons(x,...)
X ~ cons(something,cons(else,nil))

and again that's a fail.

Our final attempt is:

stmt(cons(use,cons(N,X)) ,X).
stmt(cons(use,cons(x,...),cons(something,cons(else,nil)))

which yields:

cons(use,cons(N,X)) ~ cons(use,cons(x,...))
X ~ cons(something,cons(else,nil))

and then yields:

use ~ use
cons(N,X) ~ cons(x,...)
X ~ cons(something,cons(else,nil))

which results into:

use ~ use
N ~ x
X ~ ...
X ~ cons(something,cons(else,nil))

(the ... is cons(something,cons(else,nil))). So now unification has succeeded, hurray. But we are not there yet. Now the head of the third clause has succeed, which means we now have to perform calls on the body of that clause. So we call:

atom(N).

and since N = x, it means we call x. Now atom(x) is a builtin, and succeeds (we are not going to do the unification process again here). So that means that the third clause succeeds.

SWI-Prolog predicates

1 Answers