We have:
(run* q
(fresh (x)
(==
`(,x)
q)))
In this case `(,x) is a list where the refrence to the variable x isn't quoted.
Does q unifies with a single element list?
Is the result (_0) because q unifies with the fresh variable x (even if it's in a list) or because it doesn't unify with anything at all? Or would in that case the result have been ()?
Does
qunify with a single element list?
Yes. (== (list x) q) is the same as (== q (list x)). Both q and x are fresh before the execution of this unification goal (and q does not occur in (list x)). Afterwards, it is recorded in the substitution that the value of q is (list x). No value for x is recorded.
Is the result
(_0)becausequnifies with the fresh variablex(even if it's in a list) or because it doesn't unify with anything at all? Or would in that case the result have been()?
No, q does not unify with x, but rather with a list containing x.
When the final value of the whole run* expression is returned, the variables are "reified", replaced with their values. x has no value to be replaced with, so it is printed as _0, inside a list as it happens, which list is the value associated with q.
The value of (run* q ...) is a list of all valid assignments to q, as usual. There is only one such association, for the variable q and the value (list x).
So ( (_0) ) should be printed as the value of the (run* q ...) expression -- a list of one value for q, which is a list containing an uninstantiated x, represented as a value _0.
