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

Question

Я пытался понять обычай 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?

Answer 1

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 мы не хотим совпадать. [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))]))