Recently, I’ve found myself thinking about logic programming more and more and I wanted to try implementing a logic programming system in Scala.

I’ve based my implementation on Oleg Kiselyov’s toy kanren implementation, stealing some ideas from P. Jansson & J. Jeuring, Functional Pearl: Polytypic Unification.

The essence of logic programming is twofold: relations and unification.

A relation \(R\) over sets \(X, Y\) is a subset of the Cartesian product \(X \times Y\), written \(x R y\) such that \(x \in X, y \in Y\).

We will express relations in Scala using functions assigning a (possibly empty) list of values, to values:

We use `LazyList`

as the computations might be potentially infinite.

We can define two primitive relations, `fail`

which associates to no result for
any value and `succeed`

- a trivial relation that associates the given value to
the given value.

We will use combinators to create more complicated relations:

Mapping a relation \(xRy \subseteq X \times Y\) by `g`

, creates a new relation \(S \subseteq X \times Z\) which “relates” the values of the codomain by \(g\) - \(S = \{ (x, z) \mid x \in X, y \in Y, z \in Z \wedge xRy \wedge z = g(y) \}\)

We can test it:

We can implement `flatMap`

in similar vain - simply by `flatMap`

ping on the `LazyList`

:

Another combinator `disjunction`

, or `\/`

composes relations so that all results of both relations are returned:

Test:

Similarly, we can create a conjunction of relations: a new relation that composes values belonging to both relations.

Test:

Taking a page out of Oleg Kiselyov’s description - a logic variable is a way of encoding improvable knowledge (or less optimistically improvable ignorance):

- an unbound logic variable stands for no knowledge
- a variable may be unified with a value - representing certain knowledge that “something has some value”
- a variable may be unified with another variable, or a expression which is not fully bound - representing incomplete knowledge.

To start we will use a simple `String `

representation of variable ids:

And we will use a standard scala `Map`

for knowledge representation (variable bindings or substitutions):

We will define unification in terms of a type class like the authors of Polytpic Unification:

Understanding why `children`

and `topLevelEquivalent`

should behave as above
it’s useful to look first at an example unifiable type, and the unification function itself.

`Universe`

To implement unification we need to add some methods to `Knowledge`

:

Now we can, finally, implement unification:

And a small test:

Our logic programming system will be implemented through (endo-)relations of `Knowledge`

to `Knowledge`

. We will call such relations goals or predicates, and start the implementation of our system with the primitive goal `unify`

:

We will program the next goal `choice`

against the concrete `Universe`

type:

At this step we’ll introduce some syntax allowing us to “run: predicates:

Running a predicate produces all of the results of the goal (the knowledge obtained when reasoning).

Another predicate we can implement:

Because using and declaring predicates will be so common we could use with some syntax sugar:

And because we actually never want to modify `Knowledge`

in non-primitive
predicates we will use this method for defining predicates:

Which enables us to define commonElement as follows:

I could go on with the definitions of a `cons`

and `append`

predicates, but even at this stage it’s
apparent that the current implementation has some pretty serious limitations.

Firstly, the logical variables we use aren’t scoped in any way - introducing
the variable `x`

does so “globally”.

Secondly, while we are able to write predicates against any arbitrary universe of types, implementing the actual predicates loses the benefit of scala’s type system as the implemented predicates are dynamic/unityped.

I will address these shortcomings in the next blog post.