I was trying to understand a custom core.logic constraint as defined below,

(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)))

How to interpret _ and . in the context of core.logic?

defne is a macro that uses a special pattern matching syntax, but behaves similarly to conde. (FYI the e in each of these stands for "everything" i.e. every clause can contribute.)

• The _ underscores indicate a value that must be present, but you don't care what it is.
• The . indicates a concatenation of items to the left of . and the tail of the list to the right of .. This is used to bind both individual items of a list and the remainder of the list to different values. (Also see llist in core.logic.)

A similar destructuring of a sequence in Clojure would use & instead of .:

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

So the following pattern means "we don't care about the first or second input argument, but the third should be a list where we the head is x (i.e. equal to the function's x input argument) and bind the tail to tail":

[_ _ [x . tail]]

Also note that tail can be the empty list here, and you can bind more than one value before the ..

Since your example is a recursive goal, it will eventually terminate by either finding x before y, or it will fail to match either pattern because l will (eventually) be the empty list () which won't match either case.

Simpler example

The membero definition itself is a simpler example of the same idea:

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

There are two clauses, each represented by a top-level list ():

1. [_ [x . tail]] - The first _ represents the input x arg we don't care to match on. The [x . tail] describes a pattern for the second argument l where if x is the head of l, then this pattern matches and membero succeeds.
2. [_ [head . tail] - The _ means the same thing here. But notice we've given a new name to the head of l, which only needs to be a non-empty list to satisfy this pattern. If it matches, then we recurse with (membero x tail) to continue searching.

Only the first clause can make the goal successful, by finding x in a (sub)list of l; the second clause is only used to destructure the head and tail of l and recurse.

Here's membero translated with conde and no pattern matching:

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