Clojurians Log v2

How does recursion work in core.logic? In other words, what does a recursive logic function look like? Trying to develop a mental model for how e.g. a graph traversal algorithm would work.

It looks the same, you have a conde with cases typically a base case that doesn't recurse and a recursive case that does

Very similar structurally to a recursive non-relation

Because they are relations, not functions, what you are doing is establishing relationships between lvars, and recursive relationships are, uh, I think induction

The often look very similar to datalog rules, so maybe you introduce a new lvar in the recursive case like you would in datalog for a join

interesting, thank you

I’ll play with it until I build an intuition

so if a list is defined as a recursive data type that is either a cons of some item onto a tail list, or an empty list(nil), you can prove an item is a member of a list like: 1. the list is either nil or a cons 2. if the list is nil the proof has failed 3. if the list is a cons and the item in the cons is the same as the item you are looking for, you are done 4. if the list is a cons and the item in the cons is not the same, prove that the item you are looking for is in the tail

look at ACL2S proofs for contains

or member or whatever the equivalent is

which written as core.logic looks like:

(defn membero
  [x l]
  (l/conde
   [(l/== nil l) l/fail]
   [(l/fresh [_]
      (l/conso x _ l))]
   [(l/fresh [_ y]
      (l/conso _ y l)
      (membero x y))]))

you can leave the l/fail case out, if nothing matches it is fail

and core.logic has some macros for doing sort of pattern matchy kinds of things

the actual definition of membero looks like:

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

which is the same set of two cases leaving the nil case out

then moving from lists to trees (or graphs) you just add more cases

so instead of a single case for the tail of the list you have a case for the left or right branch of a tree or whatever

which is part of the magic of core.logic, all the cases are explored simultaneously for you, so if you have more than one recursive case it is fine, and you don't have to worry about backtracking and trying another branch

something to keep in mind as well is core.logic has built in support for working with lists relationally (firsto, resto, conso, etc) and if you have some custom graph data structure, you'll either have to write your own relations for constructing/deconstructing nodes in the graph, or operate it non-relationally, which can trip you up