The whole topic of logic is largely absent at my University - can anyone recommend some literature or a path to follow?
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'd start by learning Prolog. It is a border-line mystical experience. It took me a lot longer to understand Prolog and become effective in it than anything else I've learned, but nothing else has changed my perspective about problem solving more.
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.
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.
Wow 6 volumes. Added to the list. German is also fine if there is literature and I'm trying to work on my math understanding. I also found some interesting papers that solve i.e. datalog using matrices with algebraic methods. https://arxiv.org/abs/1608.00139
Guess I'll start slowly and see how far I come. Thanks!
I share your wish that there were materials that more clearly mapped between these concepts. There's several implicated but separate concerns:
- 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.)
I really wish an approach like clojure's with core.logic was more common. It's been fairly often in my career that I run across small semi-contained problems within a larger codebase that would be very well suited to prolog, but nowhere near worth using a separate language and toolchain for.
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 agree that core.logic seems to have found a sweet spot as a pragmatic embedded domain-specific language. If core.logic had tried to replace more of the Clojure functionality, or had tried to be a stand-alone Everything Language, I doubt it was have been attractive to Clojurers.
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'd say the difference is that Prolog -- and its derivatives like Datalog and Problog -- have seen a huge amount of usage and solve real problems. Commercial implementations like SICStus support varied specialised mission critical systems. Prolog is a general purpose programming language: you can do everything in Prolog and its naturally extended with constraint programming packages.
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.
I can't speak to the relative usefulness, performance etc of the two paradigms... but:
> 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.
If you know of a few serious applications of miniKanren in the wild, it would be great to see. I also like the idea of logic programming as a library but I’ve seen enough Prolog to know that making logic programming viable takes a sophisticated interpreter, and I’ve yet to see Kanren indispensable to an application.
Could be a positive but is it? What does a non-toy problem requiring a bit of logic programming look like? Perhaps a routing or a scheduling problem? Would you not use a MIP or a constraint solver for that? They are typically callable from host languages.
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.
One success story of core.logic was its use in Threat Grid's software, which apparently ran core.logic on a cluster. Threat Grid was bought out by Cisco for an undisclosed--but apparently large--amount of money.
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.
One area of frustration I've had when trying to get minikanren to actually "do" stuff is that the interleaving search, while "complete" is extremely sensitive to the specific way one declares relations. The order in which one introduces variables and relations between them can meaningfully change how long it must search before it finds a first returned value. While I understand the complaint by Byrd and colleagues that in Prolog, you end up writing to the implementation specifics of the search procedure (in a way which isn't 'logical'), I think you effectively still do this in minikanren, but the tools you have to do it are less explicit.
I think in reality no-one rarely cares for "complete" search because you're typically trying to do the least amount of searching possible. Its easy to write a breadth first Prolog meta-interpreter in a few lines of code, but it just isnt that useful. In Prolog we use dynamic predicates and tabling to make all sorts of problems viable that wouldn't be without it. miniKanren just doesn't have the add-ons needed for broad practical use.
I think there are a few cases when one can legitimately care about "complete" search, especially if embedding minikanren in another language:
- 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.
Another huge area of frustration is the almost complete lack of documentation. Reading pages of undocumented code to guess what functionality is there, and for which inputs it even works, is a frustrating endeavour.
Prolog is an inspired revelation of the equivalence of logical relationships and sequential computation. Expressiveness and meta-programming capabilities in its homoiconic syntax are off the charts. Caveats (of which there are many) aside, Prolog is an exemplary achievement of humankind.
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.
Sort of random question: how difficult is it to write a decent Prolog interpreter? I read somewhere that you need to implement the WAM to get efficiency, but I don't know if that's true, and if it is true, how difficult is it to write a WAM?
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!