MiniKanren Racket 一元数乘法

Question

我正在尝试在 MiniKanren 中实现一元数的乘法。所以我写了以下代码：

#lang iracket/lang

(require minikanren)
(require minikanren/matche)

(defrel (unaryo n) (conde
   [(== 'z n)]
   [(fresh (m)
(== `(s ,m) n) (unaryo m))]))

(defrel (addo a b c) 
 (conde
  [(== 'z a) (== b c)] 
  [(fresh (d e)
          (== `(s ,d) a)
          (== `(s ,e) c)
          (addo d b e))]))

(defrel (mulo x y z)
  (conde
    [(== x 'z) (== z 'z)]
    [(fresh (x1 z1)
      (== `(s ,x1) x)
      (addo y z1 z)
      (mulo x1 y z1))]))
(run 1 (x) (mulo '(s (s z)) '(s (s (s z))) x))

然后我尝试执行一些测试：

1. (run 1 (x) (mulo '(s (s z)) '(s (s (s z))) x))

   输出：'((s (s (s (s (s (s z)))))))，这是正确的

2. (run 1 (x) (mulo '(s (s (s z))) x '(s (s (s (s (s (s (z)))))))))

   ，但是这个测试产生'()，这是错误的，结果应该是'((s (s z)))

你能找到我错的地方吗？预先感谢！

尝试测试

addo

它产生了正确的结果

Answer 1

(run 1 (x) (mulo '(s (s (s z))) x '(s (s (s (s (s (s (z)))))))))，但此测试产生 ' ()，这是错误的，结果应该是 '((s (s z)))

提示：如果您对传递给

unaryo

的数字运行

mulo

会发生什么？