Уточнение алгоритмов поиска в различных реализациях миниканрена
В настоящее время я изучаю miniKanren от The Reasoned Schemer and Racket.
У меня есть три варианта реализации миниканрена:
Обоснованный интриган, первое издание (MIT Press, 2005). Я назвал это
https://github.com/miniKanren/TheReasonedSchemer
PS. Он говорит, что
condiбыл заменен улучшенной версией, которая выполняет чередование.The Reasoned Schemer, второе издание (MIT Press, 2018). Я назвал это
https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd
Обоснованный интриган, первое издание (MIT Press, 2005). Я назвал это
Я провел несколько экспериментов по поводу трех приведенных выше реализаций:
1-й эксперимент:
(run* (r)
(fresh (x y)
(conde
((== 'a x) (conde
((== 'c y) )
((== 'd y))))
((== 'b x) (conde
((== 'e y) )
((== 'f y)))))
(== `(,x ,y) r)))
;; => '((a c) (a d) (b e) (b f))
(run* (x y)
(conde
((== 'a x) (conde
((== 'c y) )
((== 'd y))))
((== 'b x) (conde
((== 'e y) )
((== 'f y))))))
;; => '((a c) (a d) (b e) (b f))
(run* (r)
(fresh (x y)
(conde
((== 'a x) (conde
((== 'c y) )
((== 'd y))))
((== 'b x) (conde
((== 'e y) )
((== 'f y)))))
(== `(,x ,y) r)))
;; => '((a c) (b e) (a d) (b f))
Обратите внимание, что в первом эксперименте и дал тот же результат, но дал другой результат.
Кажется, что
conde in и использовать тот же алгоритм поиска, но использовать другой алгоритм.
2-й эксперимент:
(define listo
(lambda (l)
(conde
((nullo l) succeed)
((pairo l)
(fresh (d)
(cdro l d)
(listo d)))
(else fail))))
(define lolo
(lambda (l)
(conde
((nullo l) succeed)
((fresh (a)
(caro l a)
(listo a))
(fresh (d)
(cdro l d)
(lolo d)))
(else fail))))
(run 5 (x)
(lolo x))
;; => '(() (()) (() ()) (() () ()) (() () () ()))
(defrel (listo l)
(conde
((nullo l))
((fresh (d)
(cdro l d)
(listo d)))))
(defrel (lolo l)
(conde
((nullo l))
((fresh (a)
(caro l a)
(listo a))
(fresh (d)
(cdro l d)
(lolo d)))))
(run 5 x
(lolo x))
;; => '(() (()) ((_0)) (() ()) ((_0 _1)))
(define listo
(lambda (l)
(conde
((nullo l) succeed)
((pairo l)
(fresh (d)
(cdro l d)
(listo d)))
(else fail))))
(define lolo
(lambda (l)
(conde
((nullo l) succeed)
((fresh (a)
(caro l a)
(listo a))
(fresh (d)
(cdro l d)
(lolo d)))
(else fail))))
(run 5 (x)
(lolo x))
;; => '(() (()) ((_.0)) (() ()) ((_.0 _.1)))
Обратите внимание, что во втором эксперименте и дал тот же результат, но дал другой результат.
Кажется, что кондей в
TRS2 а также
TRS1* использовать тот же алгоритм поиска, но
TRS1 используйте другой алгоритм.
Это меня очень смущает.
Может ли кто-нибудь помочь мне прояснить эти разные алгоритмы поиска в каждой реализации minikanren выше?
Большое спасибо.
2 ответа
Думаю, после нескольких дней исследований я смог ответить на этот вопрос.
1. Разъяснение концепции
Прежде всего, хотелось бы прояснить некоторые понятия:
Есть две хорошо известные модели недетерминированных вычислений: модель потока и модель двух продолжений. Большинство реализаций miniKanren используют потоковую модель.
PS. Термин «поиск с возвратом» обычно означает поиск в глубину (DFS), который может быть смоделирован либо потоковой моделью, либо моделью двух продолжений.
2. Объясните различные версии оператора или
2.1 и в
предоставляет два конструктора целей для недетерминированного выбора и.
использует DFS, которую реализует MonadPlus stream.
Недостаток MonadPlus в том, что это нечестно. Когда первая альтернатива предлагает бесконечное количество результатов, вторая альтернатива никогда не пробуется. Это делает поиск неполным.
Чтобы решить эту неполную проблему, введено, что может чередовать два результата.
Проблема в том, что он не может хорошо работать с дивергенцией (я имею в виду мертвую петлю без значения). Например, если первая альтернатива разошлась, вторая альтернатива все равно не может быть испробована.
Это явление описано в главе 6 книги.
Детали реализации:
В, поток - это стандартный поток, то есть ленивый список.
Реализуется:
(define mplus
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f0) (choice a (lambdaf@ () (mplus (f0) f)))))))
Реализуется
mplusi
:(define mplusi
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f0) (choice a (lambdaf@ () (mplusi (f) f0)))))) ; interleaving
2,2 дюйма
удалили два вышеуказанных конструктора ворот и предоставили новый.
То же, что и, но только чередование, когда первой альтернативой является возвращаемое значение отношения, которое определяется. Так что на самом деле он больше похож на старый, если вы его не используете.
Также исправлена указанная выше проблема.
Детали реализации:
В поток не является стандартным потоком.
Как говорится в книге,
Поток - это либо пустой список, либо пара, cdr которой является потоком, либо приостановка.
Приостановка - это функция, сформированная из (lambda () body), где ((lambda () body)) - это поток.
Итак, потоки не ленивы во всех элементах, а просто ленивы в точках приостановки.
Есть только одно место для первоначального создания приостановки, а именно:
(define-syntax defrel
(syntax-rules ()
((defrel (name x ...) g ...)
(define (name x ...)
(lambda (s)
(lambda ()
((conj g ...) s)))))))
Это разумно, потому что единственный способ дать бесконечные результаты или расходиться - это рекурсивные отношения. Это также означает, что если вы используете
define вместо определения отношения вы столкнетесь с той же проблемой, что и in (это нормально для конечного поиска в глубину).
Реализуется:
(define (append-inf s-inf t-inf)
(cond
((null? s-inf) t-inf)
((pair? s-inf)
(cons (car s-inf)
(append-inf (cdr s-inf) t-inf)))
(else (lambda () ; interleaving when s-inf is a suspension
(append-inf t-inf (s-inf))))))
2.3 дюйм
происходит из ранней статьи «От функций с переменным числом переменных к отношениям с переменным числом аргументов: перспектива miniKanren». As, также удалил два старых конструктора ворот и предоставил новый.
То же, что и in, но только чередование, когда первая альтернатива - это.
Также исправлена указанная выше проблема.
Обратите внимание, что нет in. Следовательно, если рекурсивные отношения не начинаются с, вы столкнетесь с той же проблемой, что и in. Например,
(define (nevero)
(fresh (x)
(nevero)))
(run 2 (q)
(conde
((nevero))
((== #t q))
((== #f q))))
;; => divergence
Мы можем обойти эту проблему, обернув вручную:
(define (nevero)
(conde
((fresh (x)
(nevero)))))
(run 2 (q)
(conde
((nevero))
((== #t q))
((== #f q))
))
;; => '(#t #f)
Детали реализации:
В, стрим стандартный стрим + подвеска.
(define-syntax conde
(syntax-rules ()
((_ (g0 g ...) (g1 g^ ...) ...)
(lambdag@ (s)
(inc ; suspension which represents a incomplete stream
(mplus*
(bind* (g0 s) g ...)
(bind* (g1 s) g^ ...) ...))))))
(define-syntax mplus*
(syntax-rules ()
((_ e) e)
((_ e0 e ...) (mplus e0 (lambdaf@ () (mplus* e ...)))))) ; the 2nd arg of the mplus application must wrap a suspension, because multiple clauses of a conde are just syntactic sugar of nested conde with 2 goals.
Реализуется чередованием:
(define mplus
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f^) (choice a (lambdaf@ () (mplus (f) f^))))
((f^) (inc (mplus (f) f^)))))) ; interleaving when a-inf is a suspension
; assuming f must be a suspension
Обратите внимание, что хотя функция называется
mplus, это не законный MonadPlus, потому что он не подчиняется закону MonadPlus.
3. Объясните эти эксперименты в вопросе.
Теперь я могу объяснить эти эксперименты в вопросе.
1-й эксперимент
=>, потому что это DFS.
=>
'((a c) (a d) (b e) (b f)) , потому что это DFS, если нет
defref вовлеченный.
=>
'((a c) (b e) (a d) (b f)), потому что in - это чередование (самый крайний делает два самых внутренних чередования).
Обратите внимание, что если мы заменим in, результат будет таким же, как.
2-й эксперимент
=>
'(() (()) (() ()) (() () ()) (() () () ())) , потому что в нем есть DFS. Второе предложение in никогда не применяется, с тех пор как
(fresh (d) (cdro l d) (lolo d) является
binded в первом предложении предлагает бесконечное количество результатов.
=>
'(() (()) ((_0)) (() ()) ((_0 _1))) , потому что теперь можно попробовать второе предложение in.
listo а также
loloопределены средствами, которые потенциально могут создать приостановку. Когда
append-inf эти две приостановки, каждая делает шаг, а затем уступает контроль другой.
=>
'(() (()) ((_.0)) (() ()) ((_.0 _.1)), то же самое, за исключением того, что приостановки создаются с помощью.
Обратите внимание, что замена на in не изменит результата. Если вы хотите получить тот же результат, что и или, оберните
alli во втором пункте.
3-й эксперимент
=>
'((a c)), потому что в
TRS1это DFS. В
tmp-rel расходится на.
Обратите внимание, что замена на и
(run 2 ...), мы получим . Это потому, что может чередоваться. Однако он по-прежнему не может распечатать третье решение, потому что
condi не может хорошо работать с дивергенцией.
=>
'((b e) (b f) (a c)) , потому что можно архивировать полный поиск, если мы используем для определения отношения.
Обратите внимание, что окончательный результат
'((b e) (b f) (a c)) вместо того, потому что в
TRS2, приостановка только первоначально создается
defrel. Если мы ожидаем, мы можем обернуть подвеску вручную:
(define-syntax Zzz
(syntax-rules ()
[(_ g) (λ (s) (λ () (g s)))]))
(run 3 r
(fresh (x y)
(conde
((== 'a x) (tmp-rel y))
((== 'b x) (Zzz (conde ; wrap a suspension by Zzz
((== 'e y) )
((== 'f y))))))
(== `(,x ,y) r)))
;; => '((a c) (b e) (b f))
=>
'((a c) (b e)), потому что в
TRS1*, подвесы завернуть в с.
Обратите внимание, что он по-прежнему не может распечатать третье решение.
(b f) так как
tmp-rel-2 не завернутый в
conde, поэтому приостановка здесь не создается. Если мы ожидаем
'((a c) (b e) (b f)), мы можем обернуть подвеску вручную:
(define (tmp-rel-2 y)
(conde ((== 'd y) (tmp-rel-2 y)))) ; wrap a suspension by conde
4. Вывод
В общем, миниканрен - это не один язык, а целые группы языков. У каждой реализации миниканрена может быть свой хак. Могут быть некоторые угловые случаи, которые в разных реализациях ведут себя немного по-разному. К счастью, миниканрен легко понять. Когда мы сталкиваемся с этими угловыми случаями, мы можем решить их, прочитав исходный код.
5. Ссылки
Обоснованный интриган, первое издание (MIT Press, 2005)
От вариативных функций к вариадным отношениям - перспектива miniKanren
The Reasoned Schemer, второе издание (MIT Press, 2018)
µKanren: минимальное функциональное ядро для реляционного программирования
Отслеживание с возвратом, чередование и завершение преобразователей монад
Ваш первый эксперимент в
TRS1 реализация в Прологе ("и"
,, "или"
;) и в эквивалентной символической логической нотации («и» есть, или «есть»), действует как
ex1_TRS1( R )
:= ( X=a, (Y=c ; Y=d) ; X=b, (Y=e ; Y=f) ), R = [X,Y] ;; Prolog
== ( {X=a} * ({Y=c} + {Y=d}) + {X=b} * ({Y=e} + {Y=f}) ) * {R=[X,Y]} ;; Logic
== ( ({X=a}*{Y=c} + {X=a}*{Y=d}) + ({X=b}*{Y=e} + {X=b}*{Y=f}) ) * {R=[X,Y]} ;; 1
----( ( <A> + <B> ) + ( <C> + <D> ) )------------
----( <A> + <B> + <C> + <D> )------------
== ( {X=a}*{Y=c} + {X=a}*{Y=d} + {X=b}*{Y=e} + {X=b}*{Y=f} ) * {R=[X,Y]} ;; 2
== {X=a}*{Y=c}*{R=[X,Y]}
+ {X=a}*{Y=d}*{R=[X,Y]}
+ {X=b}*{Y=e}*{R=[X,Y]}
+ {X=b}*{Y=f}*{R=[X,Y]}
== {X=a}*{Y=c}*{R=[a,c]}
+ {X=a}*{Y=d}*{R=[a,d]}
+ {X=b}*{Y=e}*{R=[b,e]}
+ {X=b}*{Y=f}*{R=[b,f]}
== {R=[a,c]} + {R=[a,d]} + {R=[b,e]} + {R=[b,f]}
;; => ((a c) (a d) (b e) (b f))
В
* операция должна выполнять некоторые проверки, чтобы
{P=1}*{P=2} ==> {}, т. е. вообще ничего, поскольку эти два назначения несовместимы друг с другом. Он также может выполнять упрощения путем подстановки, начиная с
{X=a}*{Y=c}*{R=[X,Y]} к
{X=a}*{Y=c}*{R=[a,c]}.
Очевидно, что в этой реализации
((<A>+<B>)+(<C>+<D>)) == (<A>+<B>+<C>+<D>) (как видно на
;; 1 ->
;; 2шаг). Видимо то же самое и в
TRS2:
ex1_TRS2( [X,Y] ) := ( X=a, (Y=c ; Y=d) ; X=b, (Y=e ; Y=f) ).
;; => ((a c) (a d) (b e) (b f))
Но в
TRS1* порядок результатов другой,
ex1_TRS1_star( R ) := ( X=a, (Y=c ; Y=d) ; X=b, (Y=e ; Y=f) ), R=[X,Y].
;; => ((a c) (b e) (a d) (b f))
так что это должно быть было
((<A>+<B>)+(<C>+<D>)) == (<A>+<C>+<B>+<D>).
Вплоть до заказа результаты такие же.
Алгоритма поиска в книге нет, только алгоритм смешивания потоков решений. Но поскольку потоки ленивы, достигается то же самое.
Вы можете пройти остальные аналогичные процедуры и узнать больше о свойствах
+ в каждой конкретной реализации.