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
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)
becauseq
unifies 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
.