如何在 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 函数，没有统一的那些因此实现 X,Y,Z 的逻辑可以在没有 kanren 变量的情况下完成。但是，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

要在 guile-log 方案宏接口see links on this site 中进行确定性验证，您可以使用 memoization 来实现它（没有 memoization，解决方案会破坏 guile-log 上的变量堆栈）

(define tarai 
  (memo 
    (<lambda> (x y z r) 
       (if (> x y) 
           (<var> (rx ry rz) 
              (<and> 
                 (tarai (max (- x 1) 0) y z rx) 
                 (tarai (max (- y 1) 0) z x ry) 
                 (tarai (max (- z 1) 0) x y rz) 
                 (tarai (<lookup> rx) (<lookup> ry) (<lookup> rz) r))) 
           (<=> r y)))))

scheme@(guile-user)> ,time (<run> 1 (r) (tarai 12 6 0 r))
$13 = (12)
;; 0.293411s real time, 0.290711s run time.  0.000000s spent in GC.
scheme@(guile-user)> 

Answer 3

我尝试使用 clpfd 运行例如 tarai(12,X,0,12)，但它太复杂了。并且记忆不适用于 swipl 的属性变量。因此，我能找到的最佳解决方案 atm 是将确定性记忆 tarai 与类似的东西一起使用

tarai2(X,Y,Z,W) :-
  (var(X)->between(0,20,X);true),
  (var(Y)->between(0,20,Y);true),
  (var(z)->between(0,20,Z);true),
  tarai(X,Y,Z,W).

然后可以很容易地找到该范围内的所有解 Y,Z 与 tarai2(12,Y,Z,12)。

Answer 4

这个问题被重新提出来询问如何在 prolog 规范中实现更通用版本的 tarai 函数，该版本允许 x、y、z 字段中的变量。这里的技术可以在 prolog 中实现，例如kanren 需要 clpfd 有限域求解器和类似的东西（参见上面的评论讨论，例如对 numbers.scm 的引用）。关键是 nuke -> 并在所有情况下使用警卫，我们将假设运算符 >o =o 0 会将 X 限制为值 1,2 ,3,...)。此外，我们将假设通过特殊的“iso”使用区间算术约束为此类变量定义了“-o”。使用它，我们可以将 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 5

我是guile-log 的开发人员，这是一个基于 guile 方案的逻辑编程环境，它同时具有 minikanren 构造和 prolog 构造，并且可以混合使用它们。它还移植了一个 clpfd 库，因此您可以在这里执行以下操作（不幸的是 atm 它不起作用（我正在处理的一个错误））。假设导入了 clpfd。 （,, ;; 像操作一样交错看人）。将 ,, 替换为 , 和 ;;和 ;您可以使用 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).

Answer 6

这是一个缓慢的实现，它是声明性的，并使用numbers.scm（如问题作者所建议的那样）和 minkanren。

(load "minkanren.scm)
(load "numbers.scm")

(define one  (build-num 1))
(define zero (build-num 0))
(define (tarai x y z r)
    (conde
        ((<=o x y) (== r y))
        ((<o y x)
         (fresh (rx ry rz)
          (conde
           ((fresh (xx)
            (conde
             ((<o zero x) (minuso x one xx) (tarai xx y z rx))
             ((== zero x) (tarai zero y z rx))))
           (fresh (yy)
            (conde
             ((<o zero y) (minuso y one yy) (tarai yy z x ry))
             ((== zero y) (tarai zero z x ry))))
           (fresh (zz)
            (conde
             ((<o zero z) (minuso z one zz) (tarai zz x y rz))
             ((== zero z) (tarai zero x y rz))))
           (tarai rx ry rz r)))))))

如果推导方向相反（所以我们添加数字）由于声明式风格我们仍然可以解决，

tarai(4,2,Z,4):, (you need to make binaries of the number) will lead to
Y = [0, 1],
W = [0, 0, 1],
Z = [0, 0, 1],
X = [0, 0, 1].

假设如果添加表格：

tarai(12,6,0,W):
Z = (),
X = [0, 0, 1, 1],
Y = [0, 1, 1],
W = [0, 0, 1, 1].