Конда, Конди, Конде, Проводник
Я читаю Разумный интриган.
У меня есть некоторая интуиция о том, как conde работает.
Тем не менее, я не могу найти формальное определение того, что conde/conda/condu/condi делать.
Я знаю о https://www.cs.indiana.edu/~webyrd/ но, похоже, есть примеры, а не определения.
Есть ли формальное определение conde, conda, condi, condu где-то?
3 ответа
С точки зрения Пролога, 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 не требуется никакого специального "синтаксиса", достаточно простых операторов. Любая комбинация может быть использована с &&/ вместо &&: если нужно. Но ОТОХ condI также может быть реализован как функция для принятия набора (список, дерево и т. д.) целей, которые должны быть выполнены, который будет использовать некоторую умную стратегию, чтобы выбрать из них наиболее вероятную или наиболее необходимую и т. д., а не просто двоичное чередование, как в ||/ оператор (или ifI книги).
Далее книга condA может моделироваться двумя новыми операторами, ~~> а также ||~, работать вместе. Мы можем использовать их естественным путем, как, например,
g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ... ||~ gelse
который может быть интуитивно понят как " IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse ".
- "
IF-THENКомбинация "цель"- это создание цели "try", которая должна вызываться с целью продолжения отказа:
(15) (g ~~> h) f x = case g x of [] -> f x ; ys -> ys >>: h
- "
OR-ELSEКомбинация цели из цели "try" и простой цели просто называет свою цель "try" со второй целью "по ошибке", так что это всего лишь вспомогательный синтаксис для автоматической группировки операндов:
(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 &&: ... ||~ ...
Разумный Schemer покрывает conda (мягкое сокращение) и wire (совершенный выбор). Вы также найдете объяснения их поведения в превосходной диссертации Уильяма Берда о мини-Канрене. Вы отметили это сообщение как о core.logic. Чтобы быть ясным, core.logic основан на более новой версии miniKanren, чем та, что представлена в The Reasoned Schemer. miniKanren всегда чередует дизъюнктивные цели - condi и чередующихся вариантов больше не существует. conde теперь condi.
Например, используя core.logic:
conde запустит каждую группу, преуспеет, если хотя бы одна группа преуспеет, и вернет все результаты из всех успешных групп.
user> (run* [w q]
(conde [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([_0 :second] [1 :first] [2 :first])
Conda и Condu: оба остановятся после первой успешной группы (сверху вниз)
Конда возвращает все результаты только из первой успешной группы.
user> (run* [w q]
(conda [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([1 :first] [2 :first])
Проводник возвращает только один результат только из первой успешной группы.
user> (run* [w q]
(condu [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([1 :first])
Хотя понятия не имею, что делает condi.
В соответствии с основным стандартом ISO Prolog контрольные структуры, такие как (,)/2, (;)/2 и (->)/2, вырезаны прозрачными. (*->)/2 не встречается в основном стандарте ISO Prolog, но обычно системы Prolog реализуют его также прозрачно.
Это означает, что нельзя переводить:
once(A) *-> B;C
В A, !, B; C, Поскольку последние могут быть встроены в другие управляющие структуры, и если между ними существуют разногласия, эти точки выбора также будут исключены. Что, с другой стороны, кажется разумным, чтобы рассматривать это как A -> B; C,
известный просто как основной стандарт ISO Prolog if-then-else. Определенное таким образом поведение разреза, например, полезно для выхода из повторяющихся циклов без исключения. Обычный шаблон программирования сложнее архивировать с помощью if-then-else.