Here's the issue boiled down to a simpler test case :-) First, swi-prolog: # cat t.pl
a(3). foo(N) :- N. bar(a(X)) :- a(X). # swipl -f t.pl % /root/prolog/t.pl compiled 0.00 sec, 2,800 bytes ... ?- trace. true. [trace] ?- bar(a(Z)). Call: (6) bar(a(_G386)) ? creep Call: (7) a(_G386) ? creep Exit: (7) a(3) ? creep Exit: (6) bar(a(3)) ? creep Z = 3. [trace] ?- foo(a(Z)). Call: (6) foo(a(_G386)) ? creep Call: (7) a(_G386) ? creep Exit: (7) a(3) ? creep Exit: (6) foo(a(3)) ? creep Z = 3. In both cases, Z is correctly bound to 3. (The foo rule is the one we are interested in.) $ cat t.l (be a (3)) (be foo (@C) (@C -> @C)) (be bar ((a @N)) (a @N)) ~/lisp/miniPicoLisp $ ./pil t.l : (? a bar (bar (a @X))) 1 (bar (a @N)) 1 (a 3) @X=3 -> NIL That is correct: @X=3 ... however : : (? a foo (foo (a @X))) 1 (foo (a @X)) @X=NIL -> NIL : But they should be the same, as @X = 3 is a (is the) solution. Moreover, in foo (a @X) is never even tried to be proven. So I think this test case demonstrates the issue. > I still don't understand why this test of @A and/or @F for > being non-NIL is necessary at all. This looks unusual to me. holds(A,S) :- restoreSitArg(A,S,F), F ; \+ restoreSitArg(A,S,F), isAtom(A), A. Me too. At first, I also thought they simply were testing for non-NIL there. But the intent of the 'naked' F and A clauses there seems to be this: If the data bound to F (or A) is itself a clause, then that clause gets proved and variables in it get unified/bound. So after the first restoreSitArg(A,S,F), F starts out as partially bound to a clause like on(N,s0) - which itself has an unbound variable, N. After F is proven, N is bound to 3 (because on(3,s0) is asserted elsewhere, and so N = 3 is a solution). A bit tricky, with variables bound to clauses which, in turn, have in them other unbound variables that may get bound. Using call/1 there (not sure if this is the way I should use it) gives similar results, where (a @X) is not attempted to be proven. $ cat t.l (be a (3)) (be foo (@C) # (@C -> @C)) (call @C)) ~/lisp/miniPicoLisp $ ./pil t.l : (? a foo call (foo (a @X))) 1 (foo (a @X)) 1 (call (a @X)) -> NIL : Cheers, Doug -- UNSUBSCRIBE: mailto:picolisp@software-lab.de?subject=Unsubscribe