Thanks for the links, Alex! Those are interesting looking papers! I'm especially interested in the search variants, search visualization, and engine generation.
miniKanren doesn't perform backtracking, either. The implementation is purely functional, and the search is based on streams. The occurs check is important for some applications, such as writing a type inferencer as a relation. For example, in simply typed lambda calculus, self-applications such as (f f) should not type check. The occurs check ensures self-application fails. Older versions of miniKanren only support the (run* (w) (fresh (p q) (== w (list p q) (...expression in p and q...)) syntax. I thought core.logic supported multiple query variables. If not, it's only a macro away! :) We have added a few constraints beyond == (unification): * =/= (disequality constraints) * symbolo and numbero (run-time type constraints) * absento (ensures a term t1 does not appear in term t2) core.logic supports disequality constraints, and also finite domain constraints for arithmetic. symbolo and numbero are easily added to core.logic. absento can also be added. The answers for some of the constraints aren't in simplest form, however. If you are interested in fixing up the core.logic reifier, let me know! In short, the core.logic version can *almost* do everything we're doing for program synthesis, for example. It would take a little bit of work to get core.logic up to date with our latest constraints. The benefit would be that we could then use the nice core.logic finite domain solver to add arithmetic to the relational interpreter. I should point out that Greg Rosenblatt has been specializing the relational interpreter used for program synthesis, as in Barliman (https://github.com/webyrd/Barliman). The current version works in Racket and Scheme. I'm sure it can be ported to core.logic, but that also would take a little bit of work. Cheers, --Will On Wednesday, November 16, 2016 at 3:25:07 AM UTC-7, Alex Gian wrote: > > Hi Will > > Thanks for the reply and the offer, I may well take you up on it at some > stage. At the moment I am still finding out what KanRen *can* do, hey, I > only started on Reasoned Schemer last night, LOL.. I think there might > some interesting dimensions there, which were not present in Oz, I think > you touched on some of them in your "A Vision for Relational Programming in > KanRen" video, which was absolutely brilliant, BTW, cheers! > It's been a while since I've done any elementary Prolog courses, but I > think the enforced occurs check leads to some interesting ideas. > > I'll probably be popping by one of your hangouts when I'm a little more *au > fait* with MiniKanren and particularly core.logic, since my applications > are currently more in Clojure than Scheme. > > I do believe that control of the search mechanism is important, and it > would be cool to see something like it in a Kanren of the future! I never > got round to using Ciao Prolog but that sounds like the sort of thing I'm > on about. In Oz any procedure can be searched by any search engine (i.e. > "run" mechanism), so I guess, yes, you can combine different types of > searches and nest them, though I've never done it. > > Incidentally the bible for Oz is CTM > <https://mitpress.mit.edu/books/concepts-techniques-and-models-computer-programming>, > > which has been very widely acclaimed as the new SICP! > Oz itself, as well as being relational, offering logic-style variables, is > also a dataflow language, which means computations can block until data is > sufficiently instantiated to proceed. The internal model is that of a > constraint store. Its final great feature is "computational spaces" which > allow propagation/spawning of candidate solutions without backtracking > through cloning, merging any successful branches back into the original. > Best manual for this, and how alternative searches are performed is > probably Programming Constraint Services > <https://pdfs.semanticscholar.org/6d12/db1f1339d37258f23843fe2896b13dd816d6.pdf> > > which I also just found in a slightly more abridged presentation > <https://www.ps.uni-saarland.de/courses/seminar-ws04/papers/halachev.pdf>. > Other papers with some interesting approaches to graphical tools for > programmable search here > <https://www.comp.nus.edu.sg/~henz/publications/pdf/stk.pdf> (nice > interfaces), and also here > <http://www.ps.uni-saarland.de/Papers/abstracts/abstractionsMOZ04.pdf>. > > Sorry for the "hijack" I don't mean to prattle on too much about Oz, but > there may be some useful ideas there, especially for core.logic, which has > the full backing of the Java arsenal for graphics. Incidentally, I noticed > that the core.logic implementation was not as flexible as the Scheme one, > for instance not allowing > (run* (p q) (...expression in p and q...)) ; as per your Vision video > and forcing the use of > (run* (w) (fresh (p q) (== w (list p q) (...expression in p and q...)) > ; similar to my Oz example above > > OTHER than this, can you confirm that the two systems are equivalently > powerful? I wouldn't want to start with core.logic only to find that there > is something it cannot do, which the Scheme version can, especially when we > get to the cool logic/proof stuff! > > Finally, please excuse any clangers I might drop, I am not an academic, > merely a hobbyist, and some areas of my knowledge are a bit sketchy. > > Thanks again for your great work! > I think a good embedded logic system in Clojure will have a *great* > future. > I look forward to chatting in future, especially re logic applications of > Kanren. Some ideas are already in my mind... > > > > > On Tuesday, November 15, 2016 at 11:36:17 PM UTC, William Byrd wrote: >> >> Hi Alex! Welcome! :) >> >> [etc...] >> > > -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
