Требуется разъяснение в понимании пользовательского ограничения core.logic - PullRequest
Новая
       43

Требуется разъяснение в понимании пользовательского ограничения core.logic

1 голос
/ 07 июля 2019

Я пытался понять пользовательское ограничение core.logic, как определено ниже, 

(defne lefto
  "x appears to the left of y in collection l."
  [x y l]
  ([_ _ [x . tail]] (membero y tail))
  ([_ _ [_ . tail]] (lefto x y tail)))

Как интерпретировать _ и . в контексте core.logic?

1 Ответ

2 голосов
/ 07 июля 2019

defne - это макрос, который использует специальный синтаксис сопоставления с образцом, но ведет себя подобно conde. (К вашему сведению e в каждом из них означает «все», то есть каждый пункт может внести свой вклад.)

  • Подчеркивание _ указывает значение, которое должно присутствовать, но вам все равно, что это такое.
  • . указывает на объединение элементов слева от . и хвост списка справа от .. Это используется для привязки как отдельных элементов списка, так и остальной части списка к различным значениям. (Также см. llist в core.logic.)

Аналогичная деструктуризация последовательности в Clojure будет использовать & вместо .: 

(let [[_ _ [_ & tail]] coll] ...)

Таким образом, следующий шаблон означает: «нас не волнует первый или второй входной аргумент, но третий должен быть списком, в котором наша голова равна x (т.е. равна x входному аргументу функции) и привязать хвост к tail ": 

[_ _ [x . tail]]

Также обратите внимание, что tail может быть здесь пустым списком, и вы можете связать более одного значения до ..

Поскольку ваш пример является рекурсивной целью, он в конечном итоге завершится, либо найдя x до y, либо не сможет соответствовать ни одному из шаблонов, поскольку l будет (в конце концов) пустым списком (), который не будет соответствовать ни одному случаю.

Более простой пример

Само определение membero является более простым примером той же идеи: 

(defne membero
  "A relation where l is a collection, such that l contains x."
  [x l]
  ([_ [x . tail]])
  ([_ [head . tail]]
    (membero x tail)))

Есть два предложения, каждое из которых представлено списком верхнего уровня ():

  1. [_ [x . tail]] - Первый _ представляет собой ввод x arg, который нам не нужен, чтобы соответствовал on [x . tail] описывает шаблон для второго аргумента l, где, если x является заголовком l, то этот шаблон совпадает и membero успешно.
  2. [_ [head . tail] - _ означает здесь то же самое. Но обратите внимание, мы дали новое имя главе l, который должен быть непустым списком, чтобы соответствовать этому шаблону. Если он совпадает, то мы продолжаем поиск с (membero x tail).

Только первое предложение может сделать цель успешной, найдя x в (под) списке l; второй пункт используется только для деструктуры head и tail из l и рекурсии.

Вот membero переведено с conde и без сопоставления с шаблоном: 

(defn memberoo [x l]
  (conde
    [(fresh [a d]
       (conso a d l)
       (== a x))]
    [(fresh [a d]
       (conso a d l)
       (memberoo x d))]))
...