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

20,045

Solution 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.

Solution 2

The general solution for such problems are constraints.

Use 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.

Solution 3

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 3rd 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.

Solution 4

(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
Share:
20,045
user1279812
Author by

user1279812

Updated on July 09, 2022

Comments

  • user1279812
    user1279812 almost 2 years

    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?

  • Admin
    Admin about 12 years
    +1: Thanks for picking up my error! I like the technique using nth1/3 too, nice one.
  • CAFEBABE
    CAFEBABE over 8 years
    Interesting analysis. As said my primary goal was to provide a solution which is close to the posters question. I was wondering a long time why my code falls short on the first query. It should be still linear in the input. It can be slow as it is not tail recursive but is this really the explanation?. So I'm now wondering what is going on.
  • repeat
    repeat over 8 years
    @CAFEBABE. Source of the problem? The solution you proposed: "However, this can easily be fixed by reordering the goals." In effect, you solved one problem and introduced another one...
  • CAFEBABE
    CAFEBABE over 8 years
    The point is a different one. My Statement was that the predicate is in O(N). You claimed that it is not, by doing a test using timing. My statement is a purely theoretical argument which can mathematically proven. Yours is a purely empirical argument. Two question arise (a) is my code in O(N) if not why (b) is it really tail recursion which cause the problem.
  • CAFEBABE
    CAFEBABE over 8 years
    Thanks, for challenging me. I updated my answer accordingly. The solution is actually quite simple and it is purely logic programming.
  • repeat
    repeat over 8 years
    @CAFEBABE. I was not referring to empirical time measurement data, but to the actual number of inference steps. cf statistics/2 info in the SWI manual.
  • repeat
    repeat over 8 years
    @CAFEBABE. This is not about tail-recursion, not at all! If we define posAt/3 like posAt([X|_], 1, [X|_]). posAt([_|X], K, [_|Y]) :- K > 1, Kr is K-1, posAt(X, Kr, Y), K is Kr+1, K > 1. and run ?- numlist(1,1000,Zs), time((posAt(Zs,1000,Zs),false)). we get % 4,000 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 3179006 Lips). Above definition is definitely not tail-recursive, yet it runs in O(N) inferences.
  • repeat
    repeat over 8 years
    s(X) for using lists for arithmetic purposes.
  • CAFEBABE
    CAFEBABE over 8 years
    Found what I was not seeing
  • CAFEBABE
    CAFEBABE over 8 years
    Nice on ;). That was striking me from the beginning with Prolog lists. They are basically an implementation of the Peano axioms with some additional payload: the list content.