# Re: pilog: unification in variables that are clauses

```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
```