MiniKanren一元数乘法实现问题：反向查询无结果

你的问题核心是mulo关系的递归目标顺序错误，导致反向查询时无法利用已知的积约束来缩小搜索范围，最终返回空结果。以下是具体分析和修正方案：

常见错误写法（你的mulo大概率是这种） #

如果你的mulo递归分支中先调用了mulo再调用addo，就会出现正向查询正常、反向查询无结果的问题：

(define mulo
  (lambda (a b c)
    (conde
      [(== a 'z) (== c 'z)]
      [(fresh (a- c-)
         (== a `(s ,a-))
         (mulo a- b c-)  ; 错误：先递归mulo，c-无约束会无限生成
         (addo b c- c))])))

• 正向查询时（如2×3），a是具体值，递归过程中c-会被逐步约束，所以能得到正确结果。
• 反向查询时（如已知3和积6求另一个乘数），c是具体值但c-未约束，先调用mulo会让MiniKanren无限生成可能的c-，而addo的约束无法回溯匹配，最终返回空。

修正后的正确实现 #

调整递归分支中目标的顺序，先通过addo从已知的c和b约束出c-，再递归调用mulo：

; 一元数判断关系
(define unaryo
  (lambda (n)
    (conde
      [(== n 'z)]
      [(fresh (n-)
         (== n `(s ,n-))
         (unaryo n-))])))

; 一元数加法关系（已验证正常，无需修改）
(define addo
  (lambda (a b c)
    (conde
      [(== a 'z) (== b c)]
      [(fresh (a- c-)
         (== a `(s ,a-))
         (== c `(s ,c-))
         (addo a- b c-))])))

; 修正后的一元数乘法关系
(define mulo
  (lambda (a b c)
    (conde
      ; 0乘任何数结果为0
      [(== a 'z) (== c 'z)]
      ; (s a) × b = b + (a × b)，先约束c-再递归
      [(fresh (a- c-)
         (== a `(s ,a-))
         (addo b c- c)  ; 先通过addo从c和b算出c- = c - b
         (mulo a- b c-))])))

测试反向查询 #

执行你需要的反向查询：

(run* (x)
  (mulo x '(s (s (s z))) '(s (s (s (s (s (s z))))))))

会得到预期结果：'((s (s z)))

内容的提问来源于stack exchange，提问作者NAD