Logic Programming in Ada article addedHEADmaster

8 files changed, 400 insertions, 0 deletions

diff --git a/project/assets/css/kompsos.css b/project/assets/css/kompsos.css
new file mode 100644
index 0000000..625330e
--- /dev/null
+++ b/project/assets/css/kompsos.css
@@ -0,0 +1,20 @@
+
+
+table {
+    margin: 2em auto 2em auto;
+    border: 1px solid gray;
+}
+
+table th {
+    padding: 0.5em 1em 0.5em 1em;
+    border: 1px solid gray;
+    text-align: center;
+}
+
+table td {
+    padding: 0.5em 1em 0.5em 1em;
+    border: 1px solid gray;
+    text-align: right;
+}
+
+
diff --git a/project/assets/img/goal_graph_inverted.png b/project/assets/img/goal_graph_inverted.png
new file mode 100644
index 0000000..6907802
--- /dev/null
+++ b/project/assets/img/goal_graph_inverted.png
diff --git a/project/assets/img/goal_graph_inverted_preview.png b/project/assets/img/goal_graph_inverted_preview.png
new file mode 100644
index 0000000..3fb745e
--- /dev/null
+++ b/project/assets/img/goal_graph_inverted_preview.png
diff --git a/project/assets/img/zebra_graph.png b/project/assets/img/zebra_graph.png
new file mode 100644
index 0000000..5e4c439
--- /dev/null
+++ b/project/assets/img/zebra_graph.png
diff --git a/project/assets/img/zebra_graph_preview.png b/project/assets/img/zebra_graph_preview.png
new file mode 100644
index 0000000..a81b66f
--- /dev/null
+++ b/project/assets/img/zebra_graph_preview.png
diff --git a/project/complexity.yml b/project/complexity.yml
index 46ddcd8..b105064 100644
--- a/project/complexity.yml
+++ b/project/complexity.yml
@@ -20,6 +20,7 @@ unexpanded_templates:
  - "grasp.xhtml"
  - "index.xhtml"
  - "integral.xhtml"
+ - "kompsos.xhtml"
  - "links.xhtml"
  - "numberwall.xhtml"
  - "packrat.xhtml"
diff --git a/project/context/articles.json b/project/context/articles.json
index 90af5b5..c9a4276 100644
--- a/project/context/articles.json
+++ b/project/context/articles.json
@@ -1,5 +1,10 @@
 
 [
+    {   "title": "Logic Programming in Ada",
+        "anchor": "/kompsos.xhtml",
+        "taglist": ["compsci", "library", "programming"],
+        "postdate": "21/3/2026"
+    },
     {   "title": "Auckland Rail Maps",
         "anchor": "/aucklandrail.xhtml",
         "taglist": ["maps", "politics", "transport"],
diff --git a/project/templates/kompsos.xhtml b/project/templates/kompsos.xhtml
new file mode 100644
index 0000000..4fe26d8
--- /dev/null
+++ b/project/templates/kompsos.xhtml
@@ -0,0 +1,374 @@
+
+{%- 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 -%}
+