Kompsos

An experimental implementation of miniKanren in Ada, a language very much unsuited for the exercise due to its lack of support for the functional programming paradigm. Came about after reading the 2013 microKanren paper which is quite short, and then noticing that nobody had tried writing it in Ada. The name Kompsos comes from Greek, meaning "elegant" or "refined" or "dainty" and is in reference to the microKanren concept of four primitives.

Typical usage involves declaring a Goal, applying some operations to it including creating a few variable Terms, evaluating that Goal to obtain a number of States, then reifying the variable Terms with respect to one of those States. The reified Terms can then be decomposed at your leisure.

Most commonly only the main Kompsos package and the Math and Pretty_Print child packages will be needed. Although Collector is also used internally for the basic reification.

Dependencies

Build time:

• GNAT
• GPRbuild

There are no particular run time dependencies.

Building and Installation

This repository is written to use the GNAT Project Manager build tools. To build, use the following command

gprbuild kompsos.gpr

There is a single build switch of -Xbuild which can have a value of release (the default) or debug.

If you want to install this project, use

gprinstall -p -m kompsos.gpr

In addition, the project files tests.gpr and examples.gpr can be used to compile several small test and example programs respectively.

For further information on the build tools, consult the GPRbuild docs.

Technical Notes

A brief explanation of the package hierarchy:

• Kompsos Term, State, Goal datatypes, microKanren operations, evaluation, Term reification, and non-numeric miniKanren prelude.
• Kompsos.Advanced_Reify Functions to convert from Term to either a flattened array of data elements or a Multiway_Tree from the Ada Containers library. Reification into a Multiway_Tree.
• Kompsos.Collector Manual stepthrough evaluation of a Goal to find satisfying States.
• Kompsos.Math Arithmetic parts of miniKanren prelude.
• Kompsos.Pretty_Print Conversion of datatypes to Strings, conversion of Goal graphs to the DOT graph desciption language.

Since the arithmetic prelude subprograms are in a child package they are unfortunately not considered primitive operations of the Goal datatype. This makes using them slightly more awkward than they otherwise would be. But placing them all in the main package would not have made sense due to the math operations needing to know what zero and one are. It would also have made the main package unreasonably large.

Internally a Goal is structured as a directed acyclic graph. Evaluation of a Goal involves walking the graph while applying relevant operations to the base State and expanding any Conjuncts to more of the graph as they are encountered. The expanded portions, bookkeeping data, and memoised partial results are all discarded once evaluation is complete.

The various cond operations are completely absent, as they do not really make sense in an object oriented context. Use a Disjunct operation on several Goals instead.

All the Goal operations beyond the microKanren four take an array of Terms as input in order to allow for Conjunct to be reasonably implemented.

The State datatype makes use of custom unrolled linked lists, and the bookkeeping data in the Collector package uses a custom directed acyclic graph structure that reflects the main Goal graph. This is done instead of using Vectors or Maps from the standard library both to improve speed and reduce memory requirements. The improvement due to tail sharing is considerable, despite the theoretically expensive operations involved in walking the list to reify a variable.

Credits and Licensing

Written by Jedidiah Barber

Licensed under the Sunset License v1.0. For details see license.txt.