William Byrd on Logic and Relational Programming, MiniKanren (2014)

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
  • Shin-Barliman

    Research project: Program synthesis using updated interface, template and types.

  • https://dl.acm.org/doi/10.1145/3358502.3361269

    As far as Barliman, we took a step back from imrpoving the interface, and started doing experiments with a bunch of colleagues on various ways to improve synthesis speed and expressiveness.

    Until COVID-19 got in the way, Kanae Tsushima and I were beginning to put some of the pieces back together in an improved Barliman, named `新-Barliman` (`Shin-Barliman`, `shin` meaning "new" in Japanese):

    https://github.com/k-tsushima/Shin-Barliman

    I'm hoping we will make some real progress again soon!

  • mediKanren

    Proof-of-concept for reasoning over the SemMedDB knowledge base, using miniKanren + heuristics + indexing.

  • Hi Kamaal!

    I know Cisco is using core.logic, which is David Nolen's Clojure variant of miniKanren, in their ThreatGrid product. I think the Enterprisey uses of mediKanren are a bit different than the purely relational programming that I find most interesting, though.

    Having said that, we are now on our second generation of mediKanren, which is software that performs reasoning over large biomedical knowledge graphs:

    https://github.com/webyrd/mediKanren/tree/master/medikanren2

    mediKanren is being developed by the Hugh Kaul Precision Medicine Institute at the University of Alabama at Birmingham (HKPMI). HKPMI is run by Matt Might, who you may know from his work on abstract interpretation and parsing with derivatives, or from his more recent work on precision medicine. mediKanren is part of the NIH NCATS Biomedical Data Translator Project, and is funded by NCATS:

    https://ncats.nih.gov/translator

    Greg Rosenblatt, who sped up Barliman's relational interpreter many order of magnitude, has been hacking on dbKanren, which augments miniKanren with automatic goal reordering, stratified queries/aggregation, a graph database engine, and many other goodies. dbKanren is the heart of mediKanren 2.

    I can imagine co-writing a book on mediKanren 2, and its uses for precision medicine...

    Cheers,

    --Will

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo
  • dissertation-single-spaced

    Single-spaced version of my dissertation, 'Relational Programming in miniKanren: Techniques, Applications, and Implementations'

  • > In general, my opinion is that Prolog's approach is pragmatic, but it was designed in the 1970's when hardware was weaker. With modern hardware, there may be different options that better address the need for purity without sacrificing efficiency.

    I agree. We are investigating various approaches to improve the efficiency of the search, while retaining completeness, for example.

    > Regarding incompleteness, some modern Prologs use SLG-resolution (a.k.a. tabling) to at least avoid the incompleteness resulting by infinite left-recursions. This still allows infinite right recursions but it's easy to get in such a situation with recursion, or even just iteration, in any Turing complete language. I feel that tabling goes a long way towards addressing incompleteness.

    I agree that tabling is useful. Tabling is useful even with a complete search, since it can cut off certain cases in which there are infinitely many answers of similar form, and can change the complexity class of queries.

    A section of my dissertation discusses adding tabling to miniKanren, based on code Ramana Kumar and I worked on, after discussions and readings with Dan Friedman:

    https://github.com/webyrd/dissertation-single-spaced

    That tabling implementation is very tricky, though, and doesn't support constraints other than unification. It's time to revisit and update tabling in miniKanren, I think.

    > Modern Prolog interpreters generally have an option to enable the occurs check (for example, in Swi-Prolog there's an environment flag to enable it for all unifications) and there's also the ISO predicate unify_with_occurs_check/2, that can be used in meta-interpreters, I guess. I think this addresses the soundness concern.

  • microKanren

    The implementation of microKanren, a featherweight relational programming language

  • > I think that with such modern additions (i.e. apart from the cut) Prolog moves closer to the declarative ideal without sacrificing its all-around usability as a general purpose language. What do you think?

    I also used to think that Prolog was moving closer to the delcarative ideal. And I suspect that most expert Prolog programmers believe similarly.

    However, my attitude has changed in the past few years, after seeing Prolog programmers try to implement the relational interpreter from the 2017 ICFP pearl in Prolog.

    The problem is one of composing the pure features needed for expressing a program as complicated as the relational interpreter. (Of course, the relational interpreter is designed to be as short and simple as possible, bit it is still more complicated than pure relations you will find in a Prolog textbook, for example.)

    In theory, you can easily combine unification with the occurs check, SLG-resolution, disequality/disunification constraints, type constraints, etc., and avoid all impure uses of extra-logical features. In practice, I've seen people struggle to combine these features within a single Prolog implementation. In fact, after multiple attempts from multiple Prolog experts, I have yet to see a version of the relational Scheme interpreter in Prolog that can match the behavior of the miniKanren version.

    I'm not claiming that someone couldn't implement a full relational interpreter in Prolog. Obviously they could, since Prolog is Turing-complete. I'm only saying that the default choices of Prolog, plus the intricacies of combining multiple pure features (and leaving out standard and useful non-relational features), seems to make writing a relational interpreter much harder than I would have expected.

    If you are up for a challenge, I'd be happy to work on a Prolog version of the Scheme interpreter with you!

    Based on what I've seen from Prolog experts trying to reproduce the relational interpreter, and conversations with Prolog experts, my current thinking is that Prolog is actually not a good language for relational programming. Too many of the defaults must be adjusted or overridden, too many standard techniques and idioms must be abandoned, and too many potentially incompatible libraries must be composed in order to get everything "just right."

    The problem isn't that relational programming in Prolog isn't possible. The problem is that it requires enough work and non-standard techniques that in practice people don't do it.

    At least, that is what I observe as an outsider.

    If there is an easy way to combine features within a single FOSS Prolog implementation to allow for the types of relational programming we do in miniKanren, I'd be delighted to see it in action. I'd also be delighted to write a paper about it with you! :)

    > Finally, I'd like to know more about minikanrens' search. I'll look around on the internet, but is there a source you would recommend?

    I would recommend reading Jason Hemann and Dan Friedman's lovely little paper on microKanren, which gives a tutorial reconstruction of miniKanren's complete interleaving search, starting from depth-first search:

    http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

    https://github.com/jasonhemann/microKanren

    The standard exercise for learning microKanren is to translate the resulting ~50 lines of Scheme code into the language of your choice.

    You might also like this more technical paper on the `LogicT` monad:

    Backtracking, interleaving, and terminating monad transformers: (functional pearl)

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts