Подтвердить что ты не робот

Conda, condi, conde, condu

Я читаю Рассматриваемый Schemer.

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

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

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

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

4b9b3361

Ответ 1

В терминах Prolog 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" заключается в создании цели "try", которая должна быть вызвана с целью продолжения отказа:
    (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 &&: ... ||~ ... 

Ответ 2

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

Ответ 3

В качестве примера, используя 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: оба будут останавливаться после первой успешной группы (сверху вниз)

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

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, хотя.

Ответ 4

В соответствии с основным стандартом ISO Prolog контрольные структуры, такие как (,)/2, (;)/2 и (->)/2, вырезаны прозрачными. (* ->)/2 не встречается в основном стандарте ISO Prolog, но обычно системы Prolog реализуют его также прозрачно.

Это означает, что нельзя переводить:

once(A) *-> B;C

В A, !, B; C A, !, B; C Поскольку последние могут быть встроены в другие управляющие структуры, и если между ними существуют разногласия, эти точки выбора также будут исключены. Что, с другой стороны, кажется разумным, если рассматривать это как A → B; C A → B; C,

известный просто как основной стандарт ISO Prolog if-then-else. Определенное таким образом поведение разреза, например, полезно для выхода из повторяющихся циклов без исключения. Обычный шаблон программирования сложнее архивировать с помощью if-then-else.