如何在guile中实现tarai

Question

现在我想运行tarai，它的Prolog代码如下所示。一个测试用例是运行?- tarai(12,6,0,X)。这是一个相当困难的测试用例，例如GNU Prolog在此测试用例下崩溃。

tarai(X, Y, Z, R) :- 
    X > Y -> 
        X1 is max(0,X-1), tarai(X1, Y, Z, Rx),
        Y1 is max(0,Y-1), tarai(Y1, Z, X, Ry),
        Z1 is max(0,Z-1), tarai(Z1, X, Y, Rz),
        tarai(Rx, Ry, Rz, R); 
    R = Y.

我最感兴趣的是测试用例是否可以在tarai的一些miniKanren代码的完全声明版本上运行。可选地，我会对反向运行一些测试用例感兴趣。

我有点不知所措。我设法安装了guile，这是一个方案变体，并且可以成功地运行miniKanren测试用例。但是miniKanren没有整数，那么能做什么呢？

Answer 1

请注意，如果该算法存在并且是确定性的，则该算法只有一个解。您可以将方案变量作为x，y，z直接传递给kanren tarai函数，这些变量没有统一，因此可以在没有kanren变量的情况下实现X，Y，Z的逻辑。然而，R值需要是逻辑变量，并且您需要以tarai(Rx，Ry，Rz，R)形式获得有界值，例如，查找Rx，Ry，Rz的值并将这些值提供给tarai函数。此外，您还需要确保此表单是在前三个表单完成之后执行的(这很容易做到，因为没有纯粹的多项选择)，以便您知道Rx，Ry，Rz是有界的。还要注意，该算法可能依赖于执行顺序才能有效地执行，但同样，确定性意味着这一点是直接满足的。请注意，A -> B；C在这里仅翻译为方案(如果A、B、C)，因为A=X>Y是确定性的。因此，伪代码中的代码可能如下所示

(define (tarai x y z r)
  (lambda ()
    (fresh (rx ry rz)
       (if (> x y)
           (conda
             ( (conda ((tarai (- x 1) y z rx) 
                       (tarai (- y 1) z x ry)
                       (tarai (- z 1) x y rz)))
               (project (rx ry rz) (tarai rx ry rz r))))
           (== r y)))))

Answer 2

这个问题被问到如何在prolog规范中实现更通用版本的tarai函数，它允许x，y，z字段中的变量。这里的技术可以用prolog实现，例如，使用clpfd有限域求解器，而kanren需要一些类似的东西(参见上面的注释讨论，例如对numbers.scm的引用)。关键是核化->并对所有情况使用防护，我们将假设运算符>o =o <=o都是为变量定义的(例如，对于变量X，X>0会将X约束为值1,2,3，...)。我们还将假定'-o‘也是通过特殊的'iso’使用区间算术约束为这类变量定义的。使用这一点，我们可以将tarai定义为下面的代码(如果max和min也被定义为约束，这可以被简化，但在这里我们通过不等式和大量的情况来实现它们)。

(define (taray x y z w)
  (lambda ()         
    (conde ((<o x y) 
            (fresh (rx ry rz)
              (conde
               ((conde 
                  ((>o x 0) 
                   (fresh (xx) 
                     (conde
                       ((iso xx (-o x 1)) 
                        (tarai xx y z rx)))))
                  ((== x 0) (tarai 0 y z rx)))
                (conde 
                  ((>o y 0) 
                   (fresh (yy) 
                     (conde
                       ((iso yy (-o y 1)) 
                        (tarai yy z x ry)))))
                  ((== y 0) (tarai 0 z x ry)))
                (conde 
                  ((>o z 0) 
                   (fresh (zz) 
                     (conde
                       ((iso zz (-o z 1)) 
                        (tarai zz x y rz)))))
                  ((== z 0) (tarai 0 x y r<)))
                (tarai rx ry rz r)))))
            ((>=o x y) (== x y))))))

Answer 3

我是guile-log的开发人员，这是一个基于guile方案的逻辑编程环境，它同时具有minikanren结构和prolog结构，并且可以混合使用它们。它还有一个移植的clpfd库，所以在这里你可以做以下事情(不能自动柜员机，它不能工作(这是我正在解决的一个bug ))。假设导入了clpfd。(，，；是交错的kanren like ops)。将、、和；替换为；，您得到的代码可以使用clpfd库在例如swi prolog上运行。

tarai(X,Y,Z,W) :-
 (
   X #> Y , 
   (
     (
       ((X #> 0 , XX #= X - 1, tarai(XX,Y,Z,RX)) ;;
        (X  = 0 , tarai(0,Y,Z,RX))) ,,
       ((Y #> 0 , YY #= Y - 1, tarai(YY,Z,X,RY)) ;;
        (Y =  0 , tarai(0,Z,X,RY))) ,,
       ((Z #> 0 , ZZ #= Z - 1, tarai(ZZ,X,Y,RZ)) ;;
        (Z =  0 , tarai(0,X,Y,RZ)))
     ) ,,
     tarai(RX,TY,RZ,R)
   )
 ) ;;
 (X #=< Y, R=Y).