Fork me on GitHub
#core-logic
<
2018-09-12
>
risto10:09:11

hi everyone

risto10:09:25

i'm trying to figure out what's making appendo terminate, from the looks of it, it seems like it should just be infinite like anyo

risto10:09:30

does anyone have any insight into that?

hiredman16:09:00

it is a recursive goal with 3 args (x y z) and 2 cases. the first case is the base case and is only true if x unifies with the empty list and z unifies with y, the second case is only true if the first element of x and the first element of z unify, and if it is true it calls appendo again with the rest of x, y, and the rest of z

hiredman16:09:27

so it must terminate because every step where case 2 matches causes the recursive call to be made with the rest of x, so the x argument gets smaller and smaller, until case 2 no long holds and case 1 might hold

risto18:09:44

that makes sense, but the issue for me is how conj and disj are implemented

risto18:09:09

even though it's a lazy stream, conj is implemented using flatmap and disj with a fair append

risto18:09:27

so it seems like it would continue to recurse forever, because under the hood it's calling flatmap or append

hiredman18:09:45

are you actually asking about core.logic or minikanren? because flatmap isn't a string that appears in core.logic

hiredman18:09:40

append is not the same thing as appendo

risto18:09:44

isn't core.logic an implementation of minikanren?

risto18:09:42

(def appendo [xs ys out]
   (conde
     [(eq xs []) (eq ys out)]
     [(fresh [first rest rec]
        (conso first rest xs)
        (conso first rec out)
        (appendo rest ys out))]))
here fresh is calling call-fresh and conj under the hood, and conj is implemented using flatmap aka bind aka mapcat-stream

risto18:09:09

so it would just keep going forever it seems, like anyo

hiredman18:09:00

you are confusing goals implemented in core.logic with functions implemented in clojure

👍 4
risto18:09:23

why do you think i'm confusing it with functions in clojure?

hiredman18:09:52

actually it is hard to say, because call-fresh doesn't exist in core.logic either

hiredman18:09:14

because conj in clojure is the function clojure.core/conj which is definitely not implemented using flatmap

hiredman18:09:47

there is a core.logic goal called conjo, which is a constraint goal, which is kind of a different kettle of fish

risto18:09:58

ah i see the confusion, i'm referring to the names of these things from the minikanren implementation

risto18:09:12

maybe core.logic is using a different scheme for it, but it's implementing minikanren under the hood

risto18:09:37

yeah i meant conjo, sorry

risto18:09:04

it has something called conj under the hood which isn't a goal

risto18:09:12

but not the same as clojure.core/conj

hiredman18:09:12

it is minikanren in a kind of hand wavey sense, it isn't a direct port

hiredman18:09:23

I don't think core-logic's conjo is the same as conj in minikanren

hiredman18:09:31

I think, and it has been a long time since I've looked at minikanren, conj in mk is an operator on the underlying lazy stream implementation

risto18:09:48

yeah, it has a minimal implementation at the end of the paper http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

hiredman18:09:50

so it is a level of abstraction problem

risto18:09:54

but that's not enough to stop it from infinitely recursing appendo afaict. It might be because it's such a minimal implementation of kanren that they leave out the more important parts to make something like appendo work, not sure

hiredman18:09:03

mk is not implemented in mk

hiredman18:09:41

micro kanren is another thing again

risto18:09:08

what's the difference between minikanren and microkaren? microkanren is just an even more minimal version of kanren?

risto18:09:56

its on the minikanren website, i thought it was the same thing

hiredman18:09:52

yeah, it is an even more stripped down version

risto18:09:22

anyways, it says on the minikaren website that core.logic is an implementation of it.. even if it deviates somewhat it has to have some way of making sure appendo doesn't just recurse forever. I guess my question is how they manage to pull that off without ending up with a neverending stream like anyo