如何将函数式中的函数翻译成逻辑式中的关系

先看看例子：

在函数式编程中，我们可以用如下的方式定义「自然数」、「自然数加法」、「自然数乘法」：

(define (build-nat n)
  (cond
    ((= n 0) 'O)
    (else (cons 'S (build-nat (- n 1))))))

(define (succ-nat a)
  (cons 'S a))

(define (+-nat a b)
  (cond
    ((= a 0) b)
    (else (succ-nat (+-nat (- a 1) b)))))

(define (*-nat a b)
  (cond 
    ((= a 0) 0)
    (else
     (+-nat b (*-nat (- a 1) b)))))

模仿函数式编程编程的写法，我们可以在逻辑式编程中定义如下的关系：

;; using miniKanren

(defrel (succo a-1 a)
  (conso 'S a-1 a))

(defrel (zero?o n)
  (== n 'O))

(defrel (pos?o n)
  (fresh (n-1)
    (succo n-1 n)))

(defrel (+o a b c)
  (conde
   ((zero?o a) (== b c))
   ((pos?o a)
    (fresh (a-1 prev)
      (succo a-1 a)
      (succo prev c)
      (+o a-1 b prev)))))

(defrel (*o a b c)
  (conde
   ((zero?o a) (zero?o c))
   ((pos?o a)
    (fresh (a-1 prev)
      (succo a-1 a)
      (+o b prev c)
      (*o a-1 b prev)))))

得益于逻辑式编程的多方向性，我们不仅能用 +o *o 计算两数之和、两数之积，还能用它们来分解两数之和、两数之积。

但当我们使用上面定义的 *o 来分解两数之积时，程序会被卡住，这里以 (run * (x y) (*o x y 1)) 为例：

(*o x y 1) 

;; 因为 c != 0，进入 conde 的第二个分支
(pos?o x)
(succo a-1 x)
(+o b prev 1)
(*o a-1 b prev)

;; (+o b prev 1) 的一组合法分解为 (b = 0, prev = 1)
;; 于是我们转而查询
(*o a-1 0 1)

;; 又因为 c != 0，进入 conde 的第二个分支
(pos?o a-1)
(succo a-1-1 a-1)
(+o b prev 1)
(*o a-1-1 b prev)

;; 同样将 1 分解为 (b = 0, prev = 1)，我们又得到了
(*o a-1-1 0 1)  ;; 重复，导致程序卡死

会出现这样的原因是，我们在函数式编程中定义的递归边界只适用于单向的计算，而在逻辑式编程中，我们可以沿着任意方向计算，因此我们需要在逻辑式编程中定义更多递归边界。

(defrel (*o a b c)
  (conde
   ((zero?o a) (zero?o c))
   ((pos?o a) (zero?o b) (zero?o c)) ;; 增加的递归边界
   ((pos?o a) (pos?o b)
    (fresh (a-1 prev)
      (succo a-1 a)
      (+o b prev c)
      (*o a-1 b prev)))))

完整的代码见这里。