From cb21f6464bc4b4af995b288083bcfb54abb9ab6f Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Sat, 21 Mar 2026 18:09:23 +1300 Subject: Logic Programming in Ada article added --- project/assets/css/kompsos.css | 20 ++ project/assets/img/goal_graph_inverted.png | Bin 0 -> 23293 bytes project/assets/img/goal_graph_inverted_preview.png | Bin 0 -> 33699 bytes project/assets/img/zebra_graph.png | Bin 0 -> 331182 bytes project/assets/img/zebra_graph_preview.png | Bin 0 -> 24380 bytes project/complexity.yml | 1 + project/context/articles.json | 5 + project/templates/kompsos.xhtml | 374 +++++++++++++++++++++ 8 files changed, 400 insertions(+) create mode 100644 project/assets/css/kompsos.css create mode 100644 project/assets/img/goal_graph_inverted.png create mode 100644 project/assets/img/goal_graph_inverted_preview.png create mode 100644 project/assets/img/zebra_graph.png create mode 100644 project/assets/img/zebra_graph_preview.png create mode 100644 project/templates/kompsos.xhtml 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 Binary files /dev/null and b/project/assets/img/goal_graph_inverted.png differ 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 Binary files /dev/null and b/project/assets/img/goal_graph_inverted_preview.png differ diff --git a/project/assets/img/zebra_graph.png b/project/assets/img/zebra_graph.png new file mode 100644 index 0000000..5e4c439 Binary files /dev/null and b/project/assets/img/zebra_graph.png differ 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 Binary files /dev/null and b/project/assets/img/zebra_graph_preview.png differ 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 %} + +{% endblock -%} + + + +{%- block content %} +

Logic Programming in Ada

+ +

Git repository: Link
+2013 microKanren paper: Link

+ +
21/3/2026
+ + +
Introduction
+ +

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.

+ + +
Language Barrier
+ +

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.

+ + +
Structure of Solution
+ +

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.

+ +
+ + Annotated Goal graph representing the Zebra Puzzle + +
+ Annotated Goal graph representing the Zebra Puzzle
+ (Click for large version) +
+
+ +

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.

+ + +
Evaluation Method
+ +

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.

+ +
+ + Example portion of a Goal graph being inverted + +
+ Example portion of a Goal graph being inverted
+ (Click for large version) +
+
+ +

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.

+ + +
Complete Search
+ +

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.

+ + +
Performance Testing
+ +

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.

+ + +
Results
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
 ZebraLogarithmsHouses
Memory
(MB)		Time
(s)		Memory
(MB)		Time
(s)		Memory
(MB)		Time
(s)
Kompsos5.40.0217.80.5627.32.61
Kompsos
(Vector State)		5.30.0217.80.6627.35.94
Simple-miniKanren8.50.039.40.359.36.96
microKanren9.30.1210.82.29251.1354.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:

+ + + +
Conclusions
+ +

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 -%} + -- cgit