Clojurians Log v2
core-logic 2021-01-12
@him has joined the channel
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