Как осуществить тарай в хитрости

Question

Теперь я хотел бы запустить тарай, который в Прологе выглядит следующим образом. Тестовый случай будет запускать ?- 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.

Меня больше всего интересует, можно ли выполнить контрольный пример поверх полностью декларативной версии некоторого кода miniKanren для tarai. При желании мне было бы интересно запустить несколько тестов в обратном направлении.

Я немного растерялся. Мне удалось установить guile, вариант схемы, и я могу успешно выполнить тестовые примеры miniKanren . Но у miniKanren нет целых чисел, так что же можно сделать?

Answer 1

Я разработчик guile-log среды логического программирования на схеме guile, которая имеет как конструкции minikanren, так и конструкции prolog, и их можно смешивать.Она также имеет портированную библиотеку clpfd, поэтому здесь вы можете сделать следующее (к сожалению, это не работает (ошибка, над которой я работаю)).Предположим, что clpfd импортирован.(,, ;; чередует канрен как ops).Замена ,, с, и ;;с ;Вы получаете код, который может быть запущен, например, на прологе swi, используя библиотеку clpfd.

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 2

Вопрос был отклонен, чтобы спросить, как реализовать более общую версию функции tarai в спецификации пролога, которая допускает переменные в полях x, y, z.Техника здесь может быть реализована в прологе, например, с помощью решателя конечных областей clpfd, и что-то подобное необходимо для kanren (см. Комментарии выше, например, ссылку на numbers.scm).Ключевым моментом является использование nuke -> и использование защиты для всех случаев, и мы будем предполагать, что операторы> o = o <= o все определены для переменных (например, для var 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

Это медленная реализация, которая декларативна и использует 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].

Answer 4

Я попытался запустить, например, tarai (12, X, 0,12) с clpfd, но это сложно для этого. И запоминание не работает с приписанными переменными для swipl. Так что лучшее решение, которое я могу найти, - это использовать детерминированный записанный тарай с чем-то вроде

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 5

Для создания детерминированной версии в макроинтерфейсе схемы guile-log см. Ссылки на этом сайте вы можете реализовать это с памяткой, так как (без памятования решение выдает стек переменных в 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 6

Обратите внимание, что этот алгоритм имеет только одно решение, если он существует и является детерминированным.Вы можете передать переменные схемы как x, y, z непосредственно в функцию Канрена Тараи, для тех, кто не может объединить логические функции для X, Y, Z, можно обойтись без переменных Канрена.Однако значения R должны быть логическими переменными, и вам нужно получить ограниченные значения в форме тараев (Rx, Ry, Rz, R), например, найти значения Rx, Ry, Rz и передать их в функцию тарай.Также вам необходимо убедиться, что эта форма выполняется после завершения первых трех форм (что легко сделать, потому что нет чистого множественного выбора), чтобы вы знали, что Rx, Ry, Rz ограничены.Также обратите внимание, что этот алгоритм может зависеть от порядка выполнения, чтобы быть выполненным эффективно, но опять же детерминизм означает, что эта точка является прямой для удовлетворения.Обратите внимание, что A -> B;C переводит здесь просто схемы (если ABC), потому что 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)))))