Nicolás Berger <nicober...@gmail.com> writes: Hi Nicolás,
>> I've simplified the code a bit so that I don't need the `cconso` > >> relation. > > That's great. It's easier to understand this way. To simplify a tiny > bit more, the `nf` lvar can also be removed: it's unified with `f`, so > f can be used instead of nf in `(conso nf nr nl)` Ah, right. >> Ok, and now the backwards case: >> ... >> ... >> Well, that loops forever. > > I found the cause of non-termination. Before the long explanation, you > might want to open my full working version from > https://gist.github.com/nberger/6b0ad2a68c52a6005c6a > > When `l` is not ground (the backwards case), there's no constraint > that prevents it from being any arbitrary long list, so isorto and > inserto are indefinitely tried recursively looking for solutions based > on those lists. Arbitrary long `l`s generate arbitrary long `acc`s. Yeah, I've guessed that, too. > I tried avoiding this issue by adding a `(permuteo l sl)` in the > 2-arity version of isorto, which one would say it's a relation that > must hold between l and sl, but it yielded a similar result. Hehe, and that was also what I've tried to somehow put the information that both lists must be equally long in there. But I guess that would have degraded the algorithm to a naive sort, i.e., filtering the sorted permutations from all permutations instead of building a sorted list by adding values at the right positions. > I finally made it work by adding a (non-relational) goal that fails > when acc is going to be longer than sl: > > (project [sl acc] > (if (and (not (lvar? sl)) > (= (count acc) (count sl))) > fail ; acc is already long as sl, let's stop here > s#)) > > We have to first check that sl is ground (not an lvar) so we can take > its count. Oh, that's great. >> Too bad that lazy sequences aren't printed in a readable way. > > I used this slightly different version of trace-lvar which calls > pr-str to help with this: > > (defn trace-lvar [a lvar] > `(println (format "%5s = %s" (str '~lvar) (pr-str (-reify ~a ~lvar))))) > > A 3-arity version of trace-lvar that takes a transformation fn to > apply to the reified value might be handy. Thanks! >> And why are the sorted lists sl of isorto and nl of inserto always >> (the same?) fresh variable _0? I had expected that during the >> recursion, more information should be added so that their value >> builds up like >> >> sl = (1 2 . some-lvar) >> >> where some-lvar will eventually during the next recursion be fixed to >> the list (3). > > In the forward case, sl has to always be the same fresh variable > because it's our "output" lvar that will get unified with acc when l > gets to be empty. That also explains that in the end, nl and sl are > unified to the same var. See this: > > (inserto f acc nacc) ; nacc will be nl in inserto > (isorto r nacc sl) ; nacc will be acc in isorto, and it will be unified with > sl Ok, I see. > Before closing, a minor thing: > > - I had to replace the conda in inserto with conde, because when l is > not ground (so x is also not ground) we want to try both branches. Yes, conde is the right thing of course. I just put a conda there to see if this changes anything wrt termination. > That's what I found. Hope it helps :) It does! I'm really happy that I haven't been too far off the right solution. And I think the approach is good: specify the problem fully relational, and if it won't terminate, add some non-relational constraints that cut the divering paths. Bye, Tassilo -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en --- You received this message because you are subscribed to the Google Groups "Clojure" group. To unsubscribe from this group and stop receiving emails from it, send an email to clojure+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
