了解core.logic!=

Question

我希望下面的表达式返回一些结果,每个结果由两个cons单元组成,其中两个cons单元不相等.但是,它返回0结果.为什么我没有结果？

(run* [c1 c2] 
  (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2])
    (== ly [4 5])
    (membero x1 lx)
    (membero x2 lx) 
    (membero y1 ly)
    (membero y2 ly)
    (conso x1 y1 c1)
    (conso x2 y2 c2)
    (!= c1 c2)))

预期结果的例子:

• [(1 . 4) (2 . 5)]
• [(1 . 4) (1 . 5)]
• [(2 . 4) (2 . 5)]

我不希望它返回一个结果,比如[(1 . 4) (1 . 4)]每个缺点中的两个点都相等.

如果我删除该(!= c1 c2)部分,我会得到16个结果,包括两个缺点相同的结果.

如果我更换(!= c1 c2),我会得到我期望的结果:

(conde
  ((!= x1 x2))
  ((!= y1 y2)))

它应该做同样的事情,但明确检查两个单元格.

Answer 1

这不是一个有效的core.logic程序.你不能conso在尾巴不合适的地方使用.Scheme中的miniKanren将允许您执行此操作,但core.logic的行为未定义.我修改了文档字符串conso以反映这一点.一个工作计划:

(run* [c1 c2] 
  (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2])
    (== ly [4 5])
    (membero x1 lx)
    (membero x2 lx) 
    (membero y1 ly)
    (membero y2 ly)
    (== [x1 y1] c1)
    (== [x2 y2] c2)
    (!= c1 c2)))