# pilog: unification in variables that are clauses

```--- On Wed, 6/29/11, Alexander Burger <a...@software-lab.de> wrote:

> So this should be written as
>
>(be holds (@A @S)
> (or
>  ((restoreSitArg @A @S @F) (@ solve (list (-> @F))))
>  ((not (restoreSitArg @A @S @F)) (isAtom @A) (@ solve (list (-> @A)))) ) )```
```
holds(A,S) :- restoreSitArg(A,S,F), F ;
\+ restoreSitArg(A,S,F), isAtom(A), A.

Now I think that the variables-as-clauses are getting me.  In this rule, F
might get bound to (unified with?) a clause with variables. For example, F
might be bound to something like on(N,s0)  When the F clause (now bound to
on(N,s0)) is then proved, the N variable in on(N,s0) gets bound to something
(3, for example).

[trace]  ?- holds(on(N), s0 ).
Call: (6) holds(on(_G386), s0) ? creep
Call: (7) restoreSitArg(on(_G386), s0, _G462) ? creep
Exit: (7) restoreSitArg(on(_G386), s0, on(_G386, s0)) ? creep
Call: (7) on(_G386, s0) ? creep
Exit: (7) on(3, s0) ? creep
Exit: (6) holds(on(3), s0) ? creep
N = 3 .

When I try to do this as (@ (solve (list (-> @F)))) in pilog, taking it through
lisp , it prevents the values of the unified vars in @F from being used in the
surrounding pilog rule.

? (? (holds (On @N) s0))
-> T
? (solve '((holds (On @N) s0)))
-> (T)

I wonder what I should do in this case, where a variable can be bound to a
clause like that and the variables in that clause need to be bound, too?

Cheers,

Doug

--
UNSUBSCRIBE: mailto:picolisp@software-lab.de?subject=Unsubscribe
```