Fork me on GitHub
Slack Archive

This page is not created by, affiliated with, or supported by Slack Technologies, Inc.

2023-11-11

Channels

#core-logic
<
2023-11-11
>
moe14:11:04

I'm new to core.logic, and I'm working through the http://webyrd.net/alphamk/alphamk.pdf with core.logic.nominal. On page 4, when getting into details about var swapping, an example equivalent to this is given: 

(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))))
With the comment that "the unifier cannot apply the swap (a b) to either x or y, since they are both unbound...nominal unification solves this problem by introducing the notion of a suspension". In c.l.nominal, they var swap / unify the same as if the expressions were identical, neither variable being instantiated.

moe15:11:12

Example from the paper

moe16:11:50

are the suspensions just being applied?