Differences Between miniKanren and Prolog
minikanren.org
minikanren.org
I'd like to understand the relationship to RDF / SHACL / OWL and Datalog - additionally what about first order logic with relations like it's used in model checkers like smtlib and temporal logics?
Could I build a system based on miniKaren that implements RDF and OWL? Can I do that with Datalog (i.e. cozodb?)
How would you implement something like validation / SHACL with a logic language? Datamotic / XTDB seem to use some idea like a record and offer bitemporality - is this somehwere in the literature described on a theoretical level?
How is the relationship to Hoare-Logic (we had a brief stunt into that for prooving correctness for loops)
Is it a feasable idea to implement something like Apache Jena in a Datalog database like cozodb or is it a conceptually a fools errand?
I only find very theory heavy works and venture capital backed websites that implement some part but I'm missing the bigger picture.
How to make a fast implementation would also be interesting. I just don't seem to see the forest for the trees.
I'm thankful for any hints!
Check out "Simply Logic" -- free ebook. It'll give you an intro into first order predicate logic and Prolog simultaneously.
I'd suggest solving AoC2023 puzzles in Prolog. It'll give you a decent coverage of the language and some of its advanced features.
- A syntax for expressing data or rules
- A semantics for data
- A semantics for logic (e.g. a logical formalization)
- A specific set of logical axioms & rules
- An algorithm for executing a logic program
- A storage system for facts/data
- A query system for facts/data
Most of the things you mention are a bundling of some or all of the above concepts. This makes sense because it's easier to provide working implementations that way.Some systems offer a limited amount of pluggability or alternative implementations for the same concept (e.g, different "solvers" for OWL.)
But I find that there's a pronounced lack of shared formalisms (or even shared knowledge) even around things that logically should be pretty convergent. Especially if they come from different domains originally (logic programming vs. theorem proving vs. constraint programming vs. database theory, for example.)
If you're also into math, it's a beauty in itself (Godel's incompleteness theorem, quantifier elimination for logic formulas about complex numbers). I think there should be a good book on math logic somewhere, but I'm not familiar with books in English.
Guess I'll start slowly and see how far I come. Thanks!
Having that in the standard library of more languages would be so useful. I know minikanren exists, but the page kind of touches on this: it has usually been implemented as an exercise. Minikanren libs in languages where I've wanted them have been incompletely documented, and lacking some of the practical additions.
I also agree that having something similar to core.logic in many other languages would be useful.
Most miniKanren implementations in most languages were created in order for the implementor to better understand miniKanren or logic programming, or because the implementor wanted to experiment with miniKanren-related reseach ideas.
This split between a pragmatic implementation versus a small, simple to implement/understand/teach/hack implementation may be another legacy of miniKanren coming from the Scheme community, which has struggled with this dichotomy for decades.
I seem to recall Kanren being used in the medical field (as medikanren), is that built as a separate language in Racket?
Meanwhile, MiniKanren is not a general purpose programming language. You'll struggle to find a commercial grade interpreter or any of the sort of sophistication even opensource Prolog interpreters typically have. What you do find however is hundreds of re-implementations of mini or micro Kanren in every language, and many academic papers about extensions to it.
> MiniKanren is not a general purpose programming language
and
> you do find ... implementations of mini or micro Kanren in every language
could easily be positives - the idea of being able to do a bit of "logic programming" in your regular language is appealing
My impression is it's fully intended to be implemented as a library in other languages and no one expects there to be a dedicated "commercial grade" MiniKanren interpreter
Much of the success of miniKanren has been due to it not trying to be an Everything Language.
The most pragmatic variant of miniKanren, core.logic in Clojure, was popular because it didn't try to replace Clojure's behavior in general. Clojure programmers don't want to write a web server or financial application in a logic language, but might want just a bit of miniKanren-like reasoning in part of their application.
As pointed out by @giraffe_lady, pragmatic core.logic-like small embedded domain-specific language implementations in other popular languages would be useful.
The original motivation for miniKanren was to have a small, simple, easy to learn/teach/hack implementation of logic programming that could be taught to students learning functional programming in Scheme. microKanren in particular seems to have nailed this, especially since you can wrap macros around microKanren primitives to get miniKanren, and since microKanren can easily be implemented an almost any language. Once again, the fact that miniKanren and microKanren don't try to do everything is probably a key reason for their success from a teaching standpoint.
Too easy and you don’t need logic programming, a bit harder and you reach for proper solvers, so where does embedded logic programming fit?
Prolog takes the view — and mostly exists in the wild — as primarily a non embedded general purpose language. For some applications — eg a stock exchange or an airline booking service — it makes a lot of sense. You could write a web service in Prolog and then call it from other services not written in Prolog.
https://www.youtube.com/watch?v=1_v3l7uY-Ac
(The Architecture of core logic - David Nolen)
The Clojure community is very pragmatic, and uses (or used?) core.logic more like an embedded Prolog than for purely relational programming like in most of the miniKanren research. The fact that core.logic doesn't try to do everything is a benefit in the eye of Clojure programmers, I believe.
I don't know to what extent core.logic is still used in the Clojure community. Datomic uses Datalog as a query language. I don't know if there any any projects that combine Datomic and core.logic; certainly both could be used in the same application.
- if there's some other criterion or fitness measure which you can't easily express in the relational language, then having the relational program generate candidates based on the criteria you _can_ express, and then filtering or selecting from those based on some other code in the host language can be quite appealing. Then the "complete search" idea makes it natural to have the output from running your relational program be a generator in the host language.
- sometimes, even if a search is in an infinite domain, you can have some other good reason (e.g. a generating function?) for knowing how many values meet some set of criteria. A complete search can be stopped after it has found those values, but a naive use of DFS might not find anything.
miniKanren is an embedded logic language.
Now, practically speaking, if you need logical reasoning, you’ve got SWI-Prolog which is highly optimized, mature, actively developed, and has high-level concurrent predicates baked-in. Or (as I’ve done with less success) embed miniKanren in your language of choice and wish yourself luck while you try to get all your cores working on the same problem together.
Edit: found at this - not sure if it's production but at least targeting a practical application and showing tool use cases. http://minikanren.org/workshop/2020/minikanren-2020-paper7.p...