path: root/project/templates/kompsos.xhtml

{%- extends "base_plain.xhtml" -%}



{%- block title -%}Logic Programming in Ada{%- endblock -%}



{%- block footer -%}{{ plain_footer ("kompsos.xhtml") }}{%- endblock -%}



{%- block style %}
    <link href="/css/kompsos.css" rel="stylesheet" />
{% endblock -%}



{%- block content %}
<h4>Logic Programming in Ada</h4>

<p>Git repository: <a href="/cgi-bin/cgit.cgi/kompsos">Link</a><br />
2013 microKanren paper: <a href="http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf"
class="external">Link</a></p>

<h5>21/3/2026</h5>


<h5>Introduction</h5>

<p>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.</p>

<p>Fortunately, <a href="https://minikanren.org/" class="external">miniKanren</a> 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.</p>

<p>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 <i>fresh</i>, <i>unify</i>,
<i>disjunct</i>, and <i>conjunct</i>.</p>


<h5>Language Barrier</h5>

<p>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:</p>
<ul>
    <li>No functional programming support. This means no first class functions and no lambda
    expressions, but slightly less obviously also no requirement for tail call optimisation.</li>
    <li>The Ada Containers library is not designed for immutability and sharing between instances of
    a data structure. If an algorithm requires building up lots and lots of slight variations of an
    object they are not going to work.</li>
    <li>Return values for functions cannot be implicitly ignored. This means any operation that may
    see use as either a statement without a return value or a function with a return value must have
    two subprograms.</li>
    <li>A type cannot refer to itself within its own definition. It is still possible to construct
    such recursive types, but it requires jumping through some extra hoops involving accesses and
    inheriting from Ada.Finalization.Controlled.</li>
    <li>Subprograms cannot have a variable number of arguments. The closest you can get is to have
    an argument be an unconstrained array type. This is mainly of importance for conjunction.</li>
    <li>Primitive operations for a type have to be defined in the same package as that type. Not
    really a big deal, just makes syntax for using some operations slightly less convenient.</li>
</ul>

<p>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.</p>

<p>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.</p>

<p>It's not all doom and gloom though. Using a more imperative style basically gives the non-lazy
version of <i>conjunct</i> operations for free. It also needs no special treatment for query
variables and makes selecting specific variables to reify after computation easier.</p>


<h5>Structure of Solution</h5>

<p>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.</p>

<p>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 <i>fresh</i> operation. One may observe how already this is
imitating the primary cons cell list datatype of Scheme and other Lisps. Echoes of
<a href="https://en.wikipedia.org/wiki/Greenspun%27s_tenth_rule" class="external">Greenspun's tenth
rule</a> are felt very keenly throughout this project.</p>

<p>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 <i>unify</i>, <i>disjunct</i>, or <i>conjunct</i>. 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.</p>

<div class="figure">
    <a href="/img/zebra_graph.png">
        <img src="/img/zebra_graph_preview.png"
             alt="Annotated Goal graph representing the Zebra Puzzle"
             height="462"
             width="165" />
    </a>
    <div class="figcaption">
        Annotated Goal graph representing the Zebra Puzzle<br />
        (Click for large version)
    </div>
</div>

<p>Slightly nonobviously, modeling Goals as plain datatypes instead of functions like this means
Variable Terms created by <i>fresh</i> 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.</p>

<p>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.</p>


<h5>Evaluation Method</h5>

<p>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 <i>disjunct</i> 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.</p>

<p>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 <i>conjunct</i> nodes as they are
encountered.</p>

<div class="figure">
    <a href="/img/goal_graph_inverted.png">
        <img src="/img/goal_graph_inverted_preview.png"
             alt="Example portion of a Goal graph being inverted"
             height="253"
             width="483" />
    </a>
    <div class="figcaption">
        Example portion of a Goal graph being inverted<br />
        (Click for large version)
    </div>
</div>

<p>Deciding on the proper way to order the possible choices when inverting the graph arrows is done
by encoding the traversal of <i>disjunct</i> 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 <i>disjunct</i> 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.</p>

<p>Whenever a <i>conjunct</i> 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 <i>disjunct</i> traversal and ordering must be kept around to help, as otherwise
connecting back into the search graph wouldn't be possible.</p>

<p>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 <i>unify</i> 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.</p>


<h5>Complete Search</h5>

<p>There's just one problem. Depth-first search is not a complete search strategy. Consider the
following miniKanren code:</p>
<div class="precontain">
<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))
</code>
</div>

<p>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.</p>

<p>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 <i>conjunct</i>
operations, but that problem is solved by making the depth limit be how many times those very
<i>conjunct</i> 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.</p>

<p>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 <i>conjunct</i>
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.</p>


<h5>Performance Testing</h5>

<p>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.</p>

<p>Here I decided to compare four versions:</p>
<ul>
    <li>Kompsos, as outlined above.</li>
    <li>Kompsos modified so State is implemented with only a Vector, which should make it closer in
    time complexity to the States in the next two.</li>
    <li><a href="https://github.com/miniKanren/simple-miniKanren" class="external">Simple-miniKanren</a>
    which is a cleaned up and improved version of the original.</li>
    <li>microKanren, made by collecting snippets from the 2013 paper and pairing them with the
    prelude definitions from Simple-miniKanren.</li>
</ul>

<p>Each was used to evaluate the following:</p>
<ul>
    <li>An implementation of the
    <a href="https://en.wikipedia.org/wiki/Zebra_Puzzle" class="external">Zebra Puzzle</a>.</li>
    <li>The test originally used by miniKanren to check whether the <i>logo</i> function for
    evaluating logarithms is working properly by running it several times with varying parameters.
    </li>
    <li>A house number logic problem from an Algebra textbook. This one is particularly good at
    stress testing how an implementation handles constraints involving numbers.</li>
</ul>

<p>Test source code can be found in <i>example/zebra.adb</i>, <i>scheme/zebra.scm</i>,
<i>test/logo.adb</i>, <i>scheme/logo.scm</i>, <i>example/houses.adb</i>, and <i>scheme/houses.scm</i>
in the Kompsos repository.</p>

<p>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.</p>

<p>Performance was measured by using <i>/usr/bin/time</i> 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.</p>


<h5>Results</h5>

<table class="results">
    <tr>
        <th rowspan="2">&nbsp;</th>
        <th colspan="2">Zebra</th>
        <th colspan="2">Logarithms</th>
        <th colspan="2">Houses</th>
    </tr>
    <tr>
        <th>Memory<br />(MB)</th>
        <th>Time<br />(s)</th>
        <th>Memory<br />(MB)</th>
        <th>Time<br />(s)</th>
        <th>Memory<br />(MB)</th>
        <th>Time<br />(s)</th>
    </tr>
    <tr>
        <th>Kompsos</th>
        <td>5.4</td>
        <td>0.02</td>
        <td>17.8</td>
        <td>0.56</td>
        <td>27.3</td>
        <td>2.61</td>
    </tr>
    <tr>
        <th>Kompsos<br />(Vector State)</th>
        <td>5.3</td>
        <td>0.02</td>
        <td>17.8</td>
        <td>0.66</td>
        <td>27.3</td>
        <td>5.94</td>
    </tr>
    <tr>
        <th>Simple-miniKanren</th>
        <td>8.5</td>
        <td>0.03</td>
        <td>9.4</td>
        <td>0.35</td>
        <td>9.3</td>
        <td>6.96</td>
    </tr>
    <tr>
        <th>microKanren</th>
        <td>9.3</td>
        <td>0.12</td>
        <td>10.8</td>
        <td>2.29</td>
        <td>251.1</td>
        <td>354.35</td>
    </tr>
</table>

<p>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.</p>

<p>There are several interesting and nonobvious details to point out here:</p>
<ul>
    <li>Scheme versions are multithreaded while the Ada Kompsos implementation is single
    threaded. Typically this means the Scheme versions were doing about 15-40% more work than is
    apparent from the runtime as measured by the clock.</li>
    <li>Extra memory usage in Kompsos compared to Simple-miniKanren is likely due to way the
    Maps work in the Ada Containers library. They do not appear to be particularly memory efficient
    for these sorts of programs.</li>
    <li>Faster time in Simple-miniKanren for the Logarithm test is likely due to sharing of
    intermediate results in successive runs being possible in Scheme but not in Ada.</li>
    <li>Simple-miniKanren is highly space efficient, which is impressive for something using
    breadth-first search.</li>
    <li>I have no idea why the performance of microKanren is so poor. Perhaps due to excessive
    inverse-eta-delay?</li>
    <li>Performance characteristics of Kompsos could easily change if many results were required
    from a single run due to the use of iterative deepening depth-first search.</li>
</ul>


<h5>Conclusions</h5>

<p>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.</p>

<p>The performance results obtained should not be considered definitive. For one thing, use of
<a href="https://github.com/miniKanren/faster-miniKanren" class="external">Faster-miniKanren</a>
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
<a href="https://en.wikipedia.org/wiki/Finger_tree" class="external">Finger Trees</a> and
<a href="https://en.wikipedia.org/wiki/Hash_array_mapped_trie" class="external">Hash Array Mapped
Tries</a>.</p>

<p>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.</p>

<p>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.</p>
{% endblock -%}