What Is miniKanren?

You might have better luck if you try today using Claude as support?

Sorry about that.

mediKanren's source code is under MIT license, and is on GitHub. Alas, the knowledge graphs we use for mediKanren aren't produced by us, and often have very complex licenses (one KG might include knowledge from 80 or 100 databases, each with a different license). As a result, we can't just release the KGs that are needed to actually use mediKanren. Also, creating high-quality queries that take into account all the nuances and quirks of the KGs is tricky, and changes as the KGs and the Biolink standard evolve. As a result, mediKanren requires some expertise to use effectively, along with access to the KGs.

An application that uses mediKanren as a back-end (along with other reasoners) is the NIH NCATS Biomedical Data Translator:

https://ui.transltr.io/

Please keep in mind that both Translator and mediKanren are designed for researchers and for biomedical research, not for patient care or treatment recommendations.

Have you read their document [0] on how to navigate the process?

[0] https://bertrand.might.net/articles/algorithm-for-precision-...

thank you for posting this... and this is a common enough pattern (looking up previous HN threads on the same or related article) that I wonder if it's worthwhile to automate this.

> unintuitive programming language where the only error message you get is "no",

You know. "Consent" is everything these days.- :)

PS. Preferably in written form ...

Is that even possible for something like this? You've got a pretty long list of implementations, each having its own language specific syntax, e.g. https://github.com/pythological/kanren for one python version - and there are several Python versions linked on the homepage.

On top of that: some examples of the kinds of problems miniKanren can solve, based on real world examples rather than purely abstract concepts (e.g. "given a set of available air flights with origins, destinations, and prices, find me the cheapest way to get from Seattle to London")

No, but I would so love to hear someone from the team give a talk about it. That's so darn awesome

It hasn't been merged into the main branch yet, but you can embed Scryer in Python now[1], and it's quite enjoyable. I've also embedded in Java, Clojure, and elisp[2] :)

The Clojure one is bundled up into a library called libscryer-clj, which I haven't released yet, but it operates the same way as libpython-clj[3], libjulia-clj[4], and libapl-clj[5].

As an aside, Scryer is hella ergonomic. clpz+reif is an amazing and amazingly powerful combination, and Scryer's DCG philsophy over double quoted strings is chefs kiss -- it really delivers on the original mission of Prolog. Ediprolog[6] is a fantastic REPL for Emacs.

And honestly if you haven't seen Marcus Triska's work[7], by God you are missing out on one of the true joys of life.

[1]: https://github.com/jjtolton/scryer-prolog/blob/ISSUE-2464/sc...

[2]: https://github.com/mthom/scryer-prolog/discussions/2687

[3]: https://github.com/clj-python/libpython-clj

[4]: https://github.com/cnuernber/libjulia-clj

[5]: https://github.com/jjtolton/libapl-clj

[6]: https://www.metalevel.at/ediprolog/

[7]: https://www.youtube.com/@ThePowerOfProlog

> if they haven't surpassed SWI in some performance metrics yet I'd be surprised

I was/am also anticipating performance gains from Scryer. Which is why I made a point to request up to date Scryer benchmarks in the SWI forums. Still, for free/open Prolog, SWI-Prolog is hard to beat: https://swi-prolog.discourse.group/t/porting-the-swi-prolog-...

I haven't held any hangouts online for years, although I'd consider restarting them if there is interest.

We do have a monthly call of miniKanren/OCanren researchers from around the world, where someone presents on their research. If you are interested, please send me an email!

Thanks. Personally, I'd love to see more like https://alex-hhh.github.io/2021/08/fish-puzzle.html

When I was in university, the usual Prolog example was solving a game of Cluedo.

The main problem is likely that many programmers aren’t familiar with Scheme, or any kind of Lisp. So the material is presented in the context of a host language that itself requires substantial effort to really get used to.

Personally, while I did some Lisp back in university and was reasonably conversant in it at the time, nowadays whenever something nontrivial is presented in Lisp, it’s just too much mental overhead to get back into it, in addition to trying to understand the thing that is being presented.

Terminology like “logic variable” also needs to be explained, if you want to address an audience that isn’t already familiar with logic programming.

Thanks Will! I think it was the microkanren paper (it's a few years ago now so i'm not 100% sure but seeing it seems familiar). I think I will try the tutorial and see if it helps make it 'click'.

They are commutative. As to whether unification and association are the same thing... yes, kinda. Unifying two terms kinda means associating them with each other in a database. Though I will say that it would have been better to say 'unifies x and z, as well as y and 3'.

Unification in the context of logic programming is basically like "use these questions and solve for all the unknowns" in algebra, except it's done with logical statements instead of algebraic equations. Searching for something like "unification prolog" (Prolog being the most well-known logic programming language) will probably give helpful material.

For example you could start with two facts like "Fedora is red." and "Cat is green." Then if you ask the system "X is red." it'll tell you "X = fedora". If you ask it to list all the solutions of "X and Y are not the same color." it'll list "X = fedora, Y = cat" and "X = cat, Y = fedora". This process of binding variables to values (or other variables during simplification) is unification.

Unification is reflexive:

    (== x x) = x for all x

It is commutative:

    (== x y) = (== y x) for all x and y

It is idempotent:

    (== x (== x y)) = (== x y) for all x and y

And it is associative:

    (== x (== y z)) = (== (== x y) z)

It's not transitive, e.g. if we unify pairs (using made up syntax [a, b]) then

    (== [x, 1] [2, y]) = [2, 1]
    (== [2, y] [z, 3]) = [2, 3]
    (== [x, 1] [z, 3]) does not unify (since 1 does not unify with 3)

Thanks for the follow-ups but my comment wasn't really asking what unify and associate mean, I'm questioning the redundant complexity in what is supposed to be the introductory tutorial to the language.

From the submitted page, "The core language, using Scheme as the host language, is described in this short, interactive tutorial."

but one need to learn lisp to read it?..

To protect the users of the site from receiving pages that have been tampered with?

bit of a trap question - clearly it doesn't need to, plenty of people accessed it in this thread fine and it works. even if it didn't, and there was a prevalent internet standard mandating it these days, you could just handwave it away, claiming that people don't need to respect standards or something.

"why do you expect it to?" i think would have been lot less of a trick question, and that's simple: it's trivial to set up and offers security benefits people - i think reasonably - take for granted these days.

Neat.

> The six simple building blocks: variables, states, and the four kinds of goal — make two values equal, provide local variables to an existing goal, pursue two existing goals separately, and pursue two existing goals together.

> The only data structure is a pair. We can create lists using pairs.

I'll play with it more.

I have a port of https://github.com/dananau/GTPyhop and planner systems feel related to relation programming

If you use HTTP you can have middlemen hijacking your content or inserting malicious things and nobody would know. There's all kinds of weird actors out there.

The risk is that HTTPS is something you have to manage. Either your hosting provider auto-renews certs for you (which might cost) or you set up your own automation (which can fail, and I've seen enough properties with expired LE-issued certs to know that email reminders can be missed and certbot is not a silver bullet). That said, usually an expired cert fails open, ie users can still visit your website if they accept the scary "this is unsafe" warning. This is not an option if your website uses HSTS or is on a TLD with implicit HSTS (eg .dev), but in that case you're opting in to the responsibility of renewing your certs reliably.

The benefit is that you can be sure that nothing modifies the traffic between your server and the client, so the client sees your content without any modification.

The counter-points to the benefit are that a) the traffic can still be *blocked* by any party in the middle (eg a state-level firewall), b) that traffic can absolutely be modified if the client has accepted an alternative CA for whatever reason (legal, corporate, etc) and that CA is used to MITM the connection to your server, and c) you as a website operator don't necessarily care about the MITM situation of every client's network (ie them having a MITM is their problem, not yours).

There's another benefit that browsers restrict some JS API to only run on https pages, which matters if you wanted to use those API. https://developer.mozilla.org/en-US/docs/Web/Security/Secure...

I have a hunch this might be about the difference between "programming" and "coding". Web stuff, Hardware, and other things that don't get to just communicate with other programmers or programmers have a tendency of piling layers upon layers with custom glue and pipes everywhere.

There could be library of UI primitives and backend in logical language, then you would write declaration of what you want exactly:

- I want window of these size, with such controls

- when this button is clicked, text from this control appears in that DB column

and system figures out all details making it cross platform, fault tollerant, etc if all infra is coded on that platform

AWS uses a SAT solver (Z3) to resolve permissions.

I can see miniKanren (or some other logic programming language) being helpful in the realm of authorization.

Thanks! And thanks for miniKanren and reasoned schemer!

The chapters on both constraint solvers and logic programming are pretty short overviews, we're talking less than 15 pages. I wouldn't recommend it if that's what you're specifically interested in.

For SAT/SMT in Python, I've heard this book is pretty good: https://theory.stanford.edu/~nikolaj/programmingz3.html. Google OR-tools has a Python frontend and they have interactive tutorials (https://developers.google.com/optimization/examples). I don't know about logic programming in Python. Note that while there's some overlap between logic programming and constraint solving ([1] [2]), the communities are pretty independent from each other. Different histories, tools, techniques, etc.

[1]: https://www.swi-prolog.org/pldoc/man?section=clpfd

[2]: http://picat-lang.org/picatbook2015.html