Suspended var swaps in core.logic.nominal

[Moe Aboulkheir]

Afternoon,

I'm new to core.logic, and was working through the αKanren paper with core.logic.nominal.  On page 4, there is an example which translates to:

(l/run* [q]
  (n/fresh [a b]
    (l/fresh [x y]
      (l/== (n/tie a (n/tie a x)) (n/tie a (n/tie b y)))
      (l/== `(~x ~y) q)))) 

=> ((_0 _1))

The example output in the paper is as follows, with the given explanation:

((((susp ((a0 a1)) _0) _0) : ((a0 . _0))))

The first call to ≡ applies the swap (a b) to the unbound variable y, and then associates the resulting suspension (susp ((a b)) y) with x . Of course, the unifier could have applied the swap to x instead of y, resulting in a symmetric answer. The freshness constraint states that the nom a can never occur free within y, as required by the definition of binder equivalence.

 Could somebody explain to me, as if I were a child, this discrepancy?  I looked at the source, and saw code that looked very much like suspensions being applied at creation time, rather than on var instantiation like the paper elsewhere indicates, but I'm out of my depth and not in a position to reason about strategy.

Best,

Moe

[Moe Aboulkheir]

According to the wiki:

In core.logic.nominal, we implement suspensions as constraints. During swapping of a and b, whenever we encounter a variable x, we replace it with a fresh variable x' and add the suspension constraint swap [a b] x' x. This swap constraint is executed under one of two conditions:

x and x' both become bound -- the swapping can resume
x and x' become equal -- we enforce a#x' and b#x' and drop the swap constraint

I do not see how either of these conditions obtains in the quoted example — x  and y are unbound.

Best,

Moe