How does this program work?

General
1

Hi, quick question

main(X) :-
  foo(a,X),
  foo(b,X).

foo(V,[V]).
foo(V,[V|_]).
foo(V,[_|Rest]) :- foo(V,Rest).

we get X = [a,b] but I’m a little confused how backtracking works in this case given my (mis)understanding of DFS.

Is this not how DFS backtracking should work in this case?

  1. X = [a].

  2. X = [a], X = [b]. % fail

  3. X = [a], X = [b|_]. % fail

  4. X = [a], X = [_|[b]]. % fail

  5. X = [a], X = [_|[b|_]]. % fail

  6. X = [a], X = [_|[_|[b]]]. % fail

  7. X = [a], X = [_|[_|[b|_]]]. % fail

  8. X = [a], X = [_|[_|[_|[b]]]]. % fail

and so on.

If we’re making a recursive call to foo, which itself has to exhaustively search each foo rule, which includes a recursive call to foo, which itself has to exhaustively search each foo rule …. then how do we ever backtrack to foo(a,X) unifying as X = [a|_]?

2

I mean I see how it happens to work

main(X) :-
  foo(a,X),writeln(X),
  foo(b,X),writeln(X).

foo(V,[V]) :- write(V),writeln(" using one").
foo(V,[V|_]) :- write(V),writeln(" using two").
foo(V,[_|Rest]) :- write(V),writeln(" using three"),foo(V,Rest).

?- main(X).
a using one
[a]
b using three
a using two
[a|_4518]
b using three
b using one
[a,b]
X = [a, b] .

It looks like we backtrack to foo(a,X) after foo(b,X) fails the first recursive call [1]? Why? Are predicates called from the body of a rule treated differently than predicates called from a “higher level”? In the rule foo(V,[_|Rest]) :- foo(V,Rest). why isn’t the call to foo(V,Rest). exhaustive?

[1] It’s also interesting in my output here we go from b using three to a using two without b using one first. How does that work? It’s almost like foo(V,Rest). wasn’t actually called? I feel like I’m fundamentally misunderstanding dfs backtracking then.

Likewise, after a unifies we go straight to b using three without one and two? Is it some optimization that the compiler knows they won’t work so they’re not tried?

I guess another way of asking this:

Is there an optimization at play here that detects an infinite loop of failure and backtracks based on that optimization? If so, how does that work?

3

Is this not how DFS backtracking should work in this case?

Prolog’s resolution strategy is called SLD resolution:
https://en.wikipedia.org/wiki/SLD_resolution

But in practice you need to understand the so called “Byrd Box Model”, which is what you get when you trace execution:

https://eu.swi-prolog.org/pldoc/man?section=debugoverview
https://github.com/dtonhofer/prolog_notes/tree/master/other_notes/about_byrd_box_model

That said, you can trace/0 your program, or here I am using the prolog_trace library (this is your original foo without the printing):

?- trace(foo, all).
%     foo/2: [all]
true.

?- main(X).
 T [13] Call: foo(a,_6556)
 T [13 +0.5ms] Exit: foo(a,[a])
 T [13] Call: foo(b,[a])
 T [20] Call: foo(b,[])
 T [20 +1.5ms] Fail: foo(b,[])
 T [13 +4.6ms] Fail: foo(b,[a])
 T [13 +8.6ms] Redo: foo(a,[a])
 T [13 +10.1ms] Exit: foo(a,[a|_12992])
 T [13] Call: foo(b,[a|_12992])
 T [20] Call: foo(b,_242)
 T [20 +1.6ms] Exit: foo(b,[b])
 T [13 +4.5ms] Exit: foo(b,[a,b])
X = [a,b] .

?- trace(foo, -all).
%     foo/2 Not tracing
true.

where the numbers in square brackets (13 and 20) indicate the call nesting level.

And now notice that, after “using three” you get “using two” not because the recursive call does not see “using one”, but rather because the recursive call altogether fails, and “using two” is the next case of the initial “using one”…

1 Like
4

Thanks @jp-diegidio . Let me chew on this and get back to you.

6

Damn it, caught my mistake. It’s because the recursive call foo(b,[]) = foo(V,[_|Rest]). fails.

Got it. Sorry, thanks!

7

This will succeed twice for:

?- foo(X, [X]).
true ;
true.

Could rewrite as:

foo(V, [V|T]) :-
    foo_v_tail(T).

foo_v_tail([]).
foo_v_tail([_|_]).
8

Sorry, can you clarify?

?- [user].
|: main(X) :-
|:   foo(a,X),
|:   foo(b,X).
|: 
|: foo(V, [V|T]) :-
|:     foo_v_tail(T).
|: foo_v_tail([]).
|: foo_v_tail([_|_]).
|: ^D% user://1 compiled 0.01 sec, 4 clauses
true.

?- main(X).
false.
9

I did not say to remove the foo(V,[_|Rest])predicate :wink:

10

ah gotcha thanks!