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?

4

Thanks @anon19431257 . 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!