Making a "MiniKanren" using Z3Py
Relational/logic programming is quite cool. It let’s you do things that sound impossible, like run a program backwards. Using Z3py to do a lot of heavy lifting, there’s a cute, simple, and pretty powerful little microkanren you can make. You can have it answer queries like the following that run list append backwards.
The microkanren paper is really good, if you can read a little scheme http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf. I talk more and have more links about microkanren here https://www.philipzucker.com/yet-another-microkanren-in-julia/
The non-deterministic search is structured around the concept of a “goal”. A goal transforms a state into a set of possible refined states based on the assertions of the goal. In other words it can be modelled as a function State -> [State].
The state of a minikanren search is described by the currently known unifications. I’m going to short circuit this entire piece to just lean on Z3. This has the upside of not need to implement it, and the downside of Z3 being rather less controlled / general in what it returns compared to using unification.
