Simple prolog program. Getting error: >/2: Arguments are not sufficiently instantiated

Question

I made a Prolog predicate posAt(List1,P,List2) that tests whether the element at position P of List1 and List2 are equal:

posAt([X|Z], 1, [Y|W]) :-
   X = Y.
posAt([Z|X], K, [W|Y]) :-
   K > 1,
   Kr is K - 1,
   posAt(X, Kr, Y).

When testing:

?- posAt([1,2,3], X, [a,2,b]).

I expected an output of X = 2 but instead I got the following error:

ERROR: >/2: Arguments are not sufficiently instantiated

Why am I getting this error?

Answer 1

A Prolog predicate is a relation between arguments, and your statement

the element at position P of List1 and List2 are equal

is clearly an example where multiple solutions are possible.

?- posAt([1,2,3],X,[1,5,3,7]).
X = 1.

So the answer from sharky, while clearly explains why the technical error arises, requires a small correction:

posAt([X0|_], Pos, Pos, [X1|_]) :-
    X0 == X1.

Now it works as expected.

?- posAt([1,2,3],X,[1,5,3,7]).
X = 1 ;
X = 3 ;
false.

Writing simple predicates for list processing it's a very valuable apprenticeship practice, and the main way to effectively learn the language. If you are incline also to study the available library predicates, here is a version using nth1/3 from library(lists)

posAt(L0, P, L1) :-
   nth1(P, L0, E),
   nth1(P, L1, E).

This outputs:

?- posAt([1,2,3],X,[1,5,3,7]).
X = 1 ;
X = 3.

Could be interesting to attempt understanding why in this case SWI-Prolog 'top level' interpreter is able to infer the determinacy of the solution.

Answer 2

This occurs because, when the subgoal K > 1 is evaluated by Prolog, K is still an unbound variable and not a number. Standard Prolog can't (won't) evaluate the true/false value of numerical range restrictions such as this when they aren't ground (as opposed to constraint solvers like CLP, which permit this but work differently).

Consider this solution:

posAt(L0, Pos, L1) :- 
    posAt(L0, 1, Pos, L1).

posAt([X0|_], Pos, Pos, [X1|_]) :-
    X0 == X1.    
posAt([_|X0s], CurrPos, Pos, [_|X1s]) :-
    NextPos is CurrPos + 1,
    posAt(X0s, NextPos, Pos, X1s).

The first predicate posAt/3 sets up the initial condition: lists as position 1, and calls posAt/4 to iterate though the list.

The first clause of posAt/4 is a match condition: the elements in both lists at the same position are equal. In this case, the current position variable is unified with Pos, the result.

If the above clause failed because the list elements X0 and X1 were unequal, the list position CurrPos is incremented by one, and a recursive call to posAt/4 starts processing again at the next pair of items.

EDIT: Removed incorrect cut in first clause of posAt/4 (thanks to @chac for the pickup)

Answer 3

The general solution for such problems are constraints.

Use clpfd for integer arithmetic that works in all directions:

:- use_module(library(clpfd)).

posAt([X|_], 1, [X|_]).
posAt([_|X], K, [_|Y]) :-
   K #> 1, 
   Kr #= K - 1,
   posAt(X,Kr,Y).

With these simple changes, your example works exactly as expected:

?- posAt([1,2,3], X, [a,2,b]).
X = 2 ;
false.

Answer 4

TL;DR: The answers by @CAFEBABE, @CapelliC, @mat, and @sharky all fall short!

So... what exactly are the shortcomings of the answers proposed earlier?

• @CAFEBABE's stated:

  Nice about this solution is that the runtime is linear in the length of both lists.

  Let's put that statement to the test!

  ?- numlist(1,1000,Zs), time(posAt__CAFEBABE1(Zs,1000,Zs)).
  % 999,001 inferences, 0.090 CPU in 0.091 seconds (100% CPU, 11066910 Lips)
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
  % 4 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 66738 Lips)
  false.
  

  Bummer! The others do just fine:

  ?- numlist(1,1000,Zs), time(posAt__CapelliC1(Zs,1000,Zs)).
  % 671 inferences, 0.000 CPU in 0.000 seconds (98% CPU, 3492100 Lips)
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...].
  
  ?- numlist(1,1000,Zs), time(posAt__mat1(Zs,1000,Zs)).
  % 3,996 inferences, 0.001 CPU in 0.001 seconds (99% CPU, 3619841 Lips)
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
  % 5 inferences, 0.000 CPU in 0.000 seconds (89% CPU, 154703 Lips)
  false.
  
  ?- numlist(1,1000,Zs), time(posAt__sharky1(Zs,1000,Zs)).
  % 1,000 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 2627562 Lips)
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
  % 4 inferences, 0.000 CPU in 0.000 seconds (82% CPU, 97109 Lips)
  false.
  

• @CapelliC used nth1/3, which can (and does) cause problems with universal termination:

  ?- time((posAt__CapelliC1(_,N,[a,b,c]), false)).
  **LOOPS**
  

  D'oh! The others all do just fine:

  ?- time((posAt__CAFEBABE1(_,_,[a,b,c]), false)).
  % 14 inferences, 0.000 CPU in 0.000 seconds (88% CPU, 1098470 Lips)
  false.
  
  ?- time((posAt__mat1(_,_,[a,b,c]), false)).
  % 2,364 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 2764075 Lips)
  false.
  
  ?- time((posAt__sharky1(_,_,[a,b,c]), false)).
  % 6 inferences, 0.000 CPU in 0.000 seconds (89% CPU, 207247 Lips)
  false.
  

• @mat's code has complexity issues. @CAFEBABE and @CapelliC do "a little better"—their codes are faster because they use rely on lower-level primitives (is)/2 and nth1/3.

  ?- numlist(1,1000,Zs), time((posAt__mat1(Zs,_,_), false)).
  % 33,365,972 inferences, 1.643 CPU in 1.643 seconds (100% CPU, 20304661 Lips)
  false.
  
  ?- numlist(1,1000,Zs), time((posAt__CAFEBABE1(Zs,_,_), false)).
  % 1,001,002 inferences, 0.083 CPU in 0.083 seconds (100% CPU, 12006557 Lips)
  false.
  
  ?- numlist(1,1000,Zs), time((posAt__CapelliC1(Zs,_,_), false)).
  % 171,673 inferences, 0.030 CPU in 0.030 seconds (100% CPU, 5810159 Lips)
  false.
  

  The code by @sharky is clearly best in this respect:

  ?- numlist(1,1000,Zs), time((posAt__sharky1(Zs,_,_), false)).
  % 1,003 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 1605658 Lips)
  false.
  

• @sharky's code uses the meta-logical built-in predicate (==)/2 which makes it lose logical soundness when used with insufficiently instantiated terms. This query should succeed:

  ?- posAt__sharky1([a], 1, Xs).
  false.
  

  The other codes all give a logically sound answer:

  ?- posAt__CAFEBABE1([a], 1, Xs).
  Xs = [a|_G235] ;
  false.
  
  ?- posAt__CapelliC1([a], 1, Xs).
  Xs = [a|_G235].
  
  ?- posAt__mat1([a], 1, Xs).
  Xs = [a|_G235] ;
  false.
  

• Going past the first answer, @CAFEBABE's code gets more than a little inefficient:

  ?- numlist(1,1000,Zs), time(posAt__CAFEBABE1(Zs,1,Zs)).
  % 0 inferences, 0.000 CPU in 0.000 seconds (93% CPU, 0 Lips) 
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
  % 999,004 inferences, 0.076 CPU in 0.076 seconds (100% CPU, 13121058 Lips)
  false.
  

  Similar—but an order of magnitude smaller— issues show with @sharky's code:

  ?- numlist(1,1000,Zs), time(posAt__sharky1(Zs,1,Zs)).
  % 1 inferences, 0.000 CPU in 0.000 seconds (75% CPU, 31492 Lips)
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
  % 1,003 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 1078556 Lips)
  false.
  

  The codes by @CapelliC and @mat are both doing alright:

  ?- numlist(1,1000,Zs), time(posAt__CapelliC1(Zs,1,Zs)).
  % 7 inferences, 0.000 CPU in 0.000 seconds (85% CPU, 306802 Lips)
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...].
  
  ?- numlist(1,1000,Zs), time(posAt__mat1(Zs,1,Zs)).
  % 0 inferences, 0.000 CPU in 0.000 seconds (80% CPU, 0 Lips)
  Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
  % 5 inferences, 0.000 CPU in 0.000 seconds (84% CPU, 345662 Lips)
  false.
  

---

So... what do we do? Why not follow this approach and combine @mat's and @sharky's code?

:- use_module(library(clpfd)).

posAt__NEW(L0, Pos, L1) :- 
    posAt__NEW_(L0, 1, Pos, L1).

posAt__NEW_([X|_], Pos, Pos, [X|_]).
posAt__NEW_([_|X0s], CurrPos, Pos, [_|X1s]) :-
    CurrPos #< Pos,
    NextPos #= CurrPos + 1,
    posAt__NEW_(X0s, NextPos, Pos, X1s).

Let's re-run above sample queries with posAt__NEW/3:

?- numlist(1,1000,Zs), time(posAt__NEW(Zs,1000,Zs)).
% 4,997 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 18141619 Lips)
Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
% 9 inferences, 0.000 CPU in 0.000 seconds (71% CPU, 122877 Lips)
false.

?- time((posAt__NEW(_,_,[a,b,c]), false)).
% 440 inferences, 0.001 CPU in 0.001 seconds (98% CPU, 803836 Lips)
false.

?- numlist(1,1000,Zs), time((posAt__NEW(Zs,_,_), false)).
% 154,955 inferences, 0.014 CPU in 0.014 seconds (100% CPU, 11067900 Lips)
false.

?- posAt__NEW([a], 1, Xs).
Xs = [a|_G229] ;
false.

?- numlist(1,1000,Zs), time(posAt__NEW(Zs,1,Zs)).
% 1 inferences, 0.000 CPU in 0.000 seconds (93% CPU, 121818 Lips)
Zs = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;
% 7 inferences, 0.000 CPU in 0.000 seconds (86% CPU, 266748 Lips)
false.

Alright! At last, we make sure that the goal used in the 3^rd query above has linear complexity:

?- numlist(1,100,Zs), time((posAt__NEW(Zs,_,_), false)).
% 15,455 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 3545396 Lips)
false.

?- numlist(1,1000,Zs), time((posAt__NEW(Zs,_,_), false)).
% 154,955 inferences, 0.016 CPU in 0.017 seconds (98% CPU, 9456629 Lips)
false.

?- numlist(1,10000,Zs), time((posAt__NEW(Zs,_,_), false)).
% 1,549,955 inferences, 0.098 CPU in 0.099 seconds (99% CPU, 15790369 Lips)
false.

?- numlist(1,100000,Zs), time((posAt__NEW(Zs,_,_), false)).
% 15,499,955 inferences, 1.003 CPU in 1.007 seconds (100% CPU, 15446075 Lips)
false.

Answer 5

(This just popped up on my dashboard hence the late answer...)

I looked at the question and was thinking whether it is possible to provide a solution close to the original question. The problem, as already explained, is that the relation > needs its arguments instantiated. Actually similar for is. However, this can easily be fixed by reordering the goals:

posAt([X|_], 1, [X|_]).
posAt([_|X], K, [_|Y]) :-
   posAt(X, Kr, Y),
   K is Kr+1,
   K > 1.

This solution is that the runtime is linear in the length of both lists, as long as K is ground. However, there is a problem, if the first elements do match in the list as nicely illustrated in the answer by repeat.

In fact the last element is superfluous, hence, equivalent.

posAt([X|_], 1, [X|_]).
posAt([_|X], K, [_|Y]) :-
   posAt(X, Kr, Y),
   K is Kr+1.

However, as proven by @repeat this code is horribly slow. this is probably due to the fact that the code is breaking tail recursion.

A logical clean solution would solve this problem. Here we would represent the natural numbers using the Peano Axiomes (s/1 successor or relation) and the solution would become

posAt([X|_], zero, [X|_]).
posAt([_|X], s(K), [_|Y]) :-
   posAt(X, K, Y).

however, this is hard to time, hence, a hackish solution roughly equivalent

  posAt([X|_], [a], [X|_]).
  posAt([_|X], [a|L], [_|Y]) :-
      posAt(X, L, Y).

Timing this solution gives

N=8000,numlist(1,N,_Zs), length(_LN,N),time(posAt(_Zs,_LN,_Zs)).
 7,999 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 7342035 Lips)
N = 8000