为什么miniKanren中的"disj“在方案中起作用，但在球拍中不起作用？

Question

我使用minikanren库进行球拍，但我想使用"disj“和"conj”运算符。为了便于阅读，我希望能够更明确地声明我使用的是disj还是conj，而不是解析conde表达式，特别是在表达式变得更加复杂的情况下。我抄袭了“推理的阴谋者”中的源码：

(define (append∞ s∞ t∞)
  (cond
    ((null? s∞) t∞)
    ((pair? s∞)
     (cons (car s∞)
           (append∞ (cdr s∞) t∞)))
    (else (λ ()
            (append∞ t∞ (s∞))))))

(define (disj2 g1 g2)
  (λ (s)
    (append∞ (g1 s) (g2 s))))

(define-syntax disj
  (syntax-rules ()
    [(disj) '()]
    [(disj g) g]
    [(disj g0 g ...) (disj2 g0 (disj g ...))]))

这在前两种情况下可以正常工作。

> (run* (x) (disj (== 'foo x)))
'(foo)

但在使用多个目标时仅返回第一个结果：

> (run* (x) (disj (== 'foo x) (== 'bar x) (== 'foobar x)))
'(foo)

为什么会这样呢？

Answer 1

嗯。我似乎不能重现这种行为。

当我克隆TRS/2e repo时，同时添加两个

#lang racket
(provide (all-defined-out))

在trs2-impl.scm的顶部，运行该文件，然后尝试您的测试程序。我看到了预期的结果：

; 
; Welcome to Racket v7.9.0.3 [cs].
; 
trs2-impl.scm> (run* (x) (disj (== 'foo x) (== 'bar x) (== 'foobar x)))
'((foo) (bar) (foobar))

您是否看到了不同的行为？如果是这样，那么我们可以看得更深一些。你知道你使用的是哪个版本的球拍吗？我认为这无关紧要，但以防万一。