Frame 1:26 - What does q unify with?

Question

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 ()?

Answer 1

Does q unify 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) 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 ()?

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.