hi everyone

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

does anyone have any insight into that?

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

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

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

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

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

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

append is not the same thing as appendo

isn't core.logic an implementation of minikanren?

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

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

no

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

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

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

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

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

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

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

yeah i meant conjo, sorry

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

but not the same as clojure.core/conj

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

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

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

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

so it is a level of abstraction problem

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

mk is not implemented in mk

micro kanren is another thing again

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

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

yeah, it is an even more stripped down version

yeah

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