Annotated Goal graph representing the Zebra Puzzle
(Click for large version)
(Click for large version)
Git repository: Link
2013 microKanren paper: Link
Logic programming is a style of programming where a set of constraints are specified, then computation is applied automatically using some logical reasoning to find solutions. It is a very different way of doing things than the imperative, procedural, object oriented style inherent to Ada. For some paradigms it is possible to bridge the gap by reusing language constructs in ways they were not intended, but that is not going to work here. Some sort of small logic language embedded as a library is needed.
Fortunately, miniKanren is just such a small logic language. It's typically embedded as a library and the core only has three or four operations that have to be implemented, depending on how you count them. It looks almost ideal.
Unfortunately, Ada is still very unsuited to actually implementing it, as miniKanren usually leans heavily on features mostly found in functional programming languages to do what it does. The remainder of this article goes over how I went about it anyway by writing Kompsos, an implementation of miniKanren in Ada following the microKanren core operations of fresh, unify, disjunct, and conjunct.
To begin with, it is worthwhile going over the specific obstacles that make it difficult, or at the very least awkward, to do this in Ada:
Of the above, the biggest problem by far is the Ada Containers library. Since it is not designed to be used in the same way an equivalent library would be in a functional programming language, something like breadth-first search is completely out of the question here. The memory required for having the large number of duplicated Map objects around that miniKanren would use for substitutions without any data sharing involved would be... prohibitive.
The other particularly significant issue is the lack of functional programming support. It is possible to fake it to a degree with generics as higher order functions, but this has its own problem. If the compiler doesn't support shared code for generics then heavy use of them tends to explode the resulting binary size. GNAT, the main compiler currently available for Ada, does not support shared generics. So attempting to imitate the functional style implementation of the microKanren core operations is a bad idea.
It's not all doom and gloom though. Using a more imperative style basically gives the non-lazy version of conjunct operations for free. It also needs no special treatment for query variables and makes selecting specific variables to reify after computation easier.
miniKanren programs typically involve constructing a Goal, then applying it to a State to produce a potentially infinite stream of possible result States. The Goal is a function made up of some combination of operations to unify logical Terms and a disjunct/conjunct boolean logic over other Goals. A State represents a set of Variable substitutions needed to satisfy a Goal. Afterwards, the result States are then traced through to find the final value of a Variable of interest, which is called reifying that Variable.
Implementing the Terms used in unification in Kompsos is reasonably straightforward. They are just reference counted objects that either hold data, are Variables, or hold a pair of further Terms which can be built up as either an implicit linked list or implicit tree. The Variable Terms are exclusively generated using the fresh operation. One may observe how already this is imitating the primary cons cell list datatype of Scheme and other Lisps. Echoes of Greenspun's tenth rule are felt very keenly throughout this project.
Goals are a little harder. Instead of modeling them as lambda expressions as in Scheme, they are also made to be reference counted objects. Specifically, graph nodes. Each node is used to represent the necessary details for either unify, disjunct, or conjunct. Building them up node by node gives a resulting construction of a directed acyclic graph with a single node at the top and a single empty node at the bottom.
Slightly nonobviously, modeling Goals as plain datatypes instead of functions like this means Variable Terms created by fresh are completely separate and have unknown scope. This in turn means tracking the next valid Variable has to be done in Goal rather than in State as miniKanren typically does it, which causes Variable numbering to be a little bit different in initial results. Reified values remain the same, however.
A lot of experimentation was done with States because they are intimitely tied up with how to evaluate Goals. Maps from the Containers library, custom unrolled Linked Lists, and even a custom Hash Array Mapped Trie were all tried. In the end, I went with a Vector of records containing a Variable and a Term each to represent the substitutions, and a Map to make it faster to look up a specific binding in the Vector.
The way a Goal is constructed in miniKanren means applying one to a State will make it evaluate itself, going through step by step switching off at every disjunct operation to interleave results to produce a parallel breadth-first search of possible substitution States. Since a Goal is a plain datatype in Kompsos and data sharing implementations of State are unavailable, that method is unusable.
Instead, the bird's eye view of evaluating a Goal here involves inverting the direction of the arrows in the directed acyclic graph, ordering the possible choices that can be taken, and then conducting a depth-first search from the bottom upwards, expanding conjunct nodes as they are encountered.
Deciding on the proper way to order the possible choices when inverting the graph arrows is done by encoding the traversal of disjunct nodes as a little-endian binary number. For example, choosing all the first options every time would be encoded as all zeros, or just zero. Choosing the second option at the topmost disjunct then the first option for every subsequent would be encoded as a one followed by all zeros, or just one. First option, second option, all remaining first options would be 010000... or in other words two. This gives the expected interleaved ordering. These numbers are of arbitrary length however, so they are treated as Vectors of digits instead of any kind of Integer.
Whenever a conjunct node is encountered in the bottom-up search, it is expanded into the Goal graph that it would have represented and has its arrows inverted and ordered in the same way as above. Then it is spliced into the search graph and the search continues. This does mean information about the previous disjunct traversal and ordering must be kept around to help, as otherwise connecting back into the search graph wouldn't be possible.
Searching from the bottom upwards can be done because the original Goal always has a single node at the bottom as well as the top, due to having been originally built up from nothing by the programmer. Using a depth-first search method means only a single State needs to be kept at any one time. Backtracking in the case of an impossible unify just means discarding the newest substitutions in that State as necessary. A copy of the State is only needed whenever the search actually reaches the top and a result is returned, although returning does complicate matters a bit by needing the whole process to be able to be paused and resumed as in a coroutine.
There's just one problem. Depth-first search is not a complete search strategy. Consider the following miniKanren code:
(define (fives x)
(conde
((== x 5))
((fives x))))
(define (evil x)
(fresh (a)
(conde
((== a 6))
((== x 7)))
(fives a)))
(run 1 (q) (evil q))
If plain depth-first search was used, evaluation would get stuck in the fives function, forever expanding unproductive branches and completely missing the valid solution. While I am uncertain how often similar code occurs in practice, allowing the possibility is unacceptable.
So instead, Kompsos actually uses a variant of iterative deepening depth-first search. This wouldn't be complete either due to the potential infinite branching factor caused by conjunct operations, but that problem is solved by making the depth limit be how many times those very conjunct nodes have been found and expanded. Once the limit is exceeded, the search backtracks to before the first one was seen, increases the limit, and tries other branches before coming back later.
In theory, once the depth limit is exceeded all other branches should be explored to the same depth first, before the search starts from the beginning with an increased limit. In practice I think that is overly conservative. Due to the graph construction of a Goal here, there is nearly always a lot of overlap in potential branches to be explored. One branch hitting the conjunct limit most likely means all the other branches have essentially been expanded similarly, so at that point just backtracking, raising that limit, and continuing makes more sense. It's faster, too.
After making something that works, the next natural step is to test it out. I actually cycled through this quite a bit trying out various outlandish things, then going back and trying yet other things until arriving at the above implementation. Which is at least in the same ballpark as Scheme miniKanrens.
Here I decided to compare four versions:
Each was used to evaluate the following:
Test source code can be found in example/zebra.adb, scheme/zebra.scm, test/logo.adb, scheme/logo.scm, example/houses.adb, and scheme/houses.scm in the Kompsos repository.
Kompsos and associated Ada versions of the tests were compiled with GNAT. Simple-miniKanren, microKanren, and associated Scheme versions of the tests were compiled and run using Guile Scheme. In all cases the highest available optimisation level was used. Everything was compiled and run on an Intel i5-5200U CPU under Linux.
Performance was measured by using /usr/bin/time to run each program six times. The first result was discarded in an attempt to minimise the effect of CPU cache and other similar mechanisms, then the remaining results were averaged. Both program runtime and memory usage were measured.
| Zebra | Logarithms | Houses | ||||
|---|---|---|---|---|---|---|
| Memory (MB) |
Time (s) |
Memory (MB) |
Time (s) |
Memory (MB) |
Time (s) |
|
| Kompsos | 5.4 | 0.02 | 17.8 | 0.56 | 27.3 | 2.61 |
| Kompsos (Vector State) |
5.3 | 0.02 | 17.8 | 0.66 | 27.3 | 5.94 |
| Simple-miniKanren | 8.5 | 0.03 | 9.4 | 0.35 | 9.3 | 6.96 |
| microKanren | 9.3 | 0.12 | 10.8 | 2.29 | 251.1 | 354.35 |
Kompsos performed the best for the Zebra puzzle. Simple-miniKanren was the best for the Logarithm test. And for the Houses problem, Kompsos was the fastest while Simple-miniKanren used the least memory.
There are several interesting and nonobvious details to point out here:
So, what have I learned from this? Well, logic programming in Ada is definitely viable. That isn't really too surprising since any Turing-complete language can emulate any other Turing-complete language with enough effort, but it's nice to know it isn't too difficult.
The performance results obtained should not be considered definitive. For one thing, use of Faster-miniKanren would likely be faster, as might be expected from the name. I did not manage to get it to run in a way that could be included in the comparison. Other options that could be explored include writing custom immutable functional datatypes to use in Ada, such as Finger Trees and Hash Array Mapped Tries.
The microKanren concept, while nice from an explanatory point of view, proved to be terrible in execution with the given Scheme code. It turns out playing code golf is not very helpful.
But perhaps the most relevant thing to answer here: Is it worth it? Sure, you can do logic programming in Ada, but should you? And to that I have to say no, probably not. It is easier now that Kompsos is written, but it's still fighting against the supported paradigms. There is also just a lot more support in terms of research and tooling elsewhere, with no real reason to ignore it.
{% endblock -%}