Как реализовать тараи в хитрости

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

Я разработчик guile-log — среды логического программирования на схеме хитрости, которая как конструкции миниканрена, так и конструкции пролога, и их можно смешивать. Он также имеет портированную библиотеку clpfd, поэтому здесь вы можете сделать следующее (к сожалению, это не работает (ошибка, над которой я работаю)). Предположим, что clpfd импортирован. (,, ;; чередует kanren как 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).

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

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

Чтобы сделать детерминированную версию в макроинтерфейсе схемы 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)> 

Это медленная декларативная реализация, использующая numbers.scm ( как предлагает автор вопроса) и минканрен.

(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].