Determining successor in prolog using recursion

Question

I'm trying (failing) to understand an exercise where I'm given the following clauses;

pterm(null).
pterm(f0(X)) :- pterm(X).
pterm(f1(X)) :- pterm(X).

They represent a number in binary, eg. f0(null) is equivalent to 0, f1(null) is equivalent to 1, etc.

The objective is to define a predicate over pterm such that one is the successor of the other when true. It seems like a relatively simple exercise but I'm struggling to get my head around it.

Here is the code I've written so far;

incr(X,Y) :- pterm(f0(X)), pterm(f1(Y)).
incr(X,Y) :- pterm(f0(f1(X))), pterm(f1(f1(Y))).

Having tested this I know it's very much incorrect. How might I go about inspecting the top level arguments of each pterm?

I've made minimal progress in the last 4 hours so any hints/help would be appreciated.

Your program is equivalent (w.r.t. the set of solutions) to: incr(X, Y) :- pterm(X), pterm(Y). Clearly this program is much too general! — false

Tasos Papastylianou Tasos Papastylianou · Accepted Answer · 2016-10-28T10:05:53

1)
I'll start with the "how to inspect" question, as I think it will be the most useful. If you're using swi-prolog with xpce, run the guitracer:

?- consult('pterm').   % my input file
% pterm compiled 0.00 sec, 5 clauses
true.

?- guitracer.
% The graphical front-end will be used for subsequent tracing
true.

?- trace.   % debugs step by step
true.

[trace]  ?- pterm(f0(f1(null))).    % an example query to trace
true.

A graphical interface will come up. Press the down arrow to unify things step by step. What's going on should make sense fairly quickly.
(use notrace. and nodebug. appropriately to exit trace and debug modes afterwards).

truefalse

When your predicates are called using constants, checking its truth value is a matter of checking your facts database to see if that predicate with those constants can be satisfied. But when you call using variables, prolog goes through a wild goose chase, trying to unify that variable with all the allowable stuff it can link it to, to see if it can try to make that predicate true. If it can't, it gives up and says it's false.

A predicate like incr(X,Y) is still something that needs to return true or false, but, if by design, this only becomes true when Y is the incremented version of X, where X is expected to be given at query time as input, then we have tricked prolog into making a "function" that is given X as input, and "returns" Y as output, because prolog will try to find an appropriate Y that makes the predicate true.

Therefore, with your example, incr(X,Y) :- pterm(f0(X)), pterm(f1(Y)). makes no sense, because you're telling it that incr(X,Y) will return true for any X,Y, as long as prolog can use X to find in the fact database any pterm(f0(X)) that will lead to a known fact, and also use Y to find a pterm(f1(Y)) term. You haven't made Y dependent on X in any way. This query will succeed for X = null, and Y = null, for instance.

Your first clause should be something like this.

incr(X,Y) :- X = pterm(f0(Z)), Y = pterm(f1(Z)).

where = performs unification. I.e. "find a value for Z such that X is pterm(f0(Z)), and for the same value of Z it also applies that Y = pterm(f1(Z))."

In fact, this could be more concisely rewritten as a fact:

incr( pterm(f0(Z)), pterm(f1(Z)) ).

(since the actual logic is what your assignment is about, I won't offer a solution here. but hope this helps get you into grips with what's going on. feel free to have a go at the recursive version and ask another question based on that code!)

Determining successor in prolog using recursion

1 Answers