diff options
| -rw-r--r-- | project/assets/css/kompsos.css | 20 | ||||
| -rw-r--r-- | project/assets/img/goal_graph_inverted.png | bin | 0 -> 23293 bytes | |||
| -rw-r--r-- | project/assets/img/goal_graph_inverted_preview.png | bin | 0 -> 33699 bytes | |||
| -rw-r--r-- | project/assets/img/zebra_graph.png | bin | 0 -> 331182 bytes | |||
| -rw-r--r-- | project/assets/img/zebra_graph_preview.png | bin | 0 -> 24380 bytes | |||
| -rw-r--r-- | project/complexity.yml | 1 | ||||
| -rw-r--r-- | project/context/articles.json | 5 | ||||
| -rw-r--r-- | project/templates/kompsos.xhtml | 374 |
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 Binary files differnew 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 Binary files differnew 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 Binary files differnew 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 Binary files differnew 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"> </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 -%} + |
