Bartosz Witkowski - Blog.

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.

# Relations

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.

## Combinators

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 flatMapping 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:

# Logic Variables and Unification

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:

## Variables and bindings

And we will use a standard scala Map for knowledge representation (variable bindings or substitutions):

## Unifiable

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.

## A small Universe

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

## Unification

Now we can, finally, implement unification:

And a small test:

# Logic Programming

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:

# Limitations

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.