conda, condi, conde, condu

Question

Я читаю the Reasoned Schemer.

У меня есть интуиция о том, как работает conde.

Однако, я не могу найти формальное определение того, что conde/conda/condu/condi сделать.

Я знаю https://www.cs.indiana.edu/~webyrd/, но это похоже на примеры, а не определения.

Существует ли формальное определение conde, conda, condi, condu где-то?

Answer 1

В терминах Пролога, condA является «мягкой вырезать», *-> и condU является «привержен выбор» – сочетание once и мягкой вырезать, так что (once(A) *-> B ; false) выражает разрезание(A, !, B)

A  *-> B ; C %% soft cut, condA 
once(A) *-> B ; C %% committed choice, condU 

В condA, если цель A преуспевает, все решения передаются в первый пункт B, и никакие альтернативные пункты C не рассматриваются. once/1 позволяет достичь цели своего аргумента только один раз (поддерживает только одно решение, если оно есть).

condE является простой дизъюнкции, а condI является дизъюнкции, который чередуется между решениями его составных частей.

---

Вот попытка точно переводить код книги, ж/выход логических переменных и унификации, в 18 строк Haskell (где соседство является кэрри применение функции, и : означает против).Смотрите, если это проясняет вещи:

• последовательного потока комбинации ("mplus "из книги):

(1) []  ++: ys = ys 
    (2) (x:xs) ++: ys = x:(xs ++: ys) 

• Переменный комбинации потоков (" mplusI"):

(3) []  ++/ ys = ys 
    (4) (x:xs) ++/ ys = x:(ys ++/ xs) 

• Последовательная подача ("bind "):

(5) []  >>: g = [] 
    (6) (x:xs) >>: g = g x ++: (xs >>: g) 

• Переменный корма (" bindI"):

(7) []  >>/ g = [] 
    (8) (x:xs) >>/ g = g x ++/ (xs >>/ g) 

• "OR" цель комбинации ("condE "):

(9) (f ||: g) x = f x ++: g x 

• "Переменный OR" сочетание цели (" condI"):

(10) (f ||/ g) x = f x ++/ g x 

• "AND" сочетание цели ("all "):

(11) (f &&: g) x = f x >>: g 

• "Переменный AND" цель комбинации (" allI" из книги):

(12) (f &&/ g) x = f x >>/ g 

• Специальных цели

(13) true x = [x] -- a sigleton list with the same solution repackaged 
    (14) false x = [] -- an empty list, meaning the solution is rejected 

Цель производят потоки (возможно, пустые) (возможно, обновленные) решений, учитывая (возможно, частично) решение проблемы.

правила переписывают для all являются:

(all) = true 
(all g1) = g1 
(all g1 g2 g3 ...) = (\x -> g1 x >>: (all g2 g3 ...)) 
        === g1 &&: (g2 &&: (g3 &&: ...)) 
(allI g1 g2 g3 ...) = (\x -> g1 x >>/ (allI g2 g3 ...)) 
        === g1 &&/ (g2 &&/ (g3 &&/ ...)) 

правила переписывают для condX являются:

(condX) = false 
(condX (else g1 g2 ...)) = (all g1 g2 ...) === g1 &&: (g2 &&: (...)) 
(condX (g1 g2 ...))  = (all g1 g2 ...) === g1 &&: (g2 &&: (...)) 
(condX (g1 g2 ...) (h1 h2 ...) ...) = 
    (ifX g1 (all g2 ...) (ifX h1 (all h2 ...) (...))) 

Для того, чтобы прийти к конечному condE и condI перевод, т здесь нет необходимости реализовывать книги ifE и ifI, так как они снижают далее до простых комбинаций операторов, со всеми операторами, которые считаются правоассоциативная:

(condE (g1 g2 ...) (h1 h2 ...) ...) = 
    (g1 &&: g2 &&: ...) ||: (h1 &&: h2 &&: ...) ||: ... 
(condI (g1 g2 ...) (h1 h2 ...) ...) = 
    (g1 &&: g2 &&: ...) ||/ (h1 &&: h2 &&: ...) ||/ ... 

Таким образом, нет никакой необходимости в специальный «синтаксис» в Haskell, достаточно простых операторов. Любая комбинация может использоваться с &&/ вместо &&: при необходимости. Но OTOH condI также может быть реализован как функция, чтобы принять коллекцию (список, дерево и т. Д.) Целей, которые должны быть выполнены, что будет использовать некоторую разумную стратегию, чтобы выбрать из них наиболее вероятную или наиболее необходимую и т. Д., А не только простое двоичное чередование, как у ||/ оператора (или ifI книги).

Далее, книги condA может быть смоделирована двумя новыми операторами, ~~> и ||~, работающих вместе. Мы можем использовать их естественным образом, как, например,

g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ... ||~ gelse 

, который можно интуитивно считать «IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse».

• «IF-THEN» комбинация цель состоит в том, чтобы произвести «попробовать» цель, которая должна быть вызвана с предохранителями, продолжение цели:

(15) (g ~~> h) f x = case g x of [] -> f x ; ys -> ys >>: h 

• «OR-ELSE» цель сочетание «попробовать «цель и простая цель просто называет ее цель« цель »со второй целью бездействия, поэтому это не более чем удобный синтаксис для автоматической группировки операндов:

мощность

(16) (g ||~ f) x = g f x 

Если оператор ||~ «OR-ELSE» дается меньше связывания энергии, чем оператор ~~> «IF-THEN» и сделал правоассоциативной тоже, и ~~> оператор еще менее обязательным, чем &&: и т.п., чувствительная группировка выше пример автоматически производится в

(g1 ~~> (g2 &&: ...)) ||~ ((h1 ~~> (h2 &&: ...)) ||~ (... ||~ gelse)...) 

Последняя цель в ||~ цепи таким образом, должна быть простой задачей.На самом деле это не ограничение, так как последняя статья condA форма эквивалентна в любом случае простой «AND» - комбинация ее целей (или простая false также может быть использована).

Это все. Мы можем даже больше типов примерочных целей, представленных различными видами «IF» операторов, если мы хотим:

• использование переменного подачи в успешном предложении (модели, что, возможно, было названо condAI , если бы один в книге):

(17) (g ~~>/ h) f x = case g x of [] -> f x ; ys -> ys >>/ h 

• использовать поток успешное решение только раз производить сократить эффект, моделировать condU:

(18) (g ~~>! h) f x = case g x of [] -> f x ; (y:_) -> h y 

, так что, в конце концов, правила переписывают для condA и condU книги просто:

(condA (g1 g2 ...) (h1 h2 ...) ...) = 
     g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ... 

(condU (g1 g2 ...) (h1 h2 ...) ...) = 
     g1 ~~>! g2 &&: ... ||~ h1 ~~>! h2 &&: ... ||~ ... 

Answer 2

Обозначенный Schemer охватывает conda (soft cut) и condu (фиксированный выбор). Вы также найдете объяснения своего поведения в отличном dissertation on miniKanren Уильяма Берда. Вы отметили это сообщение как о core.logic. Чтобы быть ясным, core.logic основан на более поздней версии miniKanren, чем в представленной в The Reasoned Schemer. miniKanren всегда чередует дизъюнктивные цели - condi и варианты чередования больше не существуют. condeiscondi сейчас.

Answer 3

К примеру, с помощью core.logic:

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

user> (run* [w q] 
       (conde [u#] 
         [(or* [(== w 1) (== w 2)]) 
         (== q :first)] 
         [(== q :second)])) 
([_0 :second] [1 :first] [2 :first]) 

Конда и condu: и остановится после первой успешной группы (сверху вниз)

Конда возвращает все результаты из только первой успешной группы.

user> (run* [w q] 
       (conda [u#] 
         [(or* [(== w 1) (== w 2)]) 
         (== q :first)] 
         [(== q :second)])) 
([1 :first] [2 :first]) 

condu возвращает только один результат только из первой успешной группы.

user> (run* [w q] 
       (condu [u#] 
         [(or* [(== w 1) (== w 2)]) 
         (== q :first)] 
         [(== q :second)])) 
([1 :first]) 

Не знаю, что такое condi, хотя.